Document Open Access Logo

Selecting SAT Encodings for Pseudo-Boolean and Linear Integer Constraints

Authors Felix Ulrich-Oltean , Peter Nightingale , James Alfred Walker

PDF
Thumbnail PDF

File

LIPIcs.CP.2022.38.pdf
  • Filesize: 0.76 MB
  • 17 pages

Document Identifiers

Author Details

Felix Ulrich-Oltean
  • Department of Computer Science, University of York, UK
Peter Nightingale
  • Department of Computer Science, University of York, UK
James Alfred Walker
  • Department of Computer Science, University of York, UK

Funding

  • Ulrich-Oltean, Felix: Supported by grant EP/R513386/1 from the UK Engineering and Physical Sciences Research Council.

Acknowledgements

We are very grateful to Nguyen Dang for helpful conversations about portfolio approaches. The experiments were undertaken on the Viking Cluster, which is a high performance compute facility provided by the University of York. We are grateful for support from the University of York High Performance Computing service, Viking and the Research Computing team.

Cite As Get BibTex

Felix Ulrich-Oltean, Peter Nightingale, and James Alfred Walker. Selecting SAT Encodings for Pseudo-Boolean and Linear Integer Constraints. In 28th International Conference on Principles and Practice of Constraint Programming (CP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 235, pp. 38:1-38:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022) https://doi.org/10.4230/LIPIcs.CP.2022.38

Abstract

Many constraint satisfaction and optimisation problems can be solved effectively by encoding them as instances of the Boolean Satisfiability problem (SAT). However, even the simplest types of constraints have many encodings in the literature with widely varying performance, and the problem of selecting suitable encodings for a given problem instance is not trivial. We explore the problem of selecting encodings for pseudo-Boolean and linear constraints using a supervised machine learning approach. We show that it is possible to select encodings effectively using a standard set of features for constraint problems; however we obtain better performance with a new set of features specifically designed for the pseudo-Boolean and linear constraints. In fact, we achieve good results when selecting encodings for unseen problem classes. Our results compare favourably to AutoFolio when using the same feature set. We discuss the relative importance of instance features to the task of selecting the best encodings, and compare several variations of the machine learning method.

Subject Classification

ACM Subject Classification
  • Theory of computation → Constraint and logic programming
Keywords
  • Constraint programming
  • SAT encodings
  • machine learning
  • global constraints
  • pseudo-Boolean constraints
  • linear constraints

Metrics

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

Supplementary Materials

References

  1. I. Abío, R. Nieuwenhuis, A. Oliveras, E. Rodríguez-Carbonell, and V. Mayer-Eichberger. A New Look at BDDs for Pseudo-Boolean Constraints. Journal of Artificial Intelligence Research, 45:443-480, November 2012. URL: https://doi.org/10.1613/jair.3653.
  2. Ignasi Abío, Valentin Mayer-Eichberger, and Peter Stuckey. Encoding Linear Constraints into SAT. arXiv:2005.02073 [cs], May 2020. URL: http://arxiv.org/abs/2005.02073.
  3. Ignasi Abío, Valentin Mayer-Eichberger, and Peter J Stuckey. Encoding linear constraints with implication chains to CNF. In International Conference on Principles and Practice of Constraint Programming, pages 3-11. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-23219-5_1.
  4. Roberto Amadini, Maurizio Gabbrielli, and Jacopo Mauro. An enhanced features extractor for a portfolio of constraint solvers. In Proceedings of the 29th Annual ACM Symposium on Applied Computing, SAC '14, pages 1357-1359, New York, NY, USA, March 2014. Association for Computing Machinery. URL: https://doi.org/10.1145/2554850.2555114.
  5. Carlos Ansótegui, Miquel Bofill, Jordi Coll, Nguyen Dang, Juan Luis Esteban, Ian Miguel, Peter Nightingale, András Z Salamon, Josep Suy, and Mateu Villaret. Automatic detection of at-most-one and exactly-one relations for improved SAT encodings of pseudo-boolean constraints. In International Conference on Principles and Practice of Constraint Programming, pages 20-36. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-30048-7.
  6. Olivier Bailleux, Yacine Boufkhad, and Olivier Roussel. New Encodings of Pseudo-Boolean Constraints into CNF. In Oliver Kullmann, editor, Theory and Applications of Satisfiability Testing - SAT 2009, Lecture Notes in Computer Science, pages 181-194, Berlin, Heidelberg, 2009. Springer. URL: https://doi.org/10.1007/978-3-642-02777-2_19.
  7. Miquel Bofill, Jordi Coll, Peter Nightingale, Josep Suy, Felix Ulrich-Oltean, and Mateu Villaret. SAT encodings for Pseudo-Boolean constraints together with at-most-one constraints. Artificial Intelligence, 302:103604, January 2022. URL: https://doi.org/10.1016/j.artint.2021.103604.
  8. Miquel Bofill, Jordi Coll, Josep Suy, and Mateu Villaret. Compact MDDs for Pseudo-Boolean Constraints with At-Most-One Relations in Resource-Constrained Scheduling Problems. In Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence, pages 555-562, Melbourne, Australia, August 2017. International Joint Conferences on Artificial Intelligence Organization. URL: https://doi.org/10.24963/ijcai.2017/78.
  9. Miquel Bofill, Jordi Coll, Josep Suy, and Mateu Villaret. SAT encodings of pseudo-boolean constraints with at-most-one relations. In International Conference on Integration of Constraint Programming, Artificial Intelligence, and Operations Research, pages 112-128. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-19212-9.
  10. Miquel Bofill, Jordi Coll, Josep Suy, and Mateu Villaret. An MDD-based SAT encoding for pseudo-Boolean constraints with at-most-one relations. Artificial Intelligence Review, 53(7):5157-5188, 2020. URL: https://doi.org/10.1007/s10462-020-09817-6.
  11. Leo Breiman. Random Forests. Machine Learning, 45(1):5-32, October 2001. URL: https://doi.org/10.1023/A:1010933404324.
  12. Ewan Davidson, Özgür Akgün, Joan Espasa, and Peter Nightingale. Effective Encodings of Constraint Programming Models to SMT. In Helmut Simonis, editor, Principles and Practice of Constraint Programming, Lecture Notes in Computer Science, pages 143-159, Cham, 2020. Springer International Publishing. URL: https://doi.org/10.1007/978-3-030-58475-7_9.
  13. Marijn Heule, Matti Jarvisalo, Martin Suda, Markus Iser, Tomáš Balyo, and Nils Froleyks. SAT competitions. URL: https://satcompetition.github.io/ [cited 22.02.2022].
  14. Steffen Hölldobler, Norbert Manthey, and Peter Steinke. A Compact Encoding of Pseudo-Boolean Constraints into SAT. In Birte Glimm and Antonio Krüger, editors, KI 2012: Advances in Artificial Intelligence, Lecture Notes in Computer Science, pages 107-118, Berlin, Heidelberg, 2012. Springer. URL: https://doi.org/10.1007/978-3-642-33347-7_10.
  15. Barry Hurley, Lars Kotthoff, Yuri Malitsky, and Barry O'Sullivan. Proteus: A Hierarchical Portfolio of Solvers and Transformations. In Helmut Simonis, editor, Integration of AI and OR Techniques in Constraint Programming, Lecture Notes in Computer Science, pages 301-317, Cham, 2014. Springer International Publishing. URL: https://doi.org/10.1007/978-3-319-07046-9.
  16. Saurabh Joshi, Ruben Martins, and Vasco Manquinho. Generalized Totalizer Encoding for Pseudo-Boolean Constraints. In Gilles Pesant, editor, Principles and Practice of Constraint Programming, Lecture Notes in Computer Science, pages 200-209, Cham, 2015. Springer International Publishing. URL: https://doi.org/10.1007/978-3-319-23219-5_15.
  17. Pascal Kerschke, Holger H. Hoos, Frank Neumann, and Heike Trautmann. Automated Algorithm Selection: Survey and Perspectives. Evolutionary Computation, 27(1):3-45, March 2019. URL: https://doi.org/10.1162/evco_a_00242.
  18. Christophe Lecoutre and Olivier Roussel. XCSP3 Competition, 2019. URL: http://www.cril.univ-artois.fr/XCSP19/ [cited 22.02.2022].
  19. Marius Lindauer, Holger H. Hoos, Frank Hutter, and Torsten Schaub. AutoFolio: An Automatically Configured Algorithm Selector. Journal of Artificial Intelligence Research, 53:745-778, August 2015. URL: https://doi.org/10.1613/jair.4726.
  20. Peter Nightingale. Savile Row 1.9.0 Manual. URL: https://savilerow.cs.st-andrews.ac.uk/index.html [cited 22.02.2022].
  21. Peter Nightingale, Özgür Akgün, Ian P. Gent, Christopher Jefferson, Ian Miguel, and Patrick Spracklen. Automatically improving constraint models in Savile Row. Artificial Intelligence, 251:35-61, October 2017. URL: https://doi.org/10.1016/j.artint.2017.07.001.
  22. F. Pedregosa, G. Varoquaux, A. Gramfort, V. Michel, B. Thirion, O. Grisel, M. Blondel, P. Prettenhofer, R. Weiss, V. Dubourg, J. Vanderplas, A. Passos, D. Cournapeau, M. Brucher, M. Perrot, and E. Duchesnay. Scikit-learn: Machine learning in Python. Journal of Machine Learning Research, 12:2825-2830, 2011. Google Scholar
  23. Philipp Probst, Marvin N. Wright, and Anne-Laure Boulesteix. Hyperparameters and tuning strategies for random forest. WIREs Data Mining and Knowledge Discovery, 9(3):e1301, 2019. URL: https://doi.org/10.1002/widm.1301.
  24. Mirko Stojadinović and Filip Marić. meSAT: Multiple encodings of CSP to SAT. Constraints, 19(4):380-403, October 2014. URL: https://doi.org/10.1007/s10601-014-9165-7.
  25. Naoyuki Tamura, Akiko Taga, Satoshi Kitagawa, and Mutsunori Banbara. Compiling finite linear CSP into SAT. Constraints, 14(2):254-272, June 2009. URL: https://doi.org/10.1007/s10601-008-9061-0.
  26. Helsinki Institute for Information Technology University of Helsinki, Tomáš Balyo, Nils Froleyks, Marijn Heule, Markus Iser, Matti Järvisalo, and Martin Suda. Proceedings of SAT Competition 2021 : Solver and Benchmark Descriptions. In Proceedings of SAT Competition 2021. Department of Computer Science, University of Helsinki, 2021. Google Scholar
  27. Neng-Fa Zhou and Håkan Kjellerstrand. Optimizing SAT encodings for arithmetic constraints. In International Conference on Principles and Practice of Constraint Programming, pages 671-686. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-66158-2_43.
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 About DROPS Imprint Privacy Contact