3 citations · 6 across the 9 of their papers we have counts for
6 papers · 1 filter
Constraint Reductions
Olivier Bailleux, Yacine Boufkhad
This is a commentary on the CP 2003 paper "Efficient cnf encoding of boolean cardinality constraints". After recalling its context, we outline a classification of Constraints with…
Subsumption-driven clause learning with DPLL+restarts
Olivier Bailleux
We propose to use a DPLL+restart to solve SAT instances by successive simplifications based on the production of clauses that subsume the initial clauses. We show that this approac…
Unit contradiction versus unit propagation
Olivier Bailleux
Some aspects of the result of applying unit resolution on a CNF formula can be formalized as functions with domain a set of partial truth assignments. We are interested in two ways…
On the expressive power of unit resolution
Olivier Bailleux
This preliminary report addresses the expressive power of unit resolution regarding input data encoded with partial truth assignments of propositional variables. A characterization…
BoolVar/PB v1.0, a java library for translating pseudo-Boolean constraints into CNF formulae
Olivier Bailleux
BoolVar/PB is an open source java library dedicated to the translation of pseudo-Boolean constraints into CNF formulae. Input constraints can be categorized with tags. Several enco…
On the CNF encoding of cardinality constraints and beyond
Olivier Bailleux
In this report, we propose a quick survey of the currently known techniques for encoding a Boolean cardinality constraint into a CNF formula, and we discuss about the relevance of…