Solving quantified constraint satisfaction problems

Ian Philip Gent, Peter Nightingale, Andrew Rowley, Kostas Stergiou

Research output: Contribution to journalArticlepeer-review

28 Citations (Scopus)


We make a number of contributions to the study of the Quantified Constraint Satisfaction Problem (QCSP). The QCSP is an extension of the constraint satisfaction problem that can be used to model combinatorial problems containing contingency or uncertainty. It allows for universally quantified variables that can model uncertain actions and events, such as the unknown weather for a future party, or an opponent's next move in a game. In this paper we report significant contributions to two very different methods for solving QCSPs. The first approach is to implement special purpose algorithms for QCSPs; and the second is to encode QCSPs as Quantified Boolean Formulas and then use specialized QBF solvers. The discovery of particularly effective encodings influenced the design of more effective algorithms: by analyzing the properties of these encodings, we identify the features in QBF solvers responsible for their efficiency. This enables us to devise analogues of these features in QCSPs, and implement them in special purpose algorithms, yielding an effective special purpose solver, QCSP-Solve. Experiments show that this solver and a highly optimized QBF encoding are several orders of magnitude more efficient than the initially developed algorithms. A final, but significant, contribution is the identification of flaws in simple methods of generating random QCSP instances, and a means of generating instances which are not known to be flawed. (c) 2007 Elsevier B.V. All rights reserved.

Original languageEnglish
Pages (from-to)738-771
Number of pages34
JournalArtificial Intelligence
Issue number6-7
Early online date22 Nov 2007
Publication statusPublished - Apr 2008


  • quantified constraint satisfaction problems
  • quantified boolean formulas
  • arc consistency
  • search algorithms
  • random problems


Dive into the research topics of 'Solving quantified constraint satisfaction problems'. Together they form a unique fingerprint.

Cite this