OPEN ACCESS
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.
finite two-players game, quantified constraint satisfaction problem, QCSP
Ansotegui C., Gomes C., Selman B. (2005). Achilles’ heel of QBF. In Proceedings of the 20th national conference on artificial intelligence (aaai’05), p. 275-281.
Bacchus F., Stergiou K. (2007). Solution directed backjumping for QCSP. In Proceedings of the 13th international conference on principles and practice of constraint programming (cp’07), p. 148-163.
Barichard V., Stéphan I. (2014). The cut tool for QCSP. In Proceedings of the 26th ieee international conference on tools with artificial intelligence (ictai’14), p. 883-890.
Barichard V., Stéphan I. (2014). L’outil coupure pour les QCSP. In Actes des dixièmes journées francophones de programmation par contraintes (jfpc’14).
Benedetti M., Lallouet A., Vautard J. (2007). QCSP made practical by virtue of restricted quantification. In Proceedings of the 20th international joint conference on artificial intelligence (ijcai’07), p. 38-43.
Benedetti M., Lallouet A., Vautard J. (2008). Modeling adversary scheduling with QCSP+. In Proceedings of the 23th acm symposium on applied computing (sac’08), p. 151-155.
Bennaceur H. (2004). A comparison between SAT and CSP techniques. Constraints, vol. 9, no 2, p. 123-138.
Bordeaux L., Cadoli M., Mancini T. (2005). CSP Properties for Quantified Constraints: Definitions and Complexity. In Proceedings of the 20th national conference on artificial intelligence (aaai’05), p. 360-365.
Bordeaux L., Monfroy E. (2002). Beyond NP: Arc-Consistency for Quantified Constraints. In Proceedings of the 8th international conference on principles and practice of constraint programming (cp’02), p. 371-386.
Bordeaux L., Zhang L. (2007). A solver for quantified Boolean and linear constraints. In Proceedings of the 2007 acm symposium on applied computing (sac ’07), p. 321-325.
Börner F., Bulatov A., Chen H., Jeavons P., Krokhin A. (2009). The complexity of constraint satisfaction games and QCSP. Information and Computation, vol. 207, no 9, p. 923-944.
Börner F., Bulatov A., Jeavons P., Krokhin A. (2003). Quantified Constraints: Algorithms and Complexity. In Proceedings of the 17th international workshop on computer science logic (csl’03), p. 58-70.
Cadoli M., Giovanardi A., Schaerf M. (1998). An Algorithm to Evaluate Quantified Boolean Formulae. In Proceedings of the 15th national conference on artificial intelligence (aaai’98), p. 262-267.
Chen H., Madelaine F., Martin B. (2015). Quantified Constraints and Containment Problems. Logical Methods in Computer Science, vol. 11, no 3.
Coste-Marquis S., Fargier H., Lang J., Le Berre D., Marquis P. (2006). Representing Policies for Quantified Boolean Formulae. In Proceedings of the 10th international conference on principles of knowledge representation and reasoning (kr’06), p. 286-296.
Gebser M., Kaufmann B., Neumann A., Schaub T. (2007). Conflict-Driven Answer Set Solving. In Proceedings of the 20th international joint conference on artificial intelligence (ijcai’07), p. 386-392.
Gent I., Hoos H., Rowley A., Smyth K. (2003). Unsing Stochastic Local Search to Solve Quantified Boolean Formulae. In Proceedings of the 9th international conference on principles and practice of constraint programming (cp’03).
Gent I., Nightingale P., Rowley A. (2004). Encoding Quantified CSPs as Quantified Boolean Formulae. In Proceedings of the 16th european conference on artificial intelligence (ecai’04), p. 176-180.
Gent I., Nightingale P., Rowley A., Stergiou K. (2008). Solving quantified constraint satisfaction problems. Artificial Intelligence, vol. 172, no 6-7, p. 738-771.
Gent I., Nightingale P., Stergiou K. (2005). QCSP-solve: A solver for quantified constraint satisfaction problems. In Proceedings of 9th international joint conference on artificial intelligence (ijcai’05), p. 138-143.
Goultiaeva A., Bacchus F. (2010). Exploiting Circuit Representations in QBF Solving. In Proceedings of the 13th international conference on theory and applications of satisfiability testing (sat’10), p. 333-339.
Kleine Büning H., Zhao X. (2004). On Models for Quantified Boolean Formulas. In Logic versus approximation, in lecture notes in computer science 3075.
Kocsis L., Szepesvári C. (2006). Bandit based monte-carlo planning. In Proceedings of the 17th european conference on machine learning (ecml’06), vol. 4212 of LNCS, p. 282-293.
Mamoulis N., Stergiou K. (2004). Algorithms for Quantified Constraint Satisfaction Problems. In Proceedings of the 10th international conference on principles and practice of constraint programming (cp’04), p. 752-756.
Marques-Silva J., K.Sakallah. (1996). GRASP - A New Search Algorithm for Satisfiability. In Proceedings of ieee/acm international confenrence on computer-aided design (iccad’96), p. 220–227.
Nightingale P. (2007). Consistency and the Quantified Constraint Satisfaction Problem, PhD thesis, University of St Andrews.
Nightingale P. (2009). Non-binary quantified CSP: algorithms and modelling. Constraints, vol. 14, no 4, p. 539-581.
Papadimitriou C. (1994). Computational complexity. Addison-Wesley.
Pralet C., Verfaillie G. (2011). Beyond QCSP for Solving Control Problems. In Proceedings of the 17th international conference on principles and practice of constraint programming (cp’11), p. 744-758.
Prosser P. (1993). Hybrid algorithms for the constraint satisfaction problem. Computational Intelligence, vol. 9, p. 268-299.
Sabharwal A., Ansótegui C., Gomes C., Hart J., Selman B. (2006). QBF Modeling: Exploiting Player Symmetry for Simplicity and Efficiency. In Proceedings of the 9th international conference on theory and applications of satisfiability testing (sat’06), p. 382-395.
Selman B., Kautz H., Cohen B. (1994). Noise strategies for improving local search. In Proceedings of the 12th national conference on artificial intelligence (aaai’94), p. 337-343.
Stockmeyer L., Meyer A. (1973). Word problems requiring exponential time. In Proceedings of the 5th annual acm symposium on theory of computing (stoc ’73), p. 1-9.
Stynes D., Brown K. (2009). Value ordering for quantified CSPs. Constraints, vol. 14, no 1, p. 16-37.
Tsang E. (1993). Foundations of constraint satisfaction. Academic Press, London. Projet QuaCode 365
Verger G., Bessiere C. (2006). BlockSolve: a Bottom-Up Approach for Solving Quantified CSPs. In Proceedings of the 12th international conference on principles and practice of constraint programming (cp’06), p. 635-649.
Verger G., Bessiere C. (2008). Guiding Search in QCSP+ with Back-Propagation. In Proceedings of the 14th international conference on principles and practice of constraint programming (cp’08), p. 175-189.