Document Open Access Logo

A Comprehensive Study of k-Portfolios of Recent SAT Solvers

Authors Jakob Bach , Markus Iser , Klemens Böhm

PDF
Thumbnail PDF

File

LIPIcs.SAT.2022.2.pdf
  • Filesize: 0.85 MB
  • 18 pages

Document Identifiers

Author Details

Jakob Bach
  • Karlsruhe Institute of Technology (KIT), Germany
Markus Iser
  • Karlsruhe Institute of Technology (KIT), Germany
Klemens Böhm
  • Karlsruhe Institute of Technology (KIT), Germany

Acknowledgements

We want to thank Luc Mercatoris for his support with preliminary experiments.

Cite AsGet BibTex

Jakob Bach, Markus Iser, and Klemens Böhm. A Comprehensive Study of k-Portfolios of Recent SAT Solvers. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 2:1-2:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.SAT.2022.2

Abstract

Hard combinatorial problems such as propositional satisfiability are ubiquitous. The holy grail are solution methods that show good performance on all problem instances. However, new approaches emerge regularly, some of which are complementary to existing solvers in that they only run faster on some instances but not on many others. While portfolios, i.e., sets of solvers, have been touted as useful, putting together such portfolios also needs to be efficient. In particular, it remains an open question how well portfolios can exploit the complementarity of solvers. This paper features a comprehensive analysis of portfolios of recent SAT solvers, the ones from the SAT Competitions 2020 and 2021. We determine optimal portfolios with exact and approximate approaches and study the impact of portfolio size k on performance. We also investigate how effective off-the-shelf prediction models are for instance-specific solver recommendations. One result is that the portfolios found with an approximate approach are as good as the optimal solution in practice. We also observe that marginal returns decrease very quickly with larger k, and our prediction models do not give way to better performance beyond very small portfolio sizes.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Computing methodologies → Supervised learning
  • Theory of computation → Integer programming
Keywords
  • Propositional satisfiability
  • solver portfolios
  • runtime prediction
  • machine learning
  • integer programming

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. Roberto Amadini, Maurizio Gabbrielli, and Jacopo Mauro. An empirical evaluation of portfolios approaches for solving CSPs. In Proc. CPAIOR, pages 316-324, 2013. URL: https://doi.org/10.1007/978-3-642-38171-3_21.
  2. Roberto Amadini, Maurizio Gabbrielli, and Jacopo Mauro. An extensive evaluation of portfolio approaches for constraint satisfaction problems. Int. J. Interact. Multim. Artif. Intell., 3(7):81-86, 2016. URL: https://doi.org/10.9781/ijimai.2016.3712.
  3. Carlos Ansótegui, Maria Luisa Bonet, Jesús Giráldez-Cru, and Jordi Levy. Structure features for SAT instances classification. J. Appl. Log., 23:27-39, 2017. URL: https://doi.org/10.1016/j.jal.2016.11.004.
  4. Carlos Ansótegui, Maria Luisa Bonet, Jesús Giráldez-Cru, Jordi Levy, and Laurent Simon. Community structure in industrial SAT instances. J. Artif. Intell. Res., 66:443-472, 2019. URL: https://doi.org/10.1613/jair.1.11741.
  5. Carlos Ansótegui, Maria Luisa Bonet, and Jordi Levy. On the structure of industrial SAT instances. In Proc. CP, pages 127-141, 2009. URL: https://doi.org/10.1007/978-3-642-04244-7_13.
  6. Tomáš Balyo, Nils Froleyks, Marijn J. H. Heule, Markus Iser, Matti Järvisalo, and Martin Suda, editors. Proceedings of SAT Competition 2020: Solver and Benchmark Descriptions. Department of Computer Science, University of Helsinki, 2020. URL: http://hdl.handle.net/10138/318754.
  7. Tomáš Balyo, Nils Froleyks, Marijn J. H. Heule, Markus Iser, Matti Järvisalo, and Martin Suda, editors. Proceedings of SAT Competition 2021: Solver and Benchmark Descriptions. Department of Computer Science, University of Helsinki, 2021. URL: http://hdl.handle.net/10138/333647.
  8. André Biedenkapp, Joshua Marben, Marius Lindauer, and Frank Hutter. CAVE: Configuration assessment, visualization and evaluation. In Proc. LION, pages 115-130, 2018. URL: https://doi.org/10.1007/978-3-030-05348-2_10.
  9. Leo Breiman. Random forests. Mach. Learn., 45(1):5-32, 2001. URL: https://doi.org/10.1023/A:1010933404324.
  10. Marko Kleine Büning, Carsten Sinz, and David Faragó. QPR Verify: A static analysis tool for embedded software based on bounded model checking. In Proc. VSTTE, pages 21-32, 2020. URL: https://doi.org/10.1007/978-3-030-63618-0_2.
  11. Tom Carchrae and J. Christopher Beck. Applying machine learning to low-knowledge control of optimization algorithms. Comput. Intell., 21(4):372-387, 2005. URL: https://doi.org/10.1111/j.1467-8640.2005.00278.x.
  12. Tianqi Chen and Carlos Guestrin. XGBoost: A scalable tree boosting system. In Proc. KDD, pages 785-794, 2016. URL: https://doi.org/10.1145/2939672.2939785.
  13. Marco Collautti, Yuri Malitsky, Deepak Mehta, and Barry O'Sullivan. SNNAP: solver-based nearest neighbor for algorithm portfolios. In Proc. ECML PKDD, pages 435-450, 2013. URL: https://doi.org/10.1007/978-3-642-40994-3_28.
  14. Mathias Fleury and Armin Biere. Efficient all-UIP learned clause minimization. In Proc. SAT, pages 171-187, 2021. URL: https://doi.org/10.1007/978-3-030-80223-3_12.
  15. Alexandre Fréchette, Lars Kotthoff, Tomasz Michalak, Talal Rahwan, Holger Hoos, and Kevin Leyton-Brown. Using the shapley value to analyze algorithm portfolios. In Proc. AAAI, pages 3397-3403, 2016. URL: https://ojs.aaai.org/index.php/AAAI/article/view/10440.
  16. Nils Froleyks, Marijn Heule, Markus Iser, Matti Järvisalo, and Martin Suda. SAT Competition 2020. Artif. Intell., 301, 2021. URL: https://doi.org/10.1016/j.artint.2021.103572.
  17. Carla P. Gomes and Bart Selman. Algorithm portfolios. Artif. Intell., 126(1-2):43-62, 2001. URL: https://doi.org/10.1016/S0004-3702(00)00081-3.
  18. Jan Gorodkin. Comparing two k-category assignments by a k-category correlation coefficient. Comput. Biol. Chem., 28(5-6):367-374, 2004. URL: https://doi.org/10.1016/j.compbiolchem.2004.09.006.
  19. Youssef Hamadi, Said Jabbour, and Lakhdar Sais. ManySAT: a parallel SAT solver. J. Satisf. Boolean Model. Comput., 6(4):245-262, 2009. URL: https://doi.org/10.3233/SAT190070.
  20. Marijn J. H. Heule. Schur number five. In Proc. AAAI, pages 6598-6606, 2018. URL: https://ojs.aaai.org/index.php/AAAI/article/view/12209.
  21. Marijn J. H. Heule, Oliver Kullmann, and Victor W. Marek. Solving and verifying the boolean pythagorean triples problem via cube-and-conquer. In Proc. SAT, pages 228-245, 2016. URL: https://doi.org/10.1007/978-3-319-40970-2_15.
  22. Markus Iser, Luca Springer, and Carsten Sinz. Collaborative management of benchmark instances and their attributes. arXiv preprint arXiv:2009.02995, 2020. URL: https://arxiv.org/abs/2009.02995.
  23. Mikoláš Janota, Goetz Botterweck, and João Marques-Silva. On lazy and eager interactive reconfiguration. In Proc. VaMoS, pages 8:1-8:8, 2014. URL: https://doi.org/10.1145/2556624.2556644.
  24. Matti Järvisalo, Daniel Le Berre, Olivier Roussel, and Laurent Simon. The international SAT solver competitions. AI Mag., 33(1):89-92, 2012. URL: https://doi.org/10.1609/aimag.v33i1.2395.
  25. Serdar Kadioglu, Yuri Malitsky, Meinolf Sellmann, and Kevin Tierney. ISAC - instance-specific algorithm configuration. In Proc. ECAI, pages 751-756, 2010. URL: https://doi.org/10.3233/978-1-60750-606-5-751.
  26. Daniela Kaufmann and Armin Biere. AMulet 2.0 for verifying multiplier circuits. In Proc. TACAS, pages 357-364, 2021. URL: https://doi.org/10.1007/978-3-030-72013-1_19.
  27. Pascal Kerschke, Holger H. Hoos, Frank Neumann, and Heike Trautmann. Automated algorithm selection: Survey and perspectives. Evol. Comput., 27(1):3-45, 2019. URL: https://doi.org/10.1162/evco_a_00242.
  28. Andreas Krause and Daniel Golovin. Submodular Function Maximization, pages 71-104. Cambridge University Press, 2014. URL: https://doi.org/10.1017/CBO9781139177801.004.
  29. Chunxiao Li, Jonathan Chung, Soham Mukherjee, Marc Vinyals, Noah Fleming, Antonina Kolokolova, Alice Mu, and Vijay Ganesh. On the hierarchical community structure of practical SAT formulas. In Proc. SAT, 2021. URL: https://doi.org/10.1007/978-3-030-80223-3_25.
  30. Marius Lindauer, Holger H. Hoos, Frank Hutter, and Torsten Schaub. AutoFolio: An automatically configured algorithm selector. J. Artif. Intell. Res., 53:745-778, 2015. URL: https://doi.org/10.1613/jair.4726.
  31. Yuri Malitsky, Ashish Sabharwal, Horst Samulowitz, and Meinolf Sellmann. Non-model-based algorithm portfolios for SAT. In Proc. SAT, pages 369-370, 2011. URL: https://doi.org/10.1007/978-3-642-21581-0_33.
  32. Brian W. Matthews. Comparison of the predicted and observed secondary structure of T4 phage lysozyme. Biochim. Biophys. Acta - Protein Struct., 405(2):442-451, 1975. URL: https://doi.org/10.1016/0005-2795(75)90109-9.
  33. Saeed Nejati. CDCL(Crypto) and Machine Learning based SAT Solvers for Cryptanalysis. PhD thesis, University of Waterloo, Ontario, Canada, 2020. URL: http://hdl.handle.net/10012/15868.
  34. George L. Nemhauser, Laurence A. Wolsey, and Marshall L. Fisher. An analysis of approximations for maximizing submodular set functions - I. Math. Program., 14(1):265-294, 1978. URL: https://doi.org/10.1007/BF01588971.
  35. Mladen Nikolić, Filip Marić, and Predrag Janičić. Simple algorithm portfolio for SAT. Artif. Intell. Rev., 40(4):457-465, 2013. URL: https://doi.org/10.1007/s10462-011-9290-2.
  36. Yair Nof and Ofer Strichman. Real-time solving of computationally hard problems using optimal algorithm portfolios. Ann. Math. Artif. Intell., pages 1-18, 2021. URL: https://doi.org/10.1007/s10472-020-09704-4.
  37. Eoin O'Mahony, Emmanuel Hebrard, Alan Holland, Conor Nugent, and Barry O'Sullivan. Using case-based reasoning in an algorithm portfolio for constraint solving. In Proc. AICS, pages 210-216, 2008. URL: https://homepages.laas.fr/ehebrard/papers/aics2008.pdf.
  38. Fabian Pedregosa, Gaël Varoquaux, Alexandre Gramfort, Vincent Michel, Bertrand Thirion, Olivier Grisel, Mathieu Blondel, Peter Prettenhofer, Ron Weiss, Vincent Dubourg, Jake Vanderplas, Alexandre Passos, David Cournapeau, Matthieu Brucher, Matthieu Perrot, and Édouard Duchesnay. Scikit-learn: Machine learning in Python. J. Mach. Learn. Res., 12(85):2825-2830, 2011. URL: http://jmlr.org/papers/v12/pedregosa11a.html.
  39. Nikhil Pimpalkhare, Federico Mora, Elizabeth Polgreen, and Sanjit A. Seshia. MedleySolver: Online SMT algorithm selection. In Proc. SAT, pages 453-470, 2021. URL: https://doi.org/10.1007/978-3-030-80223-3_31.
  40. Horst Samulowitz, Chandra Reddy, Ashish Sabharwal, and Meinolf Sellmann. Snappy: A simple algorithm portfolio. In Proc. SAT, pages 422-428, 2013. URL: https://doi.org/10.1007/978-3-642-39071-5_33.
  41. Haroldo G. Santos and Túlio A. M. Toffolo. Python-MIP. URL: https://python-mip.com/.
  42. Dominik Schreiber. Lilotane: A lifted SAT-based approach to hierarchical planning. J. Artif. Intell. Res., 70:1117-1181, 2021. URL: https://doi.org/10.1613/jair.1.12520.
  43. Joseph Scott, Aina Niemetz, Mathias Preiner, Saeed Nejati, and Vijay Ganesh. MachSMT: A machine learning-based algorithm selector for SMT solvers. In Proc. TACAS, pages 303-325, 2021. URL: https://doi.org/10.1007/978-3-030-72013-1_16.
  44. Matthew J. Streeter, Daniel Golovin, and Stephen F. Smith. Combining multiple heuristics online. In Proc. AAAI, pages 1197-1203, 2007. URL: https://www.aaai.org/Papers/AAAI/2007/AAAI07-190.pdf.
  45. Lin Xu, Frank Hutter, Holger Hoos, and Kevin Leyton-Brown. Features for SAT. Technical report, University of British Columbia, 2012. URL: https://www.cs.ubc.ca/labs/beta/Projects/SATzilla/Report_SAT_features.pdf.
  46. Lin Xu, Frank Hutter, Holger H. Hoos, and Kevin Leyton-Brown. SATzilla: Portfolio-based algorithm selection for SAT. J. Artif. Intell. Res., 32:565-606, 2008. URL: https://doi.org/10.1613/jair.2490.
  47. Lin Xu, Frank Hutter, Holger H. Hoos, and Kevin Leyton-Brown. Evaluating component solver contributions to portfolio-based algorithm selectors. In Proc. SAT, pages 228-241, 2012. URL: https://doi.org/10.1007/978-3-642-31612-8_18.
  48. Lin Xu, Frank Hutter, Jonathan Shen, Holger H. Hoos, and Kevin Leyton-Brown. SATzilla2012: Improved algorithm selection based on cost-sensitive classification models. In Proc. SAT Challenge, pages 57-58, 2012. URL: http://hdl.handle.net/10138/34218.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact