Document Open Access Logo

Improving Reduction Techniques in Pseudo-Boolean Conflict Analysis

Authors Orestis Lomis , Jo Devriendt , Hendrik Bierlee , Tias Guns

PDF HTML 5

Files

Thumbnail PDF
PDF
LIPIcs.SAT.2025.21.pdf
  • Filesize: 1.41 MB
  • 17 pages
HTML5 Logo HTML (experimental)
LIPIcs.SAT.2025.21.html

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Constraint and logic programming
Keywords
  • Constraint Programming
  • Pseudo-Boolean Reasoning
  • Conflict Analysis

Metrics

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

Abstract

Recent pseudo-Boolean (PB) solvers leverage the cutting planes proof system to perform SAT-style conflict analysis during search. This process learns implied PB constraints, which can prune later parts of the search tree and is crucial to a PB solver’s performance. A key step in PB conflict analysis is the reduction of a reason constraint, which caused a variable propagation that contributed to the conflict. While necessary, reduction generally makes the reason constraint less strong. Consequently, different approaches to reduction have been proposed, broadly categorised as division- or saturation-based, with the aim of preserving the strength of the reason constraint as much as possible.
This paper proposes two novel techniques in each reduction category. We theoretically show how each technique yields reason constraints which are at least as strong as those obtained from existing reduction methods. We then evaluate the empirical effectiveness of the reduction techniques on hard knapsack instances and the most recent PB'24 competition benchmarks.

Cite As Get BibTex

Orestis Lomis, Jo Devriendt, Hendrik Bierlee, and Tias Guns. Improving Reduction Techniques in Pseudo-Boolean Conflict Analysis. In 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 341, pp. 21:1-21:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.SAT.2025.21

Author Details

Orestis Lomis
  • DTAI, KU Leuven, Belgium
Jo Devriendt
  • Nonfiction Software, Leuven, Belgium
Hendrik Bierlee
  • DTAI, KU Leuven, Belgium
Tias Guns
  • DTAI, KU Leuven, Belgium

Funding

This research was partly funded by the European Research Council (ERC) under the EU Horizon 2020 research and innovation programme (Grant No 101002802, CHAT-Opt).

Supplementary Materials

References

  1. Gilles Audemard and Laurent Simon. On the glucose SAT solver. Int. J. Artif. Intell. Tools, 27(1):1840001:1-1840001:25, February 2018. URL: https://doi.org/10.1142/S0218213018400018.
  2. Danel Le Berre, Pierre Marquis, Stefan Mengel, and Romain Wallon. On Irrelevant Literals in Pseudo-Boolean Constraint Learning. In Proceedings of the Twenty-Ninth International Joint Conference on Artificial Intelligence, pages 1148-1154, July 2020. URL: https://doi.org/10.24963/ijcai.2020/160.
  3. Daniel Le Berre and Anne Parrain. The sat4j library, release 2.2. J. Satisf. Boolean Model. Comput., 7(2-3):59-6, 2010. URL: https://doi.org/10.3233/sat190075.
  4. Sam Buss and Jakob Nordström. Proof complexity and SAT solving. In Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisfiability - Second Edition, volume 336 of Frontiers in Artificial Intelligence and Applications, pages 233-350. IOS Press, 2021. URL: https://doi.org/10.3233/FAIA200990.
  5. Donald Chai and Andreas Kuehlmann. A fast pseudo-boolean constraint solver. In Proceedings of the 40th Annual Design Automation Conference, pages 830-835, Anaheim CA USA, June 2003. ACM. URL: https://doi.org/10.1145/775832.776041.
  6. Donald Chai and Andreas Kuehlmann. A fast pseudo-boolean constraint solver. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 24:305-317, 2005. URL: https://doi.org/10.1109/TCAD.2004.842808.
  7. Stephen A. Cook. The complexity of theorem-proving procedures. In Michael A. Harrison, Ranan B. Banerji, and Jeffrey D. Ullman, editors, Proceedings of the 3rd Annual ACM Symposium on Theory of Computing, May 3-5, 1971, Shaker Heights, Ohio, USA, STOC '71, pages 151-158, New York, NY, USA, 1971. ACM. URL: https://doi.org/10.1145/800157.805047.
  8. W. Cook, C.R. Coullard, and Gy. Turán. On the complexity of cutting-plane proofs. Discrete Applied Mathematics, 18(1):25-38, September 1987. URL: https://doi.org/10.1016/0166-218X(87)90039-4.
  9. Jo Devriendt. Pisinger’s knapsack instances in opb format, July 2020. URL: https://doi.org/10.5281/zenodo.3939055.
  10. Jo Devriendt. Watched Propagation of 0-1 Integer Linear Constraints. In Helmut Simonis, editor, Principles and Practice of Constraint Programming, pages 160-176, Cham, 2020. Springer International Publishing. URL: https://doi.org/10.1007/978-3-030-58475-7_10.
  11. Jo Devriendt. Exact: Evaluating cutting-planes learning at the PB'24 competition. Slides, 2024. Google Scholar
  12. Jan Elffers and Jakob Nordström. Divide and Conquer: Towards Faster Pseudo-Boolean Solving. In Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence, pages 1291-1299, Stockholm, Sweden, July 2018. International Joint Conferences on Artificial Intelligence Organization. URL: https://doi.org/10.24963/ijcai.2018/180.
  13. Jan Elffers and Jakob Nordström. RoundingSat 2019: Recent work on PB solving. https://slides.com/jod/deck-26-29-32, July 2019.
  14. Armin Haken. The intractability of resolution. Theor. Comput. Sci., 39:297-308, 1985. Third Conference on Foundations of Software Technology and Theoretical Computer Science. URL: https://doi.org/10.1016/0304-3975(85)90144-6.
  15. John N Hooker. Generalized resolution and cutting planes. Annals of Operations Research, 12:217-239, 1988. Google Scholar
  16. Hannes Ihalainen, Jeremias Berg, and Matti Järvisalo. Ipbhs in pb'24 competition. Slides, 2024. Google Scholar
  17. Christoph Jabs, Jeremias Berg, and Matti Järvisalo. PB-OLL-RS and MIXED-BAG in Pseudo-Boolean Competition 2024. PB Competition 2024, 2024. Google Scholar
  18. Daniel Le Berre, Pierre Marquis, and Romain Wallon. On Weakening Strategies for PB Solvers. In Luca Pulina and Martina Seidl, editors, Theory and Applications of Satisfiability Testing - SAT 2020, pages 322-331, Cham, 2020. Springer International Publishing. URL: https://doi.org/10.1007/978-3-030-51825-7_23.
  19. Orestis Lomis, Jo Devriendt, Hendrik Bierlee, and Tias Guns. ML-KULeuven/SAT25_PB_reductions_experiments. Dataset, This research was partly funded by the European Research Council (ERC) under the EU Horizon 2020 research and innovation programme (Grant No 101002802, CHAT-Opt)., (visited on 2025-07-23). URL: https://github.com/ML-KULeuven/SAT25_PB_reductions_experiments
    Software Heritage Logo archived version
    full metadata available at: https://doi.org/10.4230/artifacts.24089
  20. J.P. Marques Silva and K.A. Sakallah. Grasp-a new search algorithm for satisfiability. In Proceedings of International Conference on Computer Aided Design, pages 220-227, 1996. URL: https://doi.org/10.1109/ICCAD.1996.569607.
  21. Gioni Mexi, Timo Berthold, Ambros Gleixner, and Jakob Nordström. Improving conflict analysis in mip solvers by pseudo-boolean reasoning. arXiv preprint arXiv:2307.14166, 2023. URL: https://doi.org/10.48550/arXiv.2307.14166.
  22. Shiwei Pan, Yiyuan Wang, Shaowei Cai, Jiangnan Li, Wenbo Zhu, and Minghao Yin. Cashwmaxsat-disjcad: Solver description. MaxSAT Evaluation 2024, 2024:25, 2024. Google Scholar
  23. David Pisinger. Where are the hard knapsack problems? Comput. Oper. Res., 32(9):2271-2284, 2005. URL: https://doi.org/10.1016/j.cor.2004.03.002.
  24. Roussel, Olivier. Pseudo-Boolean Competition of 2024. URL: https://www.cril.univ-artois.fr/PB24/.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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