Solving CSP Including a Universal Quantification
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.
KeywordsSearch Tree Constraint Satisfaction Problem Memory Consumption Conjunctive Normal Form Good Representative
Unable to display preview. Download preview PDF.
- 3.Boris, B.: Black-box testing - Techniques for functional testing of software and systems. John Wiley & Sons, Chichester (1995)Google Scholar
- 4.Golden, K., Frank, J.: Universal quantification in a constraint-based planner. In: AIPS 2002 (2002)Google Scholar
- 5.Van Roy, P., Haridi, S.: Concepts, Techniques, and Models of Computer Programming. MIT Press, Cambridge (2004) ISBN 0-262-22069-5Google Scholar