Solving CSP Including a Universal Quantification

  • Renaud De Landtsheer
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3389)


This paper presents a method to solve constraint satisfaction problems including a universally quantified variable with finite domain. Similar problems appear in the field of bounded model checking. The presented method is built on top of the Mozart constraint programming platform. The main principle of the algorithm is to consider only representative values in the domain of the quantified variable. The presented algorithm is similar to a branch and bound search. Significant improvements have been achieved both in memory consumption and execution time compared to a naive approach.


Search Tree Constraint Satisfaction Problem Memory Consumption Conjunctive Normal Form Good Representative 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Benhamou, F., Goualard, F.: Universally quantified interval constraints. In: Dechter, R. (ed.) CP 2000. LNCS, vol. 1894, pp. 67–82. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  2. 2.
    Biere, A., Cimatti, A., Clarke, E.M., Fujita, M., Zhu, Y.: Symbolic model checking using sat procedures instead of bdds. In: Proceedings of the 36th ACM/IEEE conference on Design automation, New Orleans, Louisiana, United States, pp. 317–320. ACM Press, New York (1999)CrossRefGoogle Scholar
  3. 3.
    Boris, B.: Black-box testing - Techniques for functional testing of software and systems. John Wiley & Sons, Chichester (1995)Google Scholar
  4. 4.
    Golden, K., Frank, J.: Universal quantification in a constraint-based planner. In: AIPS 2002 (2002)Google Scholar
  5. 5.
    Van Roy, P., Haridi, S.: Concepts, Techniques, and Models of Computer Programming. MIT Press, Cambridge (2004) ISBN 0-262-22069-5Google Scholar
  6. 6.
    Schulte, C.: Programming Constraint Services. LNCS (LNAI), vol. 2302. Springer, Heidelberg (2002)zbMATHCrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Renaud De Landtsheer
    • 1
  1. 1.Département d’Ingéniérie InformatiqueUCLBelgium

Personalised recommendations