{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:34:30Z","timestamp":1750307670980,"version":"3.41.0"},"reference-count":32,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2009,4,1]],"date-time":"2009-04-01T00:00:00Z","timestamp":1238544000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2009,4]]},"abstract":"<jats:p>\n            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\n            <jats:italic>solution<\/jats:italic>\n            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.\n          <\/jats:p>\n          <jats:p>\n            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\n            <jats:italic>outcome<\/jats:italic>\n            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\n            <jats:italic>locality<\/jats:italic>\n            , which allow to detect these properties incompletely but in polynomial time.\n          <\/jats:p>","DOI":"10.1145\/1507244.1507247","type":"journal-article","created":{"date-parts":[[2009,4,15]],"date-time":"2009-04-15T13:37:07Z","timestamp":1239802627000},"page":"1-25","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Generalizing consistency and other constraint properties to quantified constraints"],"prefix":"10.1145","volume":"10","author":[{"given":"Lucas","family":"Bordeaux","sequence":"first","affiliation":[{"name":"Microsoft Research, Cambridge, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marco","family":"Cadoli","sequence":"additional","affiliation":[{"name":"Universit\u00e0 di Roma \u201cLa Sapienza\u201d, Rome, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Toni","family":"Mancini","sequence":"additional","affiliation":[{"name":"Universit\u00e0 di Roma \u201cLa Sapienza\u201d, Rome, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2009,4,8]]},"reference":[{"volume-title":"Proceedings of the American Conference on Artificial Intelligence (AAAI). AAAI Press, 275--281","author":"Ans\u00f3tegui C.","key":"e_1_2_2_1_1","unstructured":"Ans\u00f3tegui , 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 . Ans\u00f3tegui, 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."},{"volume-title":"Proceedings of the International Joint Conference on Artificial Intelligence (IJCAI). Morgan Kaufmann, 2262--2267","author":"Audemard G.","key":"e_1_2_2_2_1","unstructured":"Audemard , G. , Jabbour , S. , and Sa\u00efs , L . 2007. Symmetry breaking in quantified Boolean formulae . In Proceedings of the International Joint Conference on Artificial Intelligence (IJCAI). Morgan Kaufmann, 2262--2267 . Audemard, G., Jabbour, S., and Sa\u00efs, L. 2007. Symmetry breaking in quantified Boolean formulae. In Proceedings of the International Joint Conference on Artificial Intelligence (IJCAI). Morgan Kaufmann, 2262--2267."},{"volume-title":"Proceedings of the International Conference on Principles and Practice of Constraint Programming (CP). Springer, 148--163","author":"Bacchus F.","key":"e_1_2_2_3_1","unstructured":"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 . 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."},{"key":"e_1_2_2_4_1","volume-title":"Proceedings of the Internationl Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR). Springer, 285--300","author":"Benedetti M.","year":"2004","unstructured":"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 . 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."},{"volume-title":"Proceedings of the International Joint Conference on Artificial Intelligence (IJCAI). Morgan Kaufmann, 38--43","author":"Benedetti M.","key":"e_1_2_2_5_1","unstructured":"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 . 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."},{"volume-title":"Proceedings of the International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR). Springer, 270--284","author":"Bordeaux L.","key":"e_1_2_2_6_1","unstructured":"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 . 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."},{"volume-title":"Proceedings of the American Conference on Artificial Intelligence (AAAI). AAAI Press, 360--365","author":"Bordeaux L.","key":"e_1_2_2_7_1","unstructured":"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 . 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."},{"key":"e_1_2_2_8_1","volume-title":"Beyond NP: Arc-Consistency for quantified constraints. In Proceedings of the International Conference on Principles and Practice of Constraint Programming (CP)","author":"Bordeaux L.","year":"2002","unstructured":"Bordeaux , L. and Monfroy , E . 2002 . Beyond NP: Arc-Consistency for quantified constraints. In Proceedings of the International Conference on Principles and Practice of Constraint Programming (CP) . Springer , 371--386. Bordeaux, L. and Monfroy, E. 2002. Beyond NP: Arc-Consistency for quantified constraints. In Proceedings of the International Conference on Principles and Practice of Constraint Programming (CP). Springer, 371--386."},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1244002.1244078"},{"volume-title":"Proceedings of the International Conference on Computer Science Logic (CSL). Springer, 58--70","author":"B\u00f6rner F.","key":"e_1_2_2_10_1","unstructured":"B\u00f6rner , 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 . B\u00f6rner, 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."},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1995.1025"},{"volume-title":"Proceedings of the American Conference on Artificial Intelligence (AAAI). AAAI\/MIT Press, 262--267","author":"Cadoli M.","key":"e_1_2_2_12_1","unstructured":"Cadoli , M. , Giovanardi , A. , and Schaerf , M . 1999. An algorithm to evaluate quantified Boolean formulae . In Proceedings of the American Conference on Artificial Intelligence (AAAI). AAAI\/MIT Press, 262--267 . Cadoli, M., Giovanardi, A., and Schaerf, M. 1999. An algorithm to evaluate quantified Boolean formulae. In Proceedings of the American Conference on Artificial Intelligence (AAAI). AAAI\/MIT Press, 262--267."},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1015019416843"},{"key":"e_1_2_2_14_1","volume-title":"Proceedings of the American Conference on Artificial Intelligence (AAAI). AAAI Press, 155--160","author":"Chen H.","year":"2004","unstructured":"Chen , H. 2004 a. Collapsibility and consistency in quantified constraint satisfaction . In Proceedings of the American Conference on Artificial Intelligence (AAAI). AAAI Press, 155--160 . Chen, H. 2004a. Collapsibility and consistency in quantified constraint satisfaction. In Proceedings of the American Conference on Artificial Intelligence (AAAI). AAAI Press, 155--160."},{"key":"e_1_2_2_15_1","volume-title":"Proceedings of the European Conference on Artificial Intelligence (ECAI). IOS Press, 161--165","author":"Chen H.","year":"2004","unstructured":"Chen , H. 2004 b. Quantified constraint satisfaction and bounded treewidth . In Proceedings of the European Conference on Artificial Intelligence (ECAI). IOS Press, 161--165 . Chen, H. 2004b. Quantified constraint satisfaction and bounded treewidth. In Proceedings of the European Conference on Artificial Intelligence (ECAI). IOS Press, 161--165."},{"key":"e_1_2_2_16_1","volume-title":"Proceedings of the International Joint Conference on Artificial Intelligence (IJCAI). Morgan Kaufmann, 74--79","author":"Ferguson A.","year":"2007","unstructured":"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 . 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."},{"key":"e_1_2_2_17_1","unstructured":"Fischer M. J. and Rabin M. O. 1974. Super-Exponential complexity of presburger arithmetics. In Complexity of Computation R. Karp Ed. 27--41.  Fischer M. J. and Rabin M. O. 1974. Super-Exponential complexity of presburger arithmetics. In Complexity of Computation R. Karp Ed. 27--41."},{"key":"e_1_2_2_18_1","volume-title":"Proceedings of the American Conference on Artificial Intelligence (AAAI). AAAI Press, 227--233","author":"Freuder E. C.","year":"1991","unstructured":"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 . 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."},{"volume-title":"Proceedings of the International Joint Conference on Artificial Intelligence (IJCAI). Morgan Kaufmann, 138--143","author":"Gent I.","key":"e_1_2_2_19_1","unstructured":"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 . 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."},{"volume-title":"Proceedings of the European Conference on Artificial Intelligence (ECAI). IOS Press, 176--180","author":"Gent I. P.","key":"e_1_2_2_20_1","unstructured":"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 . 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."},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/0004-3702(77)90007-8"},{"key":"e_1_2_2_22_1","doi-asserted-by":"crossref","unstructured":"Mamoulis N. and Stergiou K. 2004. Algorithms for quantified constraint satisfaction problems. Tech. rep. APES-79-2004 Apes Research Group.  Mamoulis N. and Stergiou K. 2004. Algorithms for quantified constraint satisfaction problems. Tech. rep. APES-79-2004 Apes Research Group.","DOI":"10.1007\/978-3-540-30201-8_60"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1038\/22055"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/11564751_66"},{"volume-title":"Computational Complexity","author":"Papadimitriou C. H.","key":"e_1_2_2_26_1","unstructured":"Papadimitriou , C. H. 1994. Computational Complexity . Addison Wesley . Papadimitriou, C. H. 1994. Computational Complexity. Addison Wesley."},{"key":"e_1_2_2_27_1","volume-title":"Proceedings of the International Joint Conference on Artificial Intelligence (IJCAI). Morgan Kaufmann, 1192--1197","author":"Rintanen J.","year":"1999","unstructured":"Rintanen , J. 1999 . Improvements to the Evaluation of quantified Boolean formulae . In Proceedings of the International Joint Conference on Artificial Intelligence (IJCAI). Morgan Kaufmann, 1192--1197 . Rintanen, J. 1999. Improvements to the Evaluation of quantified Boolean formulae. In Proceedings of the International Joint Conference on Artificial Intelligence (IJCAI). Morgan Kaufmann, 1192--1197."},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/11814948_33"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/11889205_37"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(76)90061-X"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/800125.804029"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/11889205_45"},{"key":"e_1_2_2_33_1","volume-title":"Proceedings of the American Conference on Artificial Intelligence (AAAI).","author":"Zhang L.","year":"2006","unstructured":"Zhang , L. 2006 . Solving QBF by combining conjunctive and disjunctive normal forms . In Proceedings of the American Conference on Artificial Intelligence (AAAI). Zhang, L. 2006. Solving QBF by combining conjunctive and disjunctive normal forms. In Proceedings of the American Conference on Artificial Intelligence (AAAI)."}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1507244.1507247","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1507244.1507247","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T13:29:37Z","timestamp":1750253377000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1507244.1507247"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,4]]},"references-count":32,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2009,4]]}},"alternative-id":["10.1145\/1507244.1507247"],"URL":"https:\/\/doi.org\/10.1145\/1507244.1507247","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2009,4]]},"assertion":[{"value":"2007-05-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2008-04-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2009-04-08","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}