A solver for quantified Boolean and linear constraints

ABSTRACT

We make a number of contributions to the understanding and practical resolution of quantified constraints. Unlike previous work in the CP literature that was essentially focused on constraints expressed as binary tables, we focus on Presburger Arithmetics, i.e., Boolean combinations of linear constraints. From a theoretical perspective, we clarify the problem of the treatment of universal quantifiers by proposing a "symmetric" version of the notion of quantified consistency. This notion imposes to maintain two constraint stores, which will be used to reason on universal and existential variables, respectively. We then describe a branch & bound algorithm that integrates both forms of propagation. Its implementation is, to the best of our knowledge, the first CP solver for this class of quantified constraints.

REFERENCES

• 1: C. Ansótegui, C. P. Gomes, and B. Selman. The Achilles' heel of QBF. In AAAI, pages 275--281, 2005.
• 2: L. Bordeaux, M. Cadoli, and T. Mancini. CSP properties for quantified constraints: Definitions and complexity. In AAAI, pages 360--365, 2005.
• 3: 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
• 4: K. N. Brown, J. Little, P. J. Creed, and E. C. Freuder. Adversarial constraint satisfaction by game-tree search. In ECAI, pages 151--155, 2004.
• 5: H. Chen. Quantified constraint satisfaction and bounded treewidth. In ECAI, pages 161--165, 2004.
• 6: H. Chen and M. Pál. Optimization, games, and quantified constraint satisfaction. In MFCS, pages 239--250, 2004.
• 7: I. P. Gent, P. Nightingale, and K. Stergiou. QCSP-Solve: A solver for quantified constraint satisfaction problems. In IJCAI, pages 138--143, 2005.
• 8: S. Manandhar, A. Tarim, and T. Walsh. Scenario-based stochastic constraint programming. In IJCAI, pages 257--262, 2003.
• 9: P. Nightingale. Consistency for quantified constraint satisfaction problems. In CP Workshop on Quantification in Constraint Programming, 2005.
• 10: C. Otwell, A. Remshagen, and K. Truemper. An effective QBF solver for planning problems. In AMCS, pages 311--316, 2004.
• 11: K. Stergiou. Repair methods for quantified CSPs. In CP, pages 652--666, 2005.
• 12: N. Yorke-Smith and C. Gervet. Certainty closure: a framework for reliable constraint reasoning with uncertainty. In CP, pages 769--783, 2003.
• 13: L. Zhang. Solving QBF by combining conjunctive and disjunctive normal forms. In AAAI, 2006. To appear.

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.m MISCELLANEOUS

Additional Classification:
  G. Mathematics of Computing
  G.m MISCELLANEOUS

General Terms:
Theory