4 papers · 1 filter
On Dedicated CDCL Strategies for PB Solvers
Daniel Le Berre, Romain Wallon
Current implementations of pseudo-Boolean (PB) solvers working on native PB constraints are based on the CDCL architecture which empowers highly efficient modern SAT solvers. In pa…
On Improving the Backjump Level in PB Solvers
Romain Wallon
Current PB solvers implement many techniques inspired by the CDCL architecture of modern SAT solvers, so as to benefit from its practical efficiency. However, they also need to dea…
On Irrelevant Literals in Pseudo-Boolean Constraint Learning
Danel Le Berre, Pierre Marquis, Stefan Mengel +1
Learning pseudo-Boolean (PB) constraints in PB solvers exploiting cutting planes based inference is not as well understood as clause learning in conflict-driven clause learning sol…
On Weakening Strategies for PB Solvers
Daniel Le Berre, Pierre Marquis, Romain Wallon
Current pseudo-Boolean solvers implement different variants of the cutting planes proof system to infer new constraints during conflict analysis. One of these variants is generaliz…