QCSP-solve: a solver for quantified constraint satisfaction problems

Abstract

The Quantified Constraint Satisfaction Problem (QCSP) is a generalization of the CSP in which some variables are universally quantified. It has been shown that a solver based on an encoding of QCSP into QBF can outperform the existing direct QCSP approaches by several orders of magnitude. In this paper we introduce an efficient QCSP solver. We show how knowledge learned from the successful encoding of QCSP into QBF can be utilized to enhance the existing QCSP techniques and speed up search by orders of magnitude. We also show how the performance of the solver can be further enhanced by incorporating advanced lookback techniques such as CBJ and solution-directed pruning. Experiments demonstrate that our solver is several orders of magnitude faster than existing direct approaches to QCSP solving, and significantly outperforms approaches based on encoding QCSPs as QBFs. 1