Encoding Quantified CSPs as Quantified Boolean Formulae

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 Formulae (QBFs), the analogous generalisation of satisfiability (SAT). We show that we can encode QCSPs as QBFs. We introduce a simple generalisation of the direct encoding of CSPs into SAT. We then introduce some adaptations of this encoding to make it effective in a QBF solver. We solve some QCSP test instances orders 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...

• Type: Conference
• Year: 2004
• Where: ECAI
• Authors: Ian P. Gent, Peter Nightingale, Andrew G. D. Rowley
• Keywords: Artificial Intelligence, ECAI 2004, Existentially Quantified, Quantified Boolean Formulae, Universally Quantified