Encoding quantified CSPs as Quantified Boolean Formulae
Ian P. Gent, Peter W. Nightingale, Andrew G. D. Rowley · 2004
Abstract. 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 QC-SPs 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 highly developed, encodings into a better understood problem can give access to extremely advanced search methods with very little implementation effort. 1