2016/12/30 by Sebastian Krings, Michael Leuschel, Michaël Leuschel
Computer Science · Mathematics · #Algorithm #Computer science #Constraint (computer-aided design) #Constraint Satisfaction and Optimization #Constraint logic programming #Constraint programming #Constraint satisfaction problem #Discrete mathematics #Enumeration #Formal Methods in Verification #Logic, Reasoning, and Knowledge #Mathematical optimization #Mathematics #Programming language #Set (abstract data type) #Solver #Soundness #Theoretical computer science #cs.LO #cs.PL
paper · pdf · doi:10.4204/eptcs.234.6
published as EPTCS 234, 2017, pp. 73-87 · In Proceedings WLP'15/'16/WFLP'16, arXiv:1701.00148
openalex publication_date 2016/12/30 · arxiv created 2017/01/03 · arxiv updated 2017/01/04 · openalex created_date 2017/01/06 · openalex updated_date 2026/08/05
We present a CLP(FD)-based constraint solver able to deal with unbounded domains. It is based on constraint propagation, resorting to enumeration if all other methods fail. An important aspect is detecting when enumeration was complete and if this has an impact on the soundness of the result. We present a technique which guarantees soundness in the following way: if the constraint solver finds a solution it is guaranteed to be correct; if the constraint solver fails to find a solution it can either return the result "definitely false" in case it knows enumeration was exhaustive, or "unknown" in case it was aborted. The technique can deal with nested universal and existential quantifiers. It can easily be extended to set comprehensions and other operators introducing new quantified variables. We show applications in data validation and proof.