2026-08-18T07:50:01Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:23755 2025-11-14T06:48:01Z ddc:004 open_access

Improving Reduction Techniques in Pseudo-Boolean Conflict Analysis Lomis, Orestis Devriendt, Jo Bierlee, Hendrik Guns, Tias Constraint Programming Pseudo-Boolean Reasoning Conflict Analysis 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Orestis Lomis and Jo Devriendt and Hendrik Bierlee and Tias Guns 2025 Is Part Of LIPIcs, Volume 341, 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.SAT.2025.21 urn:nbn:de:0030-drops-237551 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2025.21 eng https://creativecommons.org/licenses/by/4.0/legalcode