Quantified constraint solving problems and finite two-player games : The QuaCode project

Quantified Constraint Satisfaction Problems (QCSP) are a generalization of Constraint Satisfaction Problems (CSP) in which variables may be quantified existentially and universally. QCSP offers a natural framework to express PSPACE problems as finite two-player games with perfect information or planing under uncertainty. We present how QCSP may be used to model two-player games on three classical games : Nim game, MatrixGame and Connect Four. State-of-The-Art QCSP solvers have an important drawback: They explore much larger combinatorial space than the natural search space of the original problem since they are unable to recognize that some sub-problems are necessarily true. We propose a very simple and elegant solution to use efficiently QCSP to design finite two-player games. Our QCSP solver built over GeCode, a CSP library, obtained very good results compared to state-of-The-Art QCSP solvers.