PS-File
PDF-File
Bibtex Entry
Centre for Mathematics and Computer Science
Kruislaan 413, 1098 SJ Amsterdam, The Netherlands
and
Dept. of Mathematics, Computer Science, Physics & Astronomy
University of Amsterdam, Plantage Muidergracht 24
1018 TV Amsterdam, The Netherlands
apt@cwi.nl
http://www.cwi.nl/~apt
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.