Sciweavers

Share
SAT
2010
Springer

A System for Solving Constraint Satisfaction Problems with SMT

9 years 7 months ago
A System for Solving Constraint Satisfaction Problems with SMT
Abstract. SAT Modulo Theories (SMT) consists of deciding the satisfiability of a formula with respect to a decidable background theory, such as linear integer arithmetic, bit-vectors, etc, in first-order logic with equality. SMT has its roots in the field of verification. It is known that the SAT technology offers an interesting, efficient and scalable method for constraint solving, as many experimentations have shown. Although there already exist some results pointing out the adequacy of SMT techniques for constraint solving, there are no available tools to extensively explore such adequacy. In this paper we introduce a tool for translating FlatZinc (MiniZinc intermediate code) instances of constraint satisfaction problems to the standard SMT-LIB language. It can be used for deciding satisfiability as well as for optimization. The tool determines the required logic for solving each instance. The obtained results suggest that SMT can be effectively used to solve CSPs.
Miquel Bofill, Josep Suy, Mateu Villaret
Added 30 Jan 2011
Updated 30 Jan 2011
Type Journal
Year 2010
Where SAT
Authors Miquel Bofill, Josep Suy, Mateu Villaret
Comments (0)
books