×

zbMATH — the first resource for mathematics

Clause vivification by unit propagation in CDCL SAT solvers. (English) Zbl 07153711
Summary: Original and learnt clauses in Conflict-Driven Clause Learning (CDCL) SAT solvers often contain redundant literals. This may have a negative impact on solver performance, because redundant literals may deteriorate both the effectiveness of Boolean constraint propagation and the quality of subsequent learnt clauses. To overcome this drawback, we propose a clause vivification approach that eliminates redundant literals by applying unit propagation. The proposed clause vivification is activated before the SAT solver triggers some selected restarts, and only affects a subset of original and learnt clauses, which are considered to be more relevant according to metrics like the literal block distance (LBD). Moreover, we conducted an empirical investigation with instances coming from the hard combinatorial and application categories of recent SAT competitions. The results show that a significant number of additional instances are solved when the proposed approach is incorporated into five of the best performing CDCL SAT solvers (Glucose, TC\(_-\)Glucose, COMiniSatPS, MapleCOMSPS and MapleCOMSPS\(_-\)LRB). More importantly, the empirical investigation includes an in-depth analysis of the effectiveness of clause vivification. It is worth mentioning that one of the SAT solvers described here was ranked first in the main track of SAT Competition 2017 thanks to the incorporation of the proposed clause vivification. That solver was further improved in this paper and won the bronze medal in the main track of SAT Competition 2018.
MSC:
68T Artificial intelligence
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Cook, S. A., The complexity of theorem-proving procedures, (Proceedings of the Third Annual ACM Symposium on Theory of Computing (1971), ACM), 151-158
[2] Bacchus, F.; Winter, J., Effective preprocessing with hyper-resolution and equality reduction, (Proceedings of SAT-2003 (2003)), 341-355 · Zbl 1204.68176
[3] Eén, N.; Biere, A., Effective preprocessing in SAT through variable and clause elimination, (Proceedings of SAT-2005 (2005)), 61-75 · Zbl 1128.68463
[4] Piette, C.; Hamadi, Y.; Sais, L., Vivifying propositional clausal formulae, (Proceedings of ECAI-2008 (2008)), 525-529
[5] Järvisalo, M.; Heule, M.; Biere, A., Inprocessing rules, (Proceedings of IJCAR-2012 (2012)), 355-370 · Zbl 1358.68256
[6] Beame, P.; Kautz, H.; Sabharwal, A., Towards understanding and harnessing the potential of clause learning, J. Artif. Intell. Res., 22, 319-351 (2004) · Zbl 1080.68651
[7] Sörensson, N.; Biere, A., Minimizing learned clauses, (Proceedings of SAT-2009. Proceedings of SAT-2009, LNCS, vol. 5584 (2009), Springer), 237-243
[8] Wieringa, S.; Heljanko, K., Concurrent clause strengthening, (Proceedings of SAT-2013 (2013), Springer), 116-132 · Zbl 1390.68586
[9] Van Der Grinten, A.; Wotzlaw, A.; Speckenmeyer, E.; Porschen, S., Satuzk: solver description, (Proc. of SAT Challenge (2012)), 54-55
[10] Fazekas, K.; Biere, A.; Scholl, C., Incremental inprocessing in SAT solving, (Proceedings of SAT-2019. Proceedings of SAT-2019, LNCS, vol. 11628 (2019), Springer Verlag), 136-154
[11] Han, H.; Somenzi, F., On-the-fly clause improvement, (Proceedings of SAT-2009 (2009), Springer), 209-222
[12] Hamadi, Y.; Jabbour, S.; Saïs, L., Learning for dynamic subsumption, (Proceedings of ICTAI-2009 (2009)), 328-335
[13] Han, H.; Somenzi, F., Alembic: an efficient algorithm for CNF preprocessing, (Proceedings of DAC-2007 (2007)), 582-587
[14] Biere, A., Lingeling, Plingeling, Picosat and Precosat at SAT Race 2010 (2010), Johannes Kepler University: Johannes Kepler University Linz, Austria, FMV Report Series Technical Report 10/1
[15] Biere, A., Lingeling and friends entering the SAT Challenge 2012, (Proceedings of SAT Challenge (2012)), 33-34
[16] Biere, A., Lingeling, Plingeling and Treengeling entering the SAT Competition 2013, (Proceedings of SAT Competition 51 (2013))
[17] Biere, A., Yet another local search solver and lingeling and friends entering the SAT Competition 2014, SAT Competition, 2014, 2, 65 (2014)
[18] Biere, A., Lingeling and Friends Entering the SAT Race 2015 (2015), Johannes Kepler University: Johannes Kepler University Linz, Austria, FMV Report Series Technical Report 15 (2)
[19] Biere, A., Splatz, Lingeling, Plingeling, Treengeling, YalSAT entering the SAT Competition 2016, (Proc. of SAT Competition (2016)), 44-45
[20] Manthey, N.; Stephan, A.; Werner, E., Riss 6 solver and derivatives, (Proceedings of SAT Competition 2016: Solver and Benchmark Descriptions (2016)), 56-57
[21] Luo, M.; Li, C.; Xiao, F.; Manyà, F.; Lü, Z., An effective learnt clause minimization approach for CDCL SAT solvers, (Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence. Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence, IJCAI, Melbourne, Australia (2017)), 703-711
[22] Audemard, G.; Simon, L., Predicting learnt clauses quality in modern SAT solvers, (Proceedings of IJCAI-2009 (2009)), 399-404
[23] Oh, C., Improving SAT Solvers by Exploiting Empirical Characteristics of CDCL (2016), New York University: New York University NY, USA, Ph.D. thesis
[24] Liang, J. H.; Oh, C.; Ganesh, V.; Czarnecki, K., CHBR glucose, (Proceedings of SAT Competition 2016: Solver and Benchmark Descriptions (2016)), 52-53
[25] Liang, J. H.; Ganesh, V.; Poupart, P.; Czarnecki, K., Learning rate based branching heuristic for SAT solvers, (Proceedings of SAT-2016 (2016)), 123-140 · Zbl 06623509
[26] Moon, S.; Mary, I., CHBR glucose, (Proceedings of SAT Competition 2016: Solver and Benchmark Descriptions (2016)), 27
[27] Ryvchin, V.; Nadel, A., Maple_LCM_Dist_ChronoBT: featuring chronological backtracking, (Proc. of SAT Competition 2018 - Solver and Benchmark Descriptions. Proc. of SAT Competition 2018 - Solver and Benchmark Descriptions, Department of Computer Science Series of Publications B (2018), University of Helsinki), 29
[28] Yang, X.; Guanfeng, W.; Qingshan, C.; Shuwei, C., Maple_LCM_Scavel and Maple_LCM_Scavel_200, (Proc. of SAT Competition 2018 - Solver and Benchmark Descriptions. Proc. of SAT Competition 2018 - Solver and Benchmark Descriptions, Department of Computer Science Series of Publications B (2018), University of Helsinki), 30
[29] (Heule, M.; Järvisalo, M.; Martin, S., Proc. of SAT Competition 2018 - Solver and Benchmark Descriptions. Proc. of SAT Competition 2018 - Solver and Benchmark Descriptions, Department of Computer Science Series of Publications B (2018), University of Helsinki)
[30] Luo, M.; Xiao, F.; Li, C.-M.; Manyà, F.; Lü, Z., Maple_CM, Maple_CM_Dist, Maple_CM_ordUIP and Maple_CM_ordUIP+ in the SAT Competition 2018, (Proc. of SAT Competition 2018 - Solver and Benchmark Descriptions. Proc. of SAT Competition 2018 - Solver and Benchmark Descriptions, Department of Computer Science Series of Publications B (2018), University of Helsinki), 44-46
[31] Marques-Silva, J. P.; Sakallah, K. A., GRASP: a search algorithm for propositional satisfiability, IEEE Trans. Comput., 48, 5, 506-521 (1999) · Zbl 1392.68388
[32] Moskewicz, M.; Madigan, C.; Zhao, Y.; Zhang, L.; Malik, S., Chaff: engineering an efficient SAT solver, (Proceedings of DAC-2001 (2001)), 530-535
[33] Liang, J. H.; Ganesh, V.; Poupart, P.; Czarnecki, K., Exponential recency weighted average branching heuristic for SAT solvers, (Proceedings of AAAI-16 (2016)), 3434-3440
[34] Xiao, F.; Li, C.-M.; Luo, M.; Manyà, F.; Lü, Z.; Li, Y., A branching heuristic for SAT solvers based on complete implication graphs, Sci. China Inf. Sci., 62, 7, 1-13 (2019)
[35] Zhang, L.; Madigan, C.; Moskewicz, M.; Malik, S., Efficient conflict driven learning in a Boolean satisfiability solver, (Proceedings of ICCAD-2001 (2001)), 279-285
[36] Marques-Silva, J. P.; Sakallah, K. A., GRASP—a new search algorithm for satisfiability, (Proceedings of ICCAD-1996 (1996)), 220-227
[37] Wotzlaw, A.; van der Grinten, A.; Speckenmeyer, E., Effectiveness of pre- and inprocessing for CDCL-based SAT solving, arXiv preprint
[38] Marques-Silva, J., Algebraic simplification techniques for propositional satisfiability, (Proceedings of CP-2000 (2000), Springer), 537-542 · Zbl 1044.68781
[39] Heule, M. J.; Järvisalo, M.; Biere, A., Efficient CNF simplification based on binary implication graphs, (Proceedings of SAT-2011 (2011)), 201-215 · Zbl 1330.68269
[40] M. Soos, Cryptominisat 2.5.0, SAT Race competitive event booklet.
[41] Jeroslow, R. G.; Wang, J., Solving propositional satisfiability problems, Ann. Math. Artif. Intell., 1, 1, 167-187 (1990) · Zbl 0878.68107
[42] Biere, A., CaDiCaL, Lingeling, Plingeling, Treengeling, YalSAT entering the SAT Competition 2017, (Balyo, T.; Heule, M.; Järvisalo, M., Proc. of SAT Competition 2017 - Solver and Benchmark Descriptions. Proc. of SAT Competition 2017 - Solver and Benchmark Descriptions, Department of Computer Science Series of Publications B, vol. B-2017-1 (2017), University of Helsinki), 14-15
[43] Audemard, G.; Simon, L., Glucose and Syrup in the SAT’18, (Proc. of SAT Competition 2018 - Solver and Benchmark Descriptions. Proc. of SAT Competition 2018 - Solver and Benchmark Descriptions, Department of Computer Science Series of Publications B (2018), University of Helsinki), 24-25
[44] Biere, A., CaDiCaL, Lingeling, Plingeling, Treengeling, YalSAT entering the SAT Competition 2018, (Proc. of SAT Competition 2018 - Solver and Benchmark Descriptions. Proc. of SAT Competition 2018 - Solver and Benchmark Descriptions, Department of Computer Science Series of Publications B (2018), University of Helsinki), 13-14
[45] Eén, N.; Sörensson, N., An extensible SAT-solver, (Proceedings of SAT-2013 (2003), Springer), 502-518 · Zbl 1204.68191
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.