ECAI 2004 Conference Paper

[full paper]

Encoding Quantified CSPs as Quantified Boolean Formulae

Ian Gent, Peter Nightingale, Andrew Rowley

Quantified Constraint Satisfaction Problems (QCSPs) are CSPs in which some variables are universally quantified. For each possible value of such variables, we have to find ways to set the remaining, existentially quantified, variables so that the constraints are all satisfied. Interest in this topic is increasing following recent advances in Quantified Boolean Formulas (QBFs), the analogous generalisation of satisfiability (SAT). We show that we can encode QCSPs as QBFs. We introduce simple generalisations of both the direct and support encodings of CSPs into SAT. We then introduce some adaptations of these encodings to make them effective for search in a QBF solver. We solve some QCSP test instances an order of magnitude faster than using a specialised QCSP solver, taking advantage of the more advanced state of the art in QBF solving. Our conclusions are twofold. First, there is considerably more subtlety required in encodings in QBF than in SAT. Second, in an area such as QCSP where algorithmic techniques are not yet highly developed, encodings into a better understood problem can give access to extremely advanced search methods with very little implementation effort.

Keywords: Satisfiability Testing, Constraint Satisfaction, Search, Automated Reasoning

Citation: Ian Gent, Peter Nightingale, Andrew Rowley: Encoding Quantified CSPs as Quantified Boolean Formulae. In R.López de Mántaras and L.Saitta (eds.): ECAI2004, Proceedings of the 16th European Conference on Artificial Intelligence, IOS Press, Amsterdam, 2004, pp.176-180.