×

SAT competition 2020. (English) Zbl 1478.68320

Summary: The SAT Competitions constitute a well-established series of yearly open international algorithm implementation competitions, focusing on the Boolean satisfiability (or propositional satisfiability, SAT) problem. In this article, we provide a detailed account on the 2020 instantiation of the SAT Competition, including the new competition tracks and benchmark selection procedures, overview of solving strategies implemented in top-performing solvers, and a detailed analysis of the empirical data obtained from running the competition.

MSC:

68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
68R07 Computational aspects of satisfiability
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] (Biere, A.; Heule, M.; van Maaren, H.; Walsh, T., Handbook of Satisfiability. Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol. 336 (2021), IOS Press) · Zbl 1456.68001
[2] Simon, L.; Le Berre, D.; Hirsch, E. A., The SAT2002 Competition, Ann. Math. Artif. Intell., 43, 1, 307-342 (2005)
[3] Le Berre, D.; Simon, L., The essentials of the SAT 2003 Competition, (Giunchiglia, E.; Tacchella, A., Theory and Applications of Satisfiability Testing, 6th International Conference, SAT 2003. Santa Margherita Ligure, Italy, May 5-8, 2003 Selected Revised Papers. Theory and Applications of Satisfiability Testing, 6th International Conference, SAT 2003. Santa Margherita Ligure, Italy, May 5-8, 2003 Selected Revised Papers, Lecture Notes in Computer Science, vol. 2919 (2004), Springer), 452-467 · Zbl 1204.68203
[4] Le Berre, D.; Simon, L., Fifty-five solvers in Vancouver: the SAT 2004 Competition, (Hoos, H. H.; Mitchell, D. G., Theory and Applications of Satisfiability Testing, 7th International Conference, SAT 2004, Vancouver, BC, Canada, May 10-13, 2004, Revised Selected Papers. Theory and Applications of Satisfiability Testing, 7th International Conference, SAT 2004, Vancouver, BC, Canada, May 10-13, 2004, Revised Selected Papers, Lecture Notes in Computer Science, vol. 3542 (2005), Springer), 321-344 · Zbl 1122.68609
[5] Järvisalo, M.; Le Berre, D.; Roussel, O.; Simon, L., The international SAT solver competitions, AI Mag., 33, 1, 89-92 (2012)
[6] Balint, A.; Belov, A.; Järvisalo, M.; Sinz, C., Overview and analysis of the SAT Challenge 2012 solver competition, Artif. Intell., 223, 120-155 (2015)
[7] Balyo, T.; Heule, M. J.H.; Järvisalo, M.; Competition, S. A.T., Recent developments, (Singh, S. P.; Markovitch, S., Proceedings of the Thirty-First AAAI Conference on Artificial Intelligence. Proceedings of the Thirty-First AAAI Conference on Artificial Intelligence, February 4-9, 2017, San Francisco, California, USA (2017), AAAI Press), 5061-5063
[8] Heule, M. J.H.; Järvisalo, M.; Suda, M., SAT Competition 2018, J. Satisf. Boolean Model. Comput., 11, 1, 133-154 (2019)
[9] (Balyo, T.; Froleyks, N.; Heule, M. J.H.; Iser, M.; Järvisalo, M.; Suda, M., Proceedings of SAT Competition 2020; Solver and Benchmark Descriptions. Proceedings of SAT Competition 2020; Solver and Benchmark Descriptions, Department of Computer Science Report Series B, vol. B-2020-1 (2020), Department of Computer Science, University of Helsinki) · Zbl 1478.68320
[10] Kautz, H. A.; Selman, B., Planning as satisfiability, (Neumann, B., 10th European Conference on Artificial Intelligence, ECAI 92, Vienna, Austria, August 3-7, 1992. Proceedings (1992), John Wiley and Sons), 359-363
[11] Audemard, G.; Simon, L., On the glucose SAT solver, Int. J. Artif. Intell. Tools, 27, 1, 1-25 (2018)
[12] Balyo, T.; Biere, A.; Iser, M.; Sinz, C., SAT Race 2015, Artif. Intell., 241, 45-65 (2016) · Zbl 1392.68381
[13] Eén, N.; Sörensson, N., Temporal induction by incremental SAT solving, Electron. Notes Theor. Comput. Sci., 89, 4, 543-560 (2003) · Zbl 1271.68215
[14] Nadel, A.; Ryvchin, V.; Strichman, O., Ultimately incremental SAT, (Sinz, C.; Egly, U., Theory and Applications of Satisfiability Testing - SAT 2014 - 17th International Conference, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings. Theory and Applications of Satisfiability Testing - SAT 2014 - 17th International Conference, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings, Lecture Notes in Computer Science, vol. 8561 (2014), Springer), 206-218 · Zbl 1423.68464
[15] Fazekas, K.; Biere, A.; Scholl, C., Incremental inprocessing in SAT solving, (Janota, M.; Lynce, I., Theory and Applications of Satisfiability Testing - SAT 2019 - 22nd International Conference, SAT 2019, Lisbon, Portugal, July 9-12, 2019, Proceedings. Theory and Applications of Satisfiability Testing - SAT 2019 - 22nd International Conference, SAT 2019, Lisbon, Portugal, July 9-12, 2019, Proceedings, Lecture Notes in Computer Science, vol. 11628 (2019), Springer), 136-154 · Zbl 1441.68224
[16] Gupta, A.; Strichman, O., Abstraction refinement for bounded model checking, (Etessami, K.; Rajamani, S. K., Computer Aided Verification, 17th International Conference, CAV 2005, Edinburgh, Scotland, UK, July 6-10, 2005, Proceedings. Computer Aided Verification, 17th International Conference, CAV 2005, Edinburgh, Scotland, UK, July 6-10, 2005, Proceedings, Lecture Notes in Computer Science, vol. 3576 (2005), Springer), 112-124 · Zbl 1081.68620
[17] Gocht, S.; Balyo, T., Accelerating SAT based planning with incremental SAT solving, (Barbulescu, L.; Frank Mausam, J.; Smith, S. F., Proceedings of the Twenty-Seventh International Conference on Automated Planning and Scheduling. Proceedings of the Twenty-Seventh International Conference on Automated Planning and Scheduling, ICAPS 2017, Pittsburgh, Pennsylvania, USA, June 18-23, 2017 (2017), AAAI Press), 135-139
[18] Surynek, P., Unifying search-based and compilation-based approaches to multi-agent path finding through satisfiability modulo theories, (Kraus, S., Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence. Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence, IJCAI 2019, Macao, China, August 10-16, 2019, ijcai.org (2019)), 1177-1183
[19] Brummayer, R.; Biere, A., Boolector: an efficient SMT solver for bit-vectors and arrays, (Tools and Algorithms for the Construction and Analysis of Systems, 15th International Conference, TACAS 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 22-29, 2009. Proceedings. Tools and Algorithms for the Construction and Analysis of Systems, 15th International Conference, TACAS 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 22-29, 2009. Proceedings, Lecture Notes in Computer Science, vol. 5505 (2009), Springer), 174-177
[20] Wetzler, N.; Heule, M.; Hunt, W. A.J., DRAT-trim: efficient checking and trimming using expressive clausal proofs, (Sinz, C.; Egly, U., Theory and Applications of Satisfiability Testing - SAT 2014 - 17th International Conference, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings. Theory and Applications of Satisfiability Testing - SAT 2014 - 17th International Conference, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings, Lecture Notes in Computer Science, vol. 8561 (2014), Springer), 422-429 · Zbl 1423.68475
[21] Balyo, T.; Froleyks, N.; Heule, M. J.H.; Iser, M.; Järvisalo, M.; Suda, M., SAT Competition 2020 (2020)
[22] Tan, Y. K., Cake_lpr on Github (2020)
[23] Stump, A.; Sutcliffe, G.; Tinelli, C., StarExec, a cross community logic solving service (2012)
[24] Iser, M.; Sinz, C., A problem meta-data library for research in SAT, (Le Berre, D.; Järvisalo, M., Proceedings of Pragmatics of SAT 2015, Austin, Texas, USA, September 23, 2015 / Pragmatics of SAT 2018, Oxford, UK, July 7, 2018. Proceedings of Pragmatics of SAT 2015, Austin, Texas, USA, September 23, 2015 / Pragmatics of SAT 2018, Oxford, UK, July 7, 2018, EPiC Series in Computing, vol. 59 (2019), EasyChair), 144-152
[25] (Balyo, T.; Heule, M. J.; Järvisalo, M., Proceedings of SAT Competition 2017: Solver and Benchmark Descriptions. Proceedings of SAT Competition 2017: Solver and Benchmark Descriptions, Department of Computer Science Report Series B, vol. B-2017-1 (2017), Department of Computer Science, University of Helsinki)
[26] Rintanen, J.; Heljanko, K.; Niemelä, I., Planning as satisfiability: parallel plans and algorithms for plan search, Artif. Intell., 170, 12-13, 1031-1080 (2006) · Zbl 1131.68099
[27] Wehrle, M.; Rintanen, J., Planning as satisfiability with relaxed exist-step plans, (Orgun, M. A.; Thornton, J., AI 2007: Advances in Artificial Intelligence, 20th Australian Joint Conference on Artificial Intelligence, Gold Coast, Australia, December 2-6, 2007, Proceedings. AI 2007: Advances in Artificial Intelligence, 20th Australian Joint Conference on Artificial Intelligence, Gold Coast, Australia, December 2-6, 2007, Proceedings, Lecture Notes in Computer Science, vol. 4830 (2007), Springer), 244-253
[28] Balyo, T., Relaxing the relaxed exist-step parallel planning semantics, (2013 IEEE 25th International Conference on Tools with Artificial Intelligence (2013), IEEE Computer Society), 865-871
[29] Rintanen, J., Madagascar: scalable planning with SAT, (Proceedings of the 8th International Planning Competition. Proceedings of the 8th International Planning Competition, IPC-2014 (2014)), 1-5
[30] Froleyks, N. C.; Balyo, T.; Schreiber, D., PASAR-planning as satisfiability with abstraction refinement, (Surynek, P.; Yeoh, W., Proceedings of the Twelfth International Symposium on Combinatorial Search. Proceedings of the Twelfth International Symposium on Combinatorial Search, SOCS 2019, Napa, California, 16-17 July 2019 (2019), AAAI Press), 70-78
[31] Helmert, M., The Fast Downward planning system, J. Artif. Intell. Res., 26, 191-246 (2006) · Zbl 1182.68245
[32] Schreiber, D.; Pellier, D.; Fiorino, H., Tree-REX: SAT-based tree exploration for efficient and high-quality HTN planning, (Benton, J.; Lipovetzky, N.; Onaindia, E.; Smith, D. E.; Srivastava, S., Proceedings of the Twenty-Ninth International Conference on Automated Planning and Scheduling. Proceedings of the Twenty-Ninth International Conference on Automated Planning and Scheduling, ICAPS 2018, Berkeley, CA, USA, July 11-15, 2019 (2019), AAAI Press), 382-390
[33] Monasson, R.; Zecchina, R.; Kirkpatrick, S.; Selman, B.; Troyansky, L., Determining computational complexity from characteristic ‘phase transitions’, Nature, 400, 133-137 (1999) · Zbl 1369.68244
[34] Janota, M.; Lynce, I.; Marques-Silva, J., Algorithms for computing backbones of propositional formulae, AI Commun., 28, 2, 161-177 (2015) · Zbl 1373.68379
[35] Bryant, R. E., Boolean analysis of MOS circuits, IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst., 6, 4, 634-649 (1987)
[36] Fieger, K.; Balyo, T.; Schulz, C.; Schreiber, D., Finding optimal longest paths by dynamic programming in parallel, (Surynek, P.; Yeoh, W., Proceedings of the Twelfth International Symposium on Combinatorial Search. Proceedings of the Twelfth International Symposium on Combinatorial Search, SOCS 2019, Napa, California, 16-17 July 2019 (2019), AAAI Press), 61-69
[37] Philipp, T.; Steinke, P., PBLib – a library for encoding pseudo-Boolean constraints into CNF, (Heule, M.; Weaver, S. A., Theory and Applications of Satisfiability Testing - SAT 2015 - 18th International Conference, Austin, TX, USA, September 24-27, 2015, Proceedings. Theory and Applications of Satisfiability Testing - SAT 2015 - 18th International Conference, Austin, TX, USA, September 24-27, 2015, Proceedings, Lecture Notes in Computer Science, vol. 9340 (2015), Springer), 9-16 · Zbl 1471.68261
[38] Bloem, R.; Braud-Santoni, N.; Hadzic, V.; Egly, U.; Lonsing, F.; Seidl, M., Expansion-based QBF solving without recursion, (Bjørner, N.; Gurfinkel, A., 2018 Formal Methods in Computer Aided Design. 2018 Formal Methods in Computer Aided Design, FMCAD 2018, Austin, TX, USA, October 30 - November 2, 2018 (2018), IEEE), 1-10
[39] Ryan, L., Efficient algorithms for clause-learning SAT solvers (2004), Simon Fraser University, Master’s thesis
[40] Eén, N.; Sörensson, N., An extensible sat-solver, (Giunchiglia, E.; Tacchella, A., Theory and Applications of Satisfiability Testing, 6th International Conference, SAT 2003. Santa Margherita Ligure, Italy, May 5-8, 2003 Selected Revised Papers. Theory and Applications of Satisfiability Testing, 6th International Conference, SAT 2003. Santa Margherita Ligure, Italy, May 5-8, 2003 Selected Revised Papers, Lecture Notes in Computer Science, vol. 2919 (2004), Springer), 502-518 · Zbl 1204.68191
[41] Audemard, G.; Simon, L., Predicting learnt clauses quality in modern SAT solvers, (Boutilier, C., IJCAI 2009, Proceedings of the 21st International Joint Conference on Artificial Intelligence. IJCAI 2009, Proceedings of the 21st International Joint Conference on Artificial Intelligence, Pasadena, California, USA, July 11-17, 2009 (2009)), 399-404
[42] Manthey, N., Coprocessor 2.0 - a flexible CNF simplifier - (tool presentation), (Cimatti, A.; Sebastiani, R., Theory and Applications of Satisfiability Testing - SAT 2012 - 15th International Conference, Trento, Italy, June 17-20, 2012. Proceedings. Theory and Applications of Satisfiability Testing - SAT 2012 - 15th International Conference, Trento, Italy, June 17-20, 2012. Proceedings, Lecture Notes in Computer Science, vol. 7317 (2012), Springer), 436-441
[43] Oh, C., Between SAT and UNSAT: the fundamental difference in CDCL SAT, (Heule, M.; Weaver, S. A., Theory and Applications of Satisfiability Testing - SAT 2015 - 18th International Conference, Austin, TX, USA, September 24-27, 2015, Proceedings. Theory and Applications of Satisfiability Testing - SAT 2015 - 18th International Conference, Austin, TX, USA, September 24-27, 2015, Proceedings, Lecture Notes in Computer Science, vol. 9340 (2015), Springer), 307-323 · Zbl 1471.68260
[44] Liang, J. H.; Ganesh, V.; Poupart, P.; Czarnecki, K., Learning rate based branching heuristic for SAT solvers, (Creignou, N.; Le Berre, D., Theory and Applications of Satisfiability Testing - SAT 2016 - 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings. Theory and Applications of Satisfiability Testing - SAT 2016 - 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings, Lecture Notes in Computer Science, vol. 9710 (2016), Springer), 123-140 · Zbl 1475.68348
[45] Zhang, L.; Madigan, C. F.; Moskewicz, M. W.; Malik, S., Efficient conflict driven learning in Boolean satisfiability solver, (Ernst, R., Proceedings of the 2001 IEEE/ACM International Conference on Computer-Aided Design. Proceedings of the 2001 IEEE/ACM International Conference on Computer-Aided Design, ICCAD 2001, San Jose, CA, USA, November 4-8, 2001 (2001), IEEE Computer Society), 279-285
[46] Liang, J. H.; Oh, C.; Ganesh, V.; Czarnecki, K.; Poupart, P., (Balyo, T.; Heule, M. J.H.; Järvisalo, M., Proceedings of SAT Competition 2016: Solver and Benchmark Descriptions. Proceedings of SAT Competition 2016: Solver and Benchmark Descriptions, Department of Computer Science Report Series B, vol. B-2016-1 (2016), Department of Computer Science, University of Helsinki), 52-53
[47] Luo, M.; Li, C.; Xiao, F.; Manyà, F.; Lü, Z., An effective learnt clause minimization approach for CDCL SAT solvers, (Sierra, C., Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence. Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence, IJCAI 2017, Melbourne, Australia, August 19-25, 2017, ijcai.org (2017)), 703-711
[48] Xiao, F.; Luo, M.; Li, C.-M.; Manyà, F.; Lü, Z., MapleLRB LCM, Maple LCM, Maple LCM Dist, MapleLRB LCMoccRestart and Glucose-3.0+width in SAT Competition 2017, (Balyo, T.; Heule, M. J.H.; Järvisalo, M., Proceedings of SAT Competition 2017: Solver and Benchmark Descriptions. Proceedings of SAT Competition 2017: Solver and Benchmark Descriptions, Department of Computer Science Report Series B, vol. B-2017-1 (2017), Department of Computer Science, University of Helsinki), 20-21
[49] Nadel, A.; Ryvchin, V., Chronological backtracking, (Beyersdorff, O.; Wintersteiger, C. M., Theory and Applications of Satisfiability Testing - SAT 2018 - 21st International Conference, SAT 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9-12, 2018, Proceedings. Theory and Applications of Satisfiability Testing - SAT 2018 - 21st International Conference, SAT 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9-12, 2018, Proceedings, Lecture Notes in Computer Science, vol. 10929 (2018), Springer), 111-121 · Zbl 1442.68219
[50] Ryvchin, V.; Nadel, A., Maple_LCM_Dist_ChronoBT: featuring chronological backtracking, (Heule, M. J.H.; Järvisalo, M.; Suda, M., Proceedings of SAT Competition 2018: Solver and Benchmark Descriptions. Proceedings of SAT Competition 2018: Solver and Benchmark Descriptions, Department of Computer Science Report Series B, vol. B-2018-1 (2018), Department of Computer Science, University of Helsinki), 29
[51] Kochemazov, S.; Zaikin, O.; Kondratiev, V.; Semenov, A., MapleLCMDistChronoBT-DL, duplicate learnts heuristic-aided solvers at the SAT Race 2019, (Heule, M. J.H.; Järvisalo, M.; Suda, M., Proceedings of SAT Race 2019: Solver and Benchmark Descriptions. Proceedings of SAT Race 2019: Solver and Benchmark Descriptions, Department of Computer Science Report Series B, vol. B-2019-1 (2019), Department of Computer Science, University of Helsinki), 24
[52] Soos, M.; Nohl, K.; Castelluccia, C., Extending SAT solvers to cryptographic problems, (Kullmann, O., Theory and Applications of Satisfiability Testing - SAT 2009, 12th International Conference, SAT 2009, Swansea, UK, June 30 - July 3, 2009. Proceedings. Theory and Applications of Satisfiability Testing - SAT 2009, 12th International Conference, SAT 2009, Swansea, UK, June 30 - July 3, 2009. Proceedings, Lecture Notes in Computer Science, vol. 5584 (2009), Springer), 244-257
[53] Soos, M.; Kulkarni, R.; Meel, K. S., Crystalball: gazing in the black box of SAT solving, (Janota, M.; Lynce, I., Theory and Applications of Satisfiability Testing - SAT 2019 - 22nd International Conference, SAT 2019, Lisbon, Portugal, July 9-12, 2019, Proceedings. Theory and Applications of Satisfiability Testing - SAT 2019 - 22nd International Conference, SAT 2019, Lisbon, Portugal, July 9-12, 2019, Proceedings, Lecture Notes in Computer Science, vol. 11628 (2019)), 371-387 · Zbl 1441.68240
[54] Biere, A., LINGELING and friends entering the SAT Challenge 2012, (Balint, A.; Belov, A.; Diepold, D.; Gerber, S.; Järvisalo, M.; Sinz, C., Proceedings of SAT Challenge 2012: Solver and Benchmark Descriptions. Proceedings of SAT Challenge 2012: Solver and Benchmark Descriptions, Department of Computer Science Report Series B, vol. B-2012-1 (2012)), 33
[55] Biere, A.; Fazekas, K.; Fleury, M.; Heisinger, M., CaDiCaL, Kissat, Paracooba, Plingeling and Treengeling entering the SAT Competition 2020, (Balyo, T.; Froleyks, N.; Heule, M. J.H.; Iser, M.; Järvisalo, M.; Suda, M., Proceedings of SAT Competition 2020; Solver and Benchmark Descriptions. Proceedings of SAT Competition 2020; Solver and Benchmark Descriptions, Department of Computer Science Report Series B, vol. B-2020-1 (2020), Department of Computer Science, University of Helsinki), 50-53
[56] Biere, A., CaDiCaL at the SAT Race 2019, (Heule, M. J.H.; Järvisalo, M.; Suda, M., Proceedings of SAT Race 2019: Solver and Benchmark Descriptions. Proceedings of SAT Race 2019: Solver and Benchmark Descriptions, Department of Computer Science Report Series B, vol. B-2019-1 (2019), Department of Computer Science, University of Helsinki), 8-9
[57] Li, C.; Xiao, F.; Luo, M.; Manyà, F.; Lü, Z.; Li, Y., Clause vivification by unit propagation in CDCL SAT solvers, Artif. Intell., 279, Article 103197 pp. (2020) · Zbl 1478.68325
[58] Kiesl, B.; Heule, M. J.H.; Biere, A., Truth assignments as conditional autarkies, (Chen, Y.; Cheng, C.; Esparza, J., Automated Technology for Verification and Analysis - 17th International Symposium, ATVA 2019, Taipei, Taiwan, October 28-31, 2019, Proceedings. Automated Technology for Verification and Analysis - 17th International Symposium, ATVA 2019, Taipei, Taiwan, October 28-31, 2019, Proceedings, Lecture Notes in Computer Science, vol. 11781 (2019), Springer), 48-64 · Zbl 1437.68132
[59] Shaw, A.; Meel, K. S., Designing new phase selection heuristics, (Pulina, L.; Seidl, M., Theory and Applications of Satisfiability Testing - SAT 2020 - 23rd International Conference, Alghero, Italy, July 3-10, 2020, Proceedings. Theory and Applications of Satisfiability Testing - SAT 2020 - 23rd International Conference, Alghero, Italy, July 3-10, 2020, Proceedings, Lecture Notes in Computer Science, vol. 12178 (2020), Springer), 72-88 · Zbl 07331013
[60] Soos, M.; Cai, S.; Deviendt, J.; Gocht, S.; Shaw, A.; Meel, K. S., CryptoMiniSat with CCAnr at the SAT Competition 2020, (Balyo, T.; Froleyks, N.; Heule, M. J.H.; Iser, M.; Järvisalo, M.; Suda, M., Proceedings of SAT Competition 2020; Solver and Benchmark Descriptions. Proceedings of SAT Competition 2020; Solver and Benchmark Descriptions, Department of Computer Science Report Series B, vol. B-2020-1 (2020), Department of Computer Science, University of Helsinki), 27-28
[61] Soos, M.; Gocht, S.; Meel, K. S., Tinted, detached, and lazy CNF-XOR solving and its applications to counting and sampling, (Lahiri, S. K.; Wang, C., Computer Aided Verification - 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part I. Computer Aided Verification - 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part I, Lecture Notes in Computer Science, vol. 12224 (2020), Springer), 463-484 · Zbl 1478.68203
[62] Devriendt, J.; Bogaerts, B.; Bruynooghe, M.; Denecker, M., Improved static symmetry breaking for SAT, (Creignou, N.; Le Berre, D., Theory and Applications of Satisfiability Testing - SAT 2016 - 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings. Theory and Applications of Satisfiability Testing - SAT 2016 - 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings, Lecture Notes in Computer Science, vol. 9710 (2016), Springer), 104-122 · Zbl 1475.68340
[63] Hickey, R.; Bacchus, F., Trail saving on backtrack, (Pulina, L.; Seidl, M., Theory and Applications of Satisfiability Testing - SAT 2020 - 23rd International Conference, Alghero, Italy, July 3-10, 2020, Proceedings. Theory and Applications of Satisfiability Testing - SAT 2020 - 23rd International Conference, Alghero, Italy, July 3-10, 2020, Proceedings, Lecture Notes in Computer Science, vol. 12178 (2020), Springer), 46-61 · Zbl 07331011
[64] Hickey, R.; Feng, N.; Bacchus, F., Cadical-trail, Cadical-alluip, Cadical-alluip-trail, and Maple-LCM-Dist-alluip-trail at the SAT Competition 2020, (Balyo, T.; Froleyks, N.; Heule, M. J.H.; Iser, M.; Järvisalo, M.; Suda, M., Proceedings of SAT Competition 2020; Solver and Benchmark Descriptions. Proceedings of SAT Competition 2020; Solver and Benchmark Descriptions, Department of Computer Science Report Series B, vol. B-2020-1 (2020), Department of Computer Science, University of Helsinki), 10
[65] Zhang, X.; Cai, S., Four relaxed CDCL solvers, (Heule, M. J.H.; Järvisalo, M.; Suda, M., Proceedings of SAT Race 2019: Solver and Benchmark Descriptions. Proceedings of SAT Race 2019: Solver and Benchmark Descriptions, Department of Computer Science Report Series B, vol. B-2019-1 (2019), Department of Computer Science, University of Helsinki), 35-36
[66] Zhang, X.; Cai, S., Relaxed backtracking with rephasing, (Balyo, T.; Froleyks, N.; Heule, M. J.H.; Iser, M.; Järvisalo, M.; Suda, M., Proceedings of SAT Competition 2020; Solver and Benchmark Descriptions. Proceedings of SAT Competition 2020; Solver and Benchmark Descriptions, Department of Computer Science Report Series B, vol. B-2020-1 (2020), Department of Computer Science, University of Helsinki), 15-16
[67] Kochemazov, S., F2TRC: deterministic modifications of SC2018-SR2019 winners, (Balyo, T.; Froleyks, N.; Heule, M. J.H.; Iser, M.; Järvisalo, M.; Suda, M., Proceedings of SAT Competition 2020; Solver and Benchmark Descriptions. Proceedings of SAT Competition 2020; Solver and Benchmark Descriptions, Department of Computer Science Report Series B, vol. B-2020-1 (2020), Department of Computer Science, University of Helsinki), 21-22
[68] Frioux, L. L.; Baarir, S.; Sopena, J.; Kordon, F., PaInleSS: a framework for parallel SAT solving, (Gaspers, S.; Walsh, T., Theory and Applications of Satisfiability Testing - SAT 2017 - 20th International Conference, Melbourne, VIC, Australia, August 28 - September 1, 2017, Proceedings. Theory and Applications of Satisfiability Testing - SAT 2017 - 20th International Conference, Melbourne, VIC, Australia, August 28 - September 1, 2017, Proceedings, Lecture Notes in Computer Science, vol. 10491 (2017), Springer), 233-250 · Zbl 06807229
[69] Liang, J. H.; Oh, C.; Ganesh, V.; Czarnecki, K.; Poupart, P., MapleCOMSPS LRB VSIDS and MapleCOMSPS CHB VSIDS, (Balyo, T.; Heule, M. J.H.; Järvisalo, M., Proceedings of SAT Competition 2017: Solver and Benchmark Descriptions. Proceedings of SAT Competition 2017: Solver and Benchmark Descriptions, Department of Computer Science Report Series B, vol. B-2017-1 (2017), Department of Computer Science, University of Helsinki), 20-21
[70] Balyo, T.; Sanders, P.; Sinz, C., HordeSat: a massively parallel portfolio SAT solver, (Heule, M.; Weaver, S. A., Theory and Applications of Satisfiability Testing - SAT 2015 - 18th International Conference, Austin, TX, USA, September 24-27, 2015, Proceedings. Theory and Applications of Satisfiability Testing - SAT 2015 - 18th International Conference, Austin, TX, USA, September 24-27, 2015, Proceedings, Lecture Notes in Computer Science, vol. 9340 (2015), Springer), 156-172 · Zbl 1471.68237
[71] Wieringa, S.; Heljanko, K., Concurrent clause strengthening, (Järvisalo, M.; Gelder, A. V., Theory and Applications of Satisfiability Testing - SAT 2013 - 16th International Conference, Helsinki, Finland, July 8-12, 2013. Proceedings. Theory and Applications of Satisfiability Testing - SAT 2013 - 16th International Conference, Helsinki, Finland, July 8-12, 2013. Proceedings, Lecture Notes in Computer Science, vol. 7962 (2013), Springer), 116-132 · Zbl 1390.68586
[72] Audemard, G.; Simon, L., Glucose and syrup: nine years in the SAT Competitions, (Heule, M. J.H.; Järvisalo, M.; Suda, M., Proceedings of SAT Competition 2018: Solver and Benchmark Descriptions. Proceedings of SAT Competition 2018: Solver and Benchmark Descriptions, Department of Computer Science Report Series B, vol. B-2018-1 (2018), Department of Computer Science, University of Helsinki), 24-25
[73] Audemard, G.; Simon, L., Lazy clause exchange policy for parallel SAT solvers, (Sinz, C.; Egly, U., Theory and Applications of Satisfiability Testing - SAT 2014 - 17th International Conference, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings. Theory and Applications of Satisfiability Testing - SAT 2014 - 17th International Conference, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings, Lecture Notes in Computer Science, vol. 8561 (2014)), 197-205 · Zbl 1423.68431
[74] Hamadi, Y.; Jabbour, S.; Sais, L., ManySAT: a parallel SAT solver, J. Satisf. Boolean Model. Comput., 6, 4, 245-262 (2009) · Zbl 1193.68227
[75] Biere, A., CADICAL, LINGELING, PLINGELING, TREENGELING and YALSAT entering the SAT Competition 2018, (Heule, M. J.H.; Järvisalo, M.; Suda, M., Proceedings of SAT Competition 2018: Solver and Benchmark Descriptions. Proceedings of SAT Competition 2018: Solver and Benchmark Descriptions, Department of Computer Science Report Series B, vol. B-2018-1 (2018), Department of Computer Science, University of Helsinki), 13-14
[76] Schreiber, D., Engineering HordeSat towards malleability: mallob-mono in the SAT 2020 cloud track, (Balyo, T.; Froleyks, N.; Heule, M. J.H.; Iser, M.; Järvisalo, M.; Suda, M., Proceedings of SAT Competition 2020; Solver and Benchmark Descriptions. Proceedings of SAT Competition 2020; Solver and Benchmark Descriptions, Department of Computer Science Report Series B, vol. B-2020-1 (2020), Department of Computer Science, University of Helsinki), 45-46
[77] Schreiber, D.; Sanders, P., Scalable SAT solving in the cloud, (Li, C.-M.; Manyà, F., Theory and Applications of Satisfiability Testing - SAT 2021 - 24th International Conference, Barcelona, Spain, July 5-9, 2021, Proceedings. Theory and Applications of Satisfiability Testing - SAT 2021 - 24th International Conference, Barcelona, Spain, July 5-9, 2021, Proceedings, Lecture Notes in Computer Science, vol. 12831 (2021), Springer), 518-534 · Zbl 07495595
[78] Ehlers, T.; Nowotka, D., Tuning parallel SAT solvers, (Le Berre, D.; Järvisalo, M., Proceedings of Pragmatics of SAT 2015, Austin, Texas, USA, September 23, 2015 / Pragmatics of SAT 2018, Oxford, UK, July 7, 2018. Proceedings of Pragmatics of SAT 2015, Austin, Texas, USA, September 23, 2015 / Pragmatics of SAT 2018, Oxford, UK, July 7, 2018, EPiC Series in Computing, vol. 59 (2019), EasyChair), 127-143
[79] Ehlers, T.; Kulczynski, M.; Nowotka, D.; Sieweck, P., TopoSAT 2, (Balyo, T.; Froleyks, N.; Heule, M. J.H.; Iser, M.; Järvisalo, M.; Suda, M., Proceedings of SAT Competition 2020; Solver and Benchmark Descriptions. Proceedings of SAT Competition 2020; Solver and Benchmark Descriptions, Department of Computer Science Report Series B, vol. B-2020-1 (2020), Department of Computer Science, University of Helsinki), 60
[80] Riveros, O., SLIME: a minimal heuristic to boost SAT solving, (Heule, M. J.H.; Järvisalo, M.; Suda, M., Proceedings of SAT Competition 2019: Solver and Benchmark Descriptions. Proceedings of SAT Competition 2019: Solver and Benchmark Descriptions, Department of Computer Science Report Series B, vol. B-2019-1 (2019), Department of Computer Science, University of Helsinki), 38
[81] Riveros, O., SLIME SAT solver, (Balyo, T.; Froleyks, N.; Heule, M. J.H.; Iser, M.; Järvisalo, M.; Suda, M., Proceedings of SAT Competition 2020; Solver and Benchmark Descriptions. Proceedings of SAT Competition 2020; Solver and Benchmark Descriptions, Department of Computer Science Report Series B, vol. B-2020-1 (2020), Department of Computer Science, University of Helsinki), 59
[82] de Moura, L. M.; Bjørner, N., Z3: an efficient SMT solver, (Ramakrishnan, C. R.; Rehof, J., Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings. Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings, Lecture Notes in Computer Science, vol. 4963 (2008), Springer), 337-340 · Zbl 1133.68009
[83] Bjørner, N.; Phan, A., νz - maximal satisfaction with Z3, (Kutsia, T.; Voronkov, A., 6th International Symposium on Symbolic Computation in Software Science. 6th International Symposium on Symbolic Computation in Software Science, SCSS 2014, Gammarth, La Marsa, Tunisia, December 7-8, 2014. 6th International Symposium on Symbolic Computation in Software Science. 6th International Symposium on Symbolic Computation in Software Science, SCSS 2014, Gammarth, La Marsa, Tunisia, December 7-8, 2014, EPiC Series in Computing, vol. 30 (2014), EasyChair), 1-9
[84] Fazekas, K.; Kaufmann, D.; Biere, A., Ranking robustness under sub-sampling for the SAT Competition 2018 (2019), presented at Pragmatics of SAT 2019
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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.