Solving quantified constraint satisfaction problems with value selection rules

Abstract

Solving a quantified constraint satisfaction problem (QCSP) is usually a hard task due to its computational complexity. Exact algorithms play an important role in solving this problem, among which backtrack algorithms are effective. In a backtrack algorithm, an important step is assigning a variable by a chosen value when exploiting a branch, and thus a good value selection rule may speed up greatly. In this paper, we propose two value selection rules for existentially and universally quantified variables, respectively, to avoid unnecessary searching. The rule for universally quantified variables is prior to trying failure values in previous branches, and the rule for existentially quantified variables selects the promising values first. Two rules are integrated into the state-of-the-art QCSP solver, i.e., QCSPSolve, which is an exact solver based on backtracking. We perform a number of experiments to evaluate improvements brought by our rules. From computational results, we can conclude that the new value selection rules speed up the solver by 5 times on average and 30 times at most. We also show both rules perform well particularly on instances with existentially and universally quantified variables occurring alternatively.

Keywords

quantified CSP / backtracking / value selection / fail-first principle

References

[1] Chu Y, Luo C, Cai S, You H. Empirical investigation of stochastic local search for maximum satisfiability. Frontiers of Computer Science, 2019, 13(1): 86–98

[2] Zhang Z, Fu Q, Zhang X, Liu Q. Reasoning and predicting POMDP planning complexity via covering numbers. Frontiers of Computer Science, 2016, 10(4): 726–740

[3] Gao J, Wang J, Yin M. Experimental analyses on phase transitions in compiling satisfiability problems. Science China Information Sciences, 2015, 58(3): 1–11

[4] Amilhastre J, Fargier H, Marquis P. Consistency restoration and explanations in dynamic CSPs—application to configuration. Artificial Intelligence, 2002, 135(1–2): 199–234

[5] Ghallab M, Nau D, Traverso P. Automated Planning: Theory and Practice. Elsevier, 2004

[6] Palmieri A, Lallouet A. Constraint games revisited. In: Proceedings of the 26th International Joint Conference on Artificial Intelligence. 2017, 729–735

[7] Bessière C, Régin J C. MAC and combined heuristics: two reasons to forsake FC (and CBJ?) on hard problems. In: Proceedings of the 2nd International Conference on Principles and Practice of Constraint Programming. 1996, 61–75

[8] Chen X, Van B P. Conflict-directed backjumping revisited. Journal of Artificial Intelligence Research, 2001, 14(1): 53–81

[9] Geelen P A. Dual viewpoint heuristics for binary constraint satisfaction problems. In: Proceedings of the 10th European Conference on Artificial Intelligence. 1992, 31–35

[10] Gent I P, MacIntyre E, Prosser P, Smith B M, Walsh T. An empirical study of dynamic variable ordering heuristics for the constraint satisfaction problem. In: Proceedings of the 2nd International Conference on Principles and Practice of Constraint Programming. 1996, 179–193

[11] Smith B M, Grant S A. Trying harder to fail first. In: Proceedings of the 13th European Conference on Artificial Intelligence. 1998, 41–55

[12] Nightingale P. Consistency for quantified constraint satisfaction problems. In: Proceedings of the 11th International Conference on Principles and Practice of Constraint Programming. 2005, 792–796

[13] Gent I P, Nightingale P, Rowley A, Stergiou K. Solving quantified constraint satisfaction problems. Artificial Intelligence, 2008, 17(6–7): 738–771

[14] Gent I P, Nightingale P, Stergiou K. QCSP-Solve: a solver for quantified constraint satisfaction problems. In: Proceedings of the 19th International Joint Conference on Artificial Intelligence. 2005, 138–143

[15] Büning H K, Karpinski M, Flögel A. Resolution for quantified boolean formulas. Information and Computation, 1995, 117(1): 12–18

[16] Nightingale P. Non-binary quantified CSP: algorithms and modelling. Constraints, 2009, 14(4): 539–581

[17] Benedetti M, Lallouet A, Vautard J. Modeling adversary scheduling with QCSP+. In: Proceedings of the 2008 ACM Symposium on Applied Computing. 2008, 151–155

[18] Verger G, Bessière C. Guiding search in QCSP+ with backpropagation. In: Proceedings of the 14th International Conference on Principles and Practice of Constraint Programming. 2008, 175–189

[19] Verger G, Bessière C. A bottom-up approach for solving quantified CSPs. In: Proceedings of the 12th International Conference on Principles and Practice of Constraint Programming. 2006, 635–649

[20] Lallouet A, Lee J, Mak T W. Consistencies for ultra-weak solutions in minimax weighted CSPs using the duality principle. In: Proceedings of the 18th International Conference on Principles and Practice of Constraint Programming. 2012, 373–389

[21] Lallouet A, Lee J, Mak T W, Yip J. Ultra-weak solutions and consistency enforcement in minimax weighted constraint satisfaction. Constraints, 2015, 20(2): 109–154

[22] Li H, Li Z. A novel strategy of combining variable ordering heuristics for constraint satisfaction problems. IEEE Access, 2018, 6: 42750–42756

[23] Li H, Liang Y, Zhang N, Guo J, Xu D, Li Z. Improving degree-based variable ordering heuristics for solving constraint satisfaction problems. Journal of Heuristics, 2016, 22(2): 125–145

[24] Stergiou K. Preprocessing quantified constraint satisfaction problems with value reordering and directional arc and path consistency. International Journal on Artificial Intelligence Tools, 2008, 17(2): 321–337

[25] Bessière C, Régin J C, Yap R H, Zhang Y. An optimal coarse-grained arc consistency algorithm. Artificial Intelligence, 2015, 165(2): 165–185

[26] Prosser P. Hybrid algorithms for the constraint satisfaction problem. Computational Intelligence, 1993, 9(3): 268–299

[27] Davis M, Putnam H. A computing procedure for quantification theory. Journal of the ACM, 1960, 7(3): 201–215

[28] Davis M, Logemann G, Loveland D. A machine program for theorem proving. Communications of the ACM, 1962, 5(7): 394–397

[29] Bacchus F, Stergiou K. Solution directed backjumping for QCSP. In: Proceedings of the 13th International Conference on Principles and Practice of Constraint Programming. 2007, 148–163

[30] Stynes D, Brown K N. Value ordering for quantified CSPs. Constraints, 2009, 14(1): 16–37

[31] Achlioptas D, Kirousis L M, Kranakis E, Krizanc D, Molloy M, Stamatiou Y C. Random constraint satisfaction: a more accurate picture. In: Proceedings of the 3rd International Conference on Principles and Practice of Constraint Programming. 1997, 107–120

[32] Xu K, Li W. Exact phase transitions in random constraint satisfaction problems. Journal of Artificial Intelligence Research, 2000, 12(1): 93–103

[33] Xu K, Li W. An average analysis of backtracking on random constraint satisfaction problems. Annals of Mathematics and Artificial Intelligence, 2001, 33(1): 21–37

[34] Xu K, Li W. Many hard examples in exact phase transitions. Theoretical Computer Science, 2006, 355(1): 291–302

RIGHTS & PERMISSIONS

2019 Higher Education Press and Springer-Verlag GmbH Germany, part of Springer Nature