Constraint Reductions

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 respect to their deductive power regarding General Arc Consistency (GAC).

Subsumption-driven clause learning with DPLL+restarts

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 approach allows the refutation of pebbling formulae in polynomial time and linear space, as effectively as with a CDCL solver.

SAT as a game

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 search heuristics.

Unit contradiction versus unit propagation

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 for computing such functions, depending on whether the result is the production of the empty clause or the assignment of a variable with a given truth value. We show that these two models can compute the same functions with formulae of polynomially related sizes, and we explain how this result is related to the CNF encoding of Boolean constraints.

On the expressive power of unit resolution

This preliminary report addresses the expressive power of unit resolution regarding input data encoded with partial truth assignments of propositional variables. A characterization of the functions that are computable in this way, which we propose to call propagatable functions, is given. By establishing that propagatable functions can also be computed using monotone circuits, we show that there exist polynomial time complexity propagable functions requiring an exponential amount of clauses to be computed using unit resolution. These results shed new light on studying CNF encodings of NP-complete problems in order to solve them using propositional satisfiability algorithms.

BoolVar/PB v1.0, a java library for translating pseudo-Boolean constraints into CNF formulae

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 encoding schemes are implemented in a way that each input constraint can be translated using one or several encoders, according to the related tags. The library can be easily extended by adding new encoders and / or new output formats.

On the CNF encoding of cardinality constraints and beyond

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 these encodings. We also propose models to facilitate analysis and design of CNF encodings for Boolean constraints.

Evolving difficult SAT instances thanks to local search

We propose to use local search algorithms to produce SAT instances which are harder to solve than randomly generated k-CNF formulae. The first results, obtained with rudimentary search algorithms, show that the approach deserves further study. It could be used as a test of robustness for SAT solvers, and could help to investigate how branching heuristics, learning strategies, and other aspects of solvers impact there robustness.

Reified unit resolution and the failed literal rule

Unit resolution can simplify a CNF formula or detect an inconsistency by repeatedly assign the variables occurring in unit clauses. Given any CNF formula sigma, we show that there exists a satisfiable CNF formula psi with size polynomially related to the size of sigma such that applying unit resolution to psi simulates all the effects of applying it to sigma. The formula psi is said to be the reified counterpart of sigma. This approach can be used to prove that the failed literal rule, which is an inference rule used by some SAT solvers, can be entirely simulated by unit resolution. More generally, it sheds new light on the expressive power of unit resolution.