Generalizing consistency and other constraint properties to quantified constraints

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Generalizing consistency and other constraint properties to quantified constraints

Full text

Pdf (220 KB)

Source

ACM Transactions on Computational Logic (TOCL) archive
Volume 10 , Issue 3 (April 2009) table of contents

Article No. 17

Year of Publication: 2009

ISSN:1529-3785

Authors

Lucas Bordeaux	Microsoft Research, Cambridge, United Kingdom
Marco Cadoli	Università di Roma “La Sapienza”, Rome, Italy
Toni Mancini	Università di Roma “La Sapienza”, Rome, Italy

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 7, Downloads (12 Months): 65, Citation Count: 1

Additional Information:

appendices and supplements abstract references cited by index terms collaborative colleagues

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/1507244.1507247 What is a DOI?

APPENDICES and SUPPLEMENTS

Bordeaux Appendix

Online appendix to generalizing consistency and other constraint properties to quantified constraints. The appendix supports the information on article 17.

ABSTRACT

Quantified constraints and Quantified Boolean Formulae are typically much more difficult to reason with than classical constraints, because quantifier alternation makes the usual notion of solution inappropriate. As a consequence, basic properties of Constraint Satisfaction Problems (CSPs), such as consistency or substitutability, are not completely understood in the quantified case. These properties are important because they are the basis of most of the reasoning methods used to solve classical (existentially quantified) constraints, and it is desirable to benefit from similar reasoning methods in the resolution of quantified constraints.

In this article, we show that most of the properties that are used by solvers for CSP can be generalized to quantified CSP. This requires a rethinking of a number of basic concepts; in particular, we propose a notion of outcome that generalizes the classical notion of solution and on which all definitions are based. We propose a systematic study of the relations which hold between these properties, as well as complexity results regarding the decision of these properties. Finally, and since these problems are typically intractable, we generalize the approach used in CSP and propose weaker, easier to check notions based on locality, which allow to detect these properties incompletely but in polynomial time.

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	Ansótegui, C., Gomes, C. P., and Selman, B. 2005. The Achilles' heel of QBF. In Proceedings of the American Conference on Artificial Intelligence (AAAI). AAAI Press, 275--281.
	2	Audemard, G., Jabbour, S., and Saïs, L. 2007. Symmetry breaking in quantified Boolean formulae. In Proceedings of the International Joint Conference on Artificial Intelligence (IJCAI). Morgan Kaufmann, 2262--2267.
	3	Bacchus, F. and Stergiou, K. 2007. Solution directed backjumping for QCSP. In Proceedings of the International Conference on Principles and Practice of Constraint Programming (CP). Springer, 148--163.
	4	Benedetti, M. 2004. Evaluating QBF via symbolic skolemization. In Proceedings of the Internationl Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR). Springer, 285--300.
	5	Benedetti, M., Lallouet, A., and Vautard, J. 2007. QCSP made practical by virtue of restricted quantification. In Proceedings of the International Joint Conference on Artificial Intelligence (IJCAI). Morgan Kaufmann, 38--43.
	6	Bordeaux, L., Cadoli, M., and Mancini, T. 2004. Exploiting fixable, removable and determined values in constraint satisfaction problems. In Proceedings of the International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR). Springer, 270--284.
	7	Bordeaux, L., Cadoli, M., and Mancini, T. 2005. CSP properties for quantified constraints: Definitions and complexity. In Proceedings of the American Conference on Artificial Intelligence (AAAI). AAAI Press, 360--365.
	8	Lucas Bordeaux , Eric Monfroy, Beyond NP: Arc-Consistency for Quantified Constraints, Proceedings of the 8th International Conference on Principles and Practice of Constraint Programming, p.371-386, September 09-13, 2002
	9	Lucas Bordeaux , Lintao Zhang, A solver for quantified Boolean and linear constraints, Proceedings of the 2007 ACM symposium on Applied computing, March 11-15, 2007, Seoul, Korea [doi>10.1145/1244002.1244078]
	10	Börner, F., Bulatov, A., Jeavons, P., and Krokhin, A. 2003. Quantified constraints: Algorithms and complexity. In Proceedings of the International Conference on Computer Science Logic (CSL). Springer, 58--70.
	11	Hans Kleine Büning , Marek Karpinski , Andreas Flögel, Resolution for quantified Boolean formulas, Information and Computation, v.117 n.1, p.12-18, Feb. 15, 1995 [doi>10.1006/inco.1995.1025]
	12	Marco Cadoli , Andrea Giovanardi , Marco Schaerf, An algorithm to evaluate quantified Boolean formulae, Proceedings of the fifteenth national/tenth conference on Artificial intelligence/Innovative applications of artificial intelligence, p.262-267, July 1998, Madison, Wisconsin, United States
	13	Marco Cadoli , Marco Schaerf , Andrea Giovanardi , Massimo Giovanardi, An Algorithm to Evaluate Quantified Boolean Formulae and Its Experimental Evaluation, Journal of Automated Reasoning, v.28 n.2, p.101-142, February 2002 [doi>10.1023/A:1015019416843]
	14	Chen, H. 2004a. Collapsibility and consistency in quantified constraint satisfaction. In Proceedings of the American Conference on Artificial Intelligence (AAAI). AAAI Press, 155--160.
	15	Chen, H. 2004b. Quantified constraint satisfaction and bounded treewidth. In Proceedings of the European Conference on Artificial Intelligence (ECAI). IOS Press, 161--165.
	16	Ferguson, A. and O'Sullivan, B. 2007. Quantified constraint satisfaction problems: From relaxations to explanations. In Proceedings of the International Joint Conference on Artificial Intelligence (IJCAI). Morgan Kaufmann, 74--79.
	17	Fischer, M. J. and Rabin, M. O. 1974. Super-Exponential complexity of presburger arithmetics. In Complexity of Computation, R. Karp, Ed. 27--41.
	18	Freuder, E. C. 1991. Eliminating interchangeable values in constraint satisfaction problems. In Proceedings of the American Conference on Artificial Intelligence (AAAI). AAAI Press, 227--233.
	19	Gent, I., Nightingale, P., and Stergiou, K. 2005. QCSP-Solve: A solver for quantified constraint satisfaction problems. In Proceedings of the International Joint Conference on Artificial Intelligence (IJCAI). Morgan Kaufmann, 138--143.
	20	Gent, I. P., Nightingale, P., and Rowley, A. 2004. Encoding quantified CSPs as quantified Boolean formulae. In Proceedings of the European Conference on Artificial Intelligence (ECAI). IOS Press, 176--180.
	21	Mackworth, A. 1977. Consistency in networks of relations. Artif. Intell. 8, 99--118.
	22	Mamoulis, N. and Stergiou, K. 2004. Algorithms for quantified constraint satisfaction problems. Tech. rep. APES-79-2004, Apes Research Group.
	23	Monasson, R., Zecchina, R., Kirkpatrick, S., Selman, B., and Troyansky, L. 1999. Determining computational complexity from characteristic ‘phase transitions’. Nature 400, 133--137.
	24	Nightingale, P. 2005. Consistency for quantified constraint satisfaction problems. In Proceedings of the International Conference on Principles and Practice of Constraint Programming (CP). Springer, 792--796.
	25	Nightingale, P. 2007. Consistency and the quantified constraint satisfaction problem. Ph.D. thesis, University of St Andrews.
	26	Papadimitriou, C. H. 1994. Computational Complexity. Addison Wesley.
	27	Jussi Rintanen, Improvements to the Evaluation of Quantified Boolean Formulae, Proceedings of the Sixteenth International Joint Conference on Artificial Intelligence, p.1192-1197, July 31-August 06, 1999
	28	Samulowitz, H. and Bacchus, F. 2006. Binary clause reasoning in QBF. In Proceedings of the International Conference on Theory and Applications of Satisfiability Testing (SAT). Springer, 353--367.
	29	Samulowitz, H., Davies, J., and Bacchus, F. 2006. Preprocessing QBF. In Proceedings of the International Conference on Principles and Practice of Constraint Programming (CP). Springer, 514--529.
	30	Stockmeyer, L. J. 1976. The polynomial-time hierarchy. Theor. Comput. Sci. 3, 1, 1--22.
	31	L. J. Stockmeyer , A. R. Meyer, Word problems requiring exponential time(Preliminary Report), Proceedings of the fifth annual ACM symposium on Theory of computing, p.1-9, April 30-May 02, 1973, Austin, Texas, United States [doi>10.1145/800125.804029]
	32	Verger, G. and Bessière, C. 2006. A bottom-up approach for solving quantified CSPs. In Proceedings of the International Conference on Principles and Practice of Constraint Programming (CP). Springer, 635--649.
	33	Zhang, L. 2006. Solving QBF by combining conjunctive and disjunctive normal forms. In Proceedings of the American Conference on Artificial Intelligence (AAAI).