## Krzysztof R. Apt

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

### Abstract

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.

Dvi-file

PS-File

PDF-File

Bibtex Entry