Solving CSP including a universal quantification

De Landtsheer, Renaud
(2005) 2nd International Conference Multiparadigm Programming in Mozart/Oz — Location: Charleroi(Belgium) (7.October.2004)

Files

pdfdocument.pdf
  • Restricted Access
  • Adobe PDF
  • 279.42 KB
Request a copy

Details

Authors
  • De Landtsheer, RenaudUCLouvain
    Author
Abstract
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.
Affiliations

Citations

  • APA
  • Chicago
  • FWB

De Landtsheer, R. (2005). Solving CSP including a universal quantification. Lecture Notes in Computer Science, 3389, 200-210. https://doi.org/10.1007/978-3-540-31845-3_17 (Original work published 2005)