Document Open Access Logo

Exploiting Configurations of MaxSAT Solvers

Authors Josep Alòs , Carlos Ansótegui , Josep M. Salvia , Eduard Torres

PDF
Thumbnail PDF

File

LIPIcs.CP.2023.7.pdf
  • Filesize: 0.84 MB
  • 16 pages

Document Identifiers

Author Details

Josep Alòs
  • Logic & Optimization Group (LOG), University of Lleida, Spain
Carlos Ansótegui
  • Logic & Optimization Group (LOG), University of Lleida, Spain
Josep M. Salvia
  • Logic & Optimization Group (LOG), University of Lleida, Spain
Eduard Torres
  • Logic & Optimization Group (LOG), University of Lleida, Spain

Funding

This work was supported by MCIN/AEI/10.13039/501100011033 (Grant: PID2019-109137GB-C21), Agencia de Gestio d’Ajuts Universitaris i de Recerca (AGAUR), Departament d’Empresa i Coneixement de la Generalitat de Catalunya (Grant: 2022 FI_B 00010)

Acknowledgements

We want to thank Alexander Nadel for sharing the solver TT-Open-WBO with the configurable parameters exposed.

Cite AsGet BibTex

Josep Alòs, Carlos Ansótegui, Josep M. Salvia, and Eduard Torres. Exploiting Configurations of MaxSAT Solvers. In 29th International Conference on Principles and Practice of Constraint Programming (CP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 280, pp. 7:1-7:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.CP.2023.7

Abstract

In this paper, we describe how we can effectively exploit alternative parameter configurations to a MaxSAT solver. We describe how these configurations can be computed in the context of MaxSAT. In particular, we experimentally show how to easily combine configurations of a non-competitive solver to obtain a better solving approach.

Subject Classification

ACM Subject Classification
  • Theory of computation → Constraint and logic programming
Keywords
  • maximum satisfiability
  • maxsat evaluation
  • automatic configuration

Metrics

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

References

  1. Josep Alòs, Carlos Ansótegui, Josep M. Salvia, and Eduard Torres. OptiLog V2: Model, Solve, Tune and Run. In Kuldeep S. Meel and Ofer Strichman, editors, 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022), volume 236 of Leibniz International Proceedings in Informatics (LIPIcs), pages 25:1-25:16, Dagstuhl, Germany, 2022. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. ISSN: 1868-8969. URL: https://doi.org/10.4230/LIPIcs.SAT.2022.25.
  2. Carlos Ansótegui, Josep Pon, and Meinolf Sellmann. Boosting evolutionary algorithm configuration. Annals of Mathematics and Artificial Intelligence, 2021. URL: https://doi.org/10.1007/s10472-020-09726-y.
  3. Carlos Ansótegui, Josep Pon, and Meinolf Sellmann. Boosting evolutionary algorithm configuration. Annals of Mathematics and Artificial Intelligence, 90(7-9):715-734, 2022. Publisher: Springer. Google Scholar
  4. Carlos Ansótegui, Meinolf Sellmann, and Kevin Tierney. A Gender-based Genetic Algorithm for the Automatic Configuration of Algorithms. In Proceedings of the 15th International Conference on Principles and Practice of Constraint Programming, CP'09, pages 142-157. Springer-Verlag, 2009. tex.acmid: 1789011 tex.numpages: 16 tex.year: 2009 event-place: Lisbon, Portugal. URL: http://dl.acm.org/citation.cfm?id=1788994.1789011.
  5. Fahiem Bacchus, Jeremias Berg, Matti Järvisalo, Ruben Martins, and Andreas Niskanen. MaxSAT Evaluation 2022 : Solver and Benchmark Descriptions. Department of Computer Science Series of Publications B, B-2022-2, 2022. Accepted: 2022-08-25T10:09:01Z Publisher: Department of Computer Science, University of Helsinki. URL: https://helda.helsinki.fi/handle/10138/347396.
  6. Jeremias Berg, Emir Demirovic, and Peter Stuckey. Core-boosted linear search for incomplete maxsat. Integration of Constraint Programming, Artificial Intelligence, and Operations Research: 16th International Conference, CPAIOR 2019, 2019. Google Scholar
  7. Yi Chu, Shaowei Cai, Zhendong Lei, and Xiang He. Nuwls-c: Solver description. MaxSAT Evaluation 2022, page 28, 2022. Google Scholar
  8. Jan Elffers and Jakob Nordström. Divide and conquer: Towards faster pseudo-boolean solving. Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence, pages 1291-1299, 2018. URL: https://www.ijcai.org/Proceedings/2018/180.
  9. Youssef Hamadi, Said Jabbour, and Lakhdar Sais. ManySAT: a parallel SAT solver. JSAT, 6:245-262, June 2009. URL: https://doi.org/10.3233/SAT190070.
  10. Frank Hutter, Holger H Hoos, and Kevin Leyton-Brown. Sequential Model-Based Optimization for General Algorithm Configuration (extended version). International Conference on Learning and Intelligent Optimization, 2011. Google Scholar
  11. Jo Devriendt. Exact Solver Repository, April 2023. URL: https://gitlab.com/JoD/exact.
  12. Saurabh Joshi, Prateek Kumar, Sukrut Rao, and Ruben Martins. Open-wbo-inc: Approximation strategies for incomplete weighted maxsat. J. Satisf. Boolean Model. Comput., 11(1):73-97, 2019. URL: https://doi.org/10.3233/SAT190118.
  13. Serdar Kadioglu, Yuri Malitsky, Meinolf Sellmann, and Kevin Tierney. ISAC – Instance-Specific Algorithm Configuration. In ECAI 2010, pages 751-756. IOS Press, 2010. URL: https://doi.org/10.3233/978-1-60750-606-5-751.
  14. Marius Lindauer, Katharina Eggensperger, Matthias Feurer, André Biedenkapp, Difan Deng, Carolin Benjamins, Tim Ruhkopf, René Sass, and Frank Hutter. SMAC3: A Versatile Bayesian Optimization Package for Hyperparameter Optimization. In ArXiv: 2109.09831, 2021. URL: https://arxiv.org/abs/2109.09831.
  15. Ole Lübke and Sibylle Schupp. nosat-maxsat. In MaxSAT Evaluation 2022, pages 29-30. Department of Computer Science, University of Helsinki, 2022. Google Scholar
  16. Alexander Nadel. Polarity and Variable Selection Heuristics for SAT-Based Anytime MaxSAT: System Description. Journal on Satisfiability, Boolean Modeling and Computation, 12(1):17-22, September 2020. URL: https://doi.org/10.3233/SAT-200126.
  17. Olivier Roussel. Description of ppfolio 2012. In Proceedings of SAT Challenge 2012: Solver and Benchmark Descriptions, 2012. Google Scholar
  18. Jiongzhi Zheng, Kun He, Zhuo Chen, Jianrong Zhou, and Chu-Min Li. Decision tree based hybrid walking strategies. MaxSAT Evaluation 2022, page 24, 2022. Google Scholar
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