activity
20102020
most citedOn the CNF encoding of cardinality constraints and beyond

3 citations · 6 across the 9 of their papers we have counts for

collaborators

9 papers

cs.AI2020

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…

cs.AI2019

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…

cs.CC2015

SAT as a game

Olivier Bailleux

We propose a funny representation of SAT. While the primary interest is to present propositional satisfiability in a playful way for pedagogical purposes, it could also inspire new…

cs.AI2012★ 1 cited

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…

cs.AI2011★ 1 cited

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…

cs.AI2011★ 1 cited

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…