1 citations · 1 across the 5 of their papers we have counts for
5 papers
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…
Graph Width Measures for CNF-Encodings with Auxiliary Variables
Stefan Mengel, Romain Wallon
We consider bounded width CNF-formulas where the width is measured by popular graph width measures on graphs associated to CNF-formulas. Such restricted graph classes, in particula…