Abstract
It is of great the oretical and practical significance to develop the efficient SAT solvers due to its important applications in hardware and software verifications and so on, and learnt clauses play the crucial role in state of the art SAT solvers. In order to effectively manage learnt clauses, avoid the geometrical growth of learnt clauses, reduce the memory footprint of the redundant learnt clauses and improve the efficiency of the SAT solver eventually, learnt clauses need to be evaluated properly. The commonly used evaluation methods are based on the length of learnt clause, while short clauses are kept according to these methods. One of the current mainstream practices is the variable state independent decaying sum (VSIDS) evaluation method, the other is based on the evaluation of the literals blocks distance (LBD). There have been also some attempts to combine these two methods. The present work is focused on the hybrid evaluation algorithm by combining the trend intensity and the LBD. Based on the analysis of the frequency of learnt clauses, the trend of learnt clause being used is taken as an evaluation method which is then mixed with the LBD evaluation algorithm. The hybrid algorithm not only reflects the distribution of learnt clauses in conflict analysis, but also makes full use of literals information. The experimental comparison shows that the hybrid evaluation algorithm has advantages over the LBD evaluation algorithm in both the serial version and the parallel version of SAT solver, and the number of problems solved has significantly increased.
Article PDF
Avoid common mistakes on your manuscript.
References
S.A. Cook, The complexity of theorem proving procedures, in Proceeding of 3rd Annual ACM Symposium on Theory of Computing, New York, 1971, pp. 151–158.
E. Clarke, A. Biere, R. Raimi, Y. Zhu, Bounded model checking using satisfiability solving, Form. Method. Syst. Des. 19(1) (2001), 7–34.
Y. Vizel, G. Weissengbcher, S. Malik, Boolean satisfiability solvers and their applications in model checking, Proc. IEEE. 103(11) (2015), 2021–2035.
L. Kuper, G. Katz, J. Gottschlich, K. Julian, C. Barrett, M. Kochenderfer, Toward Scalable Verification for Safety-Critical Deep Networks, ar**v preprint ar**v: 1801.05950, 2018.
M. Davis, H. Putnam, A computing procedure for quantification theory, J. ACM. 7(3) (1960), 201–215.
J. Franco, M. Paull, Probabilistic analysis of the Davis Putnam procedure for solving the satisfiability problem, Discrete Appl. Math. 5(1) (1983), 77–87.
J.P. Marques-Silva, K.A. Sakallah, GRASP: a search algorithm for propositional satisfiability. IEEE Transac. Comput. 48(5) (1999), 506–521.
M.W. Moskewicz, C.F. Conor, Y. Zhao, L. Zhang, S. Malik, Chaff: engineering an efficient SAT solver, in Proceedings of the 38th annual Design Automation Conference, ACM, New York, 2001, pp. 530–535.
N. Een, N. Sorensson, An extensible SAT-solver, in: Theory and Applications of Satisfiability Testing, Springer, Berlin, Heidelberg, 2004, pp. 502–518.
J. Marques-Silva, I. Lynce, S. Malik, Conflict-driven clause learning SAT solvers, in: A. Biere, M. Heule, H. van Maaren, T. Walsh (Eds.), Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications. IOS Press, The Netherlands, 2009, pp. 131–153.
G. Audemard, L. Simon, Glucose: A solver that predicts learnt clauses quality, SAT Competition, Swansea, Wales, United Kingdom, June 30–July 3, 2009, pp. 7–8.
T. Ehlers, SAT and CP-Parallelisation and Applications, Universitätsbibliothek Kiel, Germany, 2017.
N. Sorensson, N. Een, Minisat v1.13- A SAT solver with conflict-clause minimization, SAT Competition. 2005(53) (2005), 1–2.
J.H. Liang, C. Oh, V. Ganesh, K. Czarnecki, P. Poupart, Maple-COMSPS, MapleCOMSPS LRB, Maple COMSPS CHB, SAT Competition Bordeaux, France, 2016, p. 52.
A.Biere, P{re, i}coSAT, SAT Competition, Swansea, Wales, United Kingdom, June 30–July 3, 2009, pp. 41–43.
A. Biere, Lingeling and friends entering the SAT challenge 2012, in Proceedings of SAT Challenge, 2012, pp. 33–34.
Y. Hamadi, J. Said, S. Lakhdar, ManySAT: a parallel SAT solver, J. Satisfiability Boolean Model. Comput. 6 (2008), 245–262.
O. Roussel, Description of ppfolio (2011), in Proceeding of SAT, Trento, Italy, June 17–20, 2012, p. 46.
A. Biere, Lingeling, plingeling, picosat and precosat at sat race 2010, FMV Rep Ser. Tech. Rep. 10(1) (2010), 1–4.
A. Biere, Splatz, Lingeling, PLingeling, Treengeling, YalSAT Entering the SAT Competition 2016, in Proceedings of SAT Competition, 2016, pp. 44–45.
G. Audemard, L. Simon, Glucose and Syrup in the SAT Race 2015, SAT Race, Austin, Texas, USA, September 24–27, 2015.
W. Chrabakh, R. Wolski, GridSAT: a system for solving satisfiability problems using a computational grid, Parallel Comput. 32(9) (2006), 660–687.
M. Lewis, T. Schubert, B. Becker, Multithreaded SAT solving, in Design Automation Conference, 2007, ASP-DAC’07 (Asia and South Pacific IEEE 2007), pp. 926–931.
M. Heule, M. Jarvisalo, T. Balyo, Results page of SAT Competition 2017, Sept. 1, 2017. Retrieved September 20, 2018, from https://baldur.iti.kit.edu/sat-competition-2017/index.php?cat=results
K. Claessen, N. Een, M. Sheeran, N. Sorensson, SAT-solving in practice, in Discrete Event Systems, WODES 2008, 9th International Workshop on IEEE, 2008, pp. 61–67.
J.H. Liang, V. Ganesh, P. Poupart, K. Czarnecki, Learning rate based branching heuristic for SAT solvers, in Proceedings of the 19th International Conference on Theory and Applications of Satisfiability Testing, Springer, Cham, 2016.
J.H. Liang, V. Ganesh, P. Poupart, K. Czarnecki, Exponential recency weighted average banching heuristic for SAT solvers, in AAAI, 2016, pp. 3434–3440.
M. Soos, The CryptoMiniSat 5 set of solvers at SAT Competition 2016, in SAT Competition, Bordeaux, France, 2016, p. 28.
G. Audemard, L. Simon, Lazy clause exchange policy for parallel SAT solvers, in Theory and Applications of Satisfiability Testing–SAT 2014–17th Internation Conference Vienna, Austria, 2014.
A. Gilles, L. Simon, On the Glucose SAT solver, Int. J. Artif. Intell. Tools. 27(1) (2018). 1840001.
Z.H. Fu, M. Yogesh, M. Sharad, New features of the SAT04 versions of zChaff, in SAT Competition 2004, Solver Descriptions, 2004.
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
This is an open access article distributed under the CC BY-NC 4.0 license (http://creativecommons.org/licenses/by-nc/4.0/).
About this article
Cite this article
Wu, G., Chen, Q., Xu, Y. et al. A Hybrid Learnt Clause Evaluation Algorithm for SAT Problem. Int J Comput Intell Syst 12, 250–258 (2018). https://doi.org/10.2991/ijcis.2018.125905645
Received:
Revised:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.2991/ijcis.2018.125905645