A Logical Analysis of
Boolean Constraints

Krzysztof R. Apt

Centre for Mathematics and Computer Science
Kruislaan 413, 1098 SJ Amsterdam, The Netherlands
Dept. of Mathematics, Computer Science, Physics & Astronomy
University of Amsterdam, Plantage Muidergracht 24
1018 TV Amsterdam, The Netherlands


In (Apt 1998a) we provided a proof theoretic account of constraint programming. Here we show how it can be used to analyse Boolean constraints. More precisely, we show here how a Boolean constraint solver based on the look-ahead search strategy can be defined in a purely logical way. To this end we characterize arc consistency for Boolean constraints by proof theoretic means. As a byproduct we clarify the status of the proof rules introduced in (Codognet and Diaz 1996) that form a basis of their Boolean constraint solver. These considerations lead to a simple Boolean constraint solver that generates all solutions to a given set of Boolean constraints. It performs well on various benchmarks.

Bibtex Entry