×

The MergeSat solver. (English) Zbl 07495587

Li, Chu-Min (ed.) et al., Theory and applications of satisfiability testing – SAT 2021. 24th international conference, Barcelona, Spain, July 5–9, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12831, 387-398 (2021).
Summary: Successful SAT solvers in recent competitions are typically based on the winner of the previous competition. Due to this procedure, for multiple years relevant features like incremental solving have not been supported by winning solvers anymore. Furthermore, bug fixes in one solver do not evolve into predecessors. This work presents MergeSat, a SAT solver that is also based on leading solvers of the past years. However, MergeSat can replace MiniSat or Glucose, as relevant features have been added back. Also, new techniques from other solvers of the community have been adapted, and implementation issues have been identified and fixed. These issues did not surface in an original solver or its successor during competitions. Finally, we provide a mechanism to easily incorporate changes of other solver, as well as a development and test environment to identify potential issues when merging techniques early. With this setup, MergeSat is a good starting point for future research development and integration into other solvers.
For the entire collection see [Zbl 1482.68030].

MSC:

68Q25 Analysis of algorithms and problem complexity
68R07 Computational aspects of satisfiability
68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
PDF BibTeX XML Cite
Full Text: DOI

References:

[1] Audemard, G.; Lagniez, J-M; Simon, L.; Järvisalo, M.; Van Gelder, A., Improving glucose for incremental SAT solving with assumptions: application to MUS extraction, Theory and Applications of Satisfiability Testing - SAT 2013, 309-317 (2013), Heidelberg: Springer, Heidelberg · Zbl 1390.68587
[2] Audemard, G., Simon, L.: Predicting learnt clauses quality in modern sat solvers. In: Proceedings of the 21st International Jont Conference on Artifical Intelligence, IJCAI’09, pp. 399-404. Morgan Kaufmann Publishers Inc., San Francisco (2009)
[3] Balint, A., Belov, A., Heule, M.J., Järvisalo, M. (eds.): Proceedings of SAT Challenge 2013, Department of Computer Science Series of Publications B, vol. B-2013-1. University of Helsinki, Helsinki, Finland (2013)
[4] Balyo, T.; Biere, A.; Iser, M.; Sinz, C., SAT race 2015, Artif. Intell., 241, 45-65 (2016) · Zbl 1392.68381
[5] Balyo, T., Froleyks, N., Heule, M., Iser, M., Järvisalo, M., Suda, M. (eds.): Department of Computer Science Report Series B, vol. B-2020-1. University of Helsinki (2020)
[6] Balyo, T.; Sanders, P.; Sinz, C.; Heule, M.; Weaver, S., HordeSat: a massively parallel portfolio SAT solver, Theory and Applications of Satisfiability Testing - SAT 2015, 156-172 (2015), Cham: Springer, Cham · Zbl 1471.68237
[7] Balyo, T., Heule, M., Järvisalo, M.: Proceedings of SAT Competition 2017: Solver and Benchmark Descriptions, Series of Publications B, vol. B-2017-1. Department of Computer Science, University of Helsinki, Finland (2017)
[8] Balyo, T., Heule, M.: Proceedings of SAT Competition 2016: Solver and Benchmark Descriptions. Department of Computer Science Series of Publications B, University of Helsinki, Finland (2016)
[9] Bayless, S., Bayless, N., Hoos, H.H., Hu, A.J.: Sat modulo monotonic theories. In: Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence, AAAI’15, pp. 3702-3709. AAAI Press (2015)
[10] Belov, A., Diepold, D., Heule, M.J., Järvisalo, M. (eds.): Proceedings of SAT Competition 2014, Department of Computer Science Series of Publications B, vol. B-2014-2. University of Helsinki, Helsinki, Finland (2014)
[11] Biere, A.: PrecoSAT system description (2009). http://fmv.jku.at/precosat/preicosat-sc09.pdf
[12] Biere, A.: Lingeling, Plingeling, PicoSAT and PrecoSAT at SAT Race 2010. FMV Report Series Technical Report 10/1, Johannes Kepler University, Linz, Austria (2010)
[13] Biere, A.: CaDiCaL, Lingeling, Plingeling, Treengeling, YalSAT entering the SAT competition 2017. In: Balyo, T., Heule, M., Järvisalo, M. (eds.) Proceedings of SAT Competition 2017 - Solver and Benchmark Descriptions. Department of Computer Science Series of Publications B, vol. B-2017-1, pp. 14-15. University of Helsinki (2017)
[14] Biere, A., Fazekas, K., Fleury, M., Heisinger, M.: CaDiCaL, kissat, paracooba, plingeling and treengeling entering the SAT competition 2020. In: Balyo, T., Froleyks, N., Heule, M., Iser, M., Järvisalo, M., Suda, M. (eds.) Proc. of SAT Competition 2020 - Solver and Benchmark Descriptions. Department of Computer Science Report Series B, vol. B-2020-1, pp. 51-53. University of Helsinki (2020)
[15] Brummayer, R., Biere, A.: Fuzzing and delta-debugging SMT solvers. In: Workshop SMT 2010, pp. 1-5. ACM (2009)
[16] Clarke, E.; Kroening, D.; Lerda, F.; Jensen, K.; Podelski, A., A tool for checking ANSI-C programs, Tools and Algorithms for the Construction and Analysis of Systems, 168-176 (2004), Heidelberg: Springer, Heidelberg · Zbl 1126.68470
[17] Eén, N.; Sörensson, N.; Giunchiglia, E.; Tacchella, A., An extensible SAT-solver, Theory and Applications of Satisfiability Testing, 502-518 (2004), Heidelberg: Springer, Heidelberg · Zbl 1204.68191
[18] Ehlers, T., Nowotka, D.: Tuning parallel sat solvers. In: Berre, D.L., Järvisalo, M. (eds.) Proceedings of Pragmatics of SAT 2015 and 2018. EPiC Series in Computing, vol. 59, pp. 127-143. EasyChair (2019). https://easychair.org/publications/paper/NkG7
[19] Xiao, F., Luo, M., Li., C.M., Manya F., Lü, Z.: MapleLRB_LCM, Maple_LCM, Maple_LCM_Dist, MapleLRB_LCMoccRestart and Glucose-3.0+width in SAT Competition (2017)
[20] Fichte, J.K., Manthey, N., Stecklina, J., Schidler, A.: Towards faster reasoners by using transparent huge pages (2020). https://arxiv.org/abs/2004.14378
[21] Heule Jr, M., Warren, A.H., Wetzler, N.: Trimming while checking clausal proofs. In: FMCAD (2013) · Zbl 1423.68475
[22] Heule, M., Järvisalo, M., Suda, M. (eds.): Proceedings of SAT Competition 2018: Solver and Benchmark Descriptions, Department of Computer Science Series of Publications B, vol. B-2018-1. Department of Computer Science, University of Helsinki, Finland (2018)
[23] Heule, M., Järvisalo, M., Suda, M. (eds.): Proceedings of SAT Race 2019: Solver and Benchmark Descriptions, Department of Computer Science Report Series B, vol. B-2019-1. Department of Computer Science, University of Helsinki, Finland (2019)
[24] Hickey, R.; Bacchus, F.; Janota, M.; Lynce, I., Speeding up assumption-based SAT, Theory and Applications of Satisfiability Testing - SAT 2019, 164-182 (2019), Cham: Springer, Cham · Zbl 1441.68226
[25] Hickey, R.; Bacchus, F.; Pulina, L.; Seidl, M., Trail saving on backtrack, Theory and Applications of Satisfiability Testing - SAT 2020, 46-61 (2020), Cham: Springer, Cham · Zbl 07331011
[26] Hölldobler, S.; Manthey, N.; Saptawijaya, A.; Fermüller, CG; Voronkov, A., Improving resource-unaware SAT solvers, Logic for Programming, Artificial Intelligence, and Reasoning, 519-534 (2010), Heidelberg: Springer, Heidelberg · Zbl 1306.68145
[27] Hoos, HH; Kaufmann, B.; Schaub, T.; Schneider, M.; Nicosia, G.; Pardalos, P., Robust benchmark set selection for boolean constraint solvers, Learning and Intelligent Optimization, 138-152 (2013), Heidelberg: Springer, Heidelberg
[28] Hutter, F.; Hoos, HH; Leyton-Brown, K.; Stützle, T., Paramils: an automatic algorithm configuration framework, J. Artif. Int. Res., 36, 1, 267-306 (2009) · Zbl 1192.68831
[29] Liang, J.H., Chanseok Oh, V.G.K.C., Poupart, P.: MapleCOMSPS, MapleCOMSPS_LRB, MapleCOMSPS \(\_\) CHB. In: Proceedings of SAT Competition 2016 (2016). http://hdl.handle.net/10138/164630
[30] Katebi, H.; Sakallah, KA; Marques-Silva, JP; Sakallah, KA; Simon, L., Empirical study of the anatomy of modern sat solvers, Theory and Applications of Satisfiability Testing - SAT 2011, 343-356 (2011), Heidelberg: Springer, Heidelberg · Zbl 1330.68271
[31] Kochemazov, S.; Pulina, L.; Seidl, M., Improving implementation of SAT competitions 2017-2019 winners, Theory and Applications of Satisfiability Testing - SAT 2020, 139-148 (2020), Cham: Springer, Cham · Zbl 07331018
[32] Kottler, S.: Description of the sapperlot, sartagnan and moussaka solvers for the sat-competition 2011 (2011)
[33] Manthey, N.: Refining unsatisfiable cores in incremental SAT solving. Technical report, TU Dresden (2015)
[34] Manthey, N., Lindauer, M.: Spybug: Automated bug detection in the configuration space of sat solvers. In: SAT, pp. 554-561 (2016) · Zbl 1475.68443
[35] Luo, M., Li, C.M., Xiao, F., Manya, F., Lü, Z.: An effective learnt clause minimization approach for CDCL SAT solvers. In: Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence, IJCAI-17, pp. 703-711 (2017). doi:10.24963/ijcai.2017/98
[36] Martins, R.; Manquinho, V.; Lynce, I.; Sinz, C.; Egly, U., Open-WBO: a modular MaxSAT solver, Theory and Applications of Satisfiability Testing - SAT 2014, 438-445 (2014), Cham: Springer, Cham · Zbl 1423.68461
[37] ML4AAD Group: SMAC v3 project. https://github.com/automl/SMAC3 (2017), version visited last on August 2017
[38] Möhle, S., Manthey, N.: Better evaluations by analyzing benchmark structure, pp. 1-10 (2016). http://www.pragmaticsofsat.org/2016/reg/POS-16_paper_4.pdf
[39] Nadel, A.; Ryvchin, V.; Beyersdorff, O.; Wintersteiger, CM, Chronological backtracking, Theory and Applications of Satisfiability Testing - SAT 2018, 111-121 (2018), Cham: Springer, Cham · Zbl 1442.68219
[40] Nethercote, N., Seward, J.: Valgrind: A framework for heavyweight dynamic binary instrumentation. SIGPLAN Not. 42(6), 89-100 (2007). doi:10.1145/1273442.1250746
[41] Oh, C.; Heule, M.; Weaver, S., Between SAT and UNSAT: the fundamental difference in CDCL SAT, Theory and Applications of Satisfiability Testing - SAT 2015, 307-323 (2015), Cham: Springer, Cham · Zbl 1471.68260
[42] Ryvchin, V., Nadel, A.: Maple \(\_\) LCM \(\_\) Dist \(\_\) ChronoBT: featuring chronological backtracking. In: Proceedings of SAT Competition 2018 (2018). http://hdl.handle.net/10138/237063 · Zbl 1442.68219
[43] Soos, M.; Nohl, K.; Castelluccia, C.; Kullmann, O., Extending SAT solvers to cryptographic problems, Theory and Applications of Satisfiability Testing - SAT 2009, 244-257 (2009), Heidelberg: Springer, Heidelberg
[44] Kochemazov, S., Oleg Zaikin, V.K., Semenov, A.: Maplelcmdistchronobt-dl, duplicate learnts heuristic-aided solvers at the sat race 2019 (2019)
[45] van der Tak, P.; Ramos, A.; Heule, M., Reusing the assignment trail in cdcl solvers, JSAT, 7, 4, 133-138 (2011) · Zbl 1331.68214
[46] Zhang, X., Cai, S.: Relaxed backtracking with rephasing. In: Balyo, T., Froleyks, N., Heule, M., Iser, M., Järvisalo, M., Suda, M. (eds.) Proceedings of SAT Competition 2020 - Solver and Benchmark Descriptions. Department of Computer Science Report Series B, vol. B-2020-1, pp. 15-15. University of Helsinki (2020)
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.