Sciweavers

SAT
2005
Springer

Optimizations for Compiling Declarative Models into Boolean Formulas

13 years 9 months ago
Optimizations for Compiling Declarative Models into Boolean Formulas
Advances in SAT solver technology have enabled many automated analysis and reasoning tools to reduce their input problem to a SAT problem, and then to use an efficient SAT solver to solve the underlying analysis or reasoning problem. The solving time for SAT solvers can vary substantially for semantically identical SAT problems depending on how the problem is expressed. This property motivates the development of new optimization techniques whose goal is to produce more efficiently solvable SAT problems, thereby improving the overall performance of the analysis or reasoning tool. This paper presents our experience using several mechanical techniques that enable the Alloy Analyzer to generate optimized SAT formulas from first-order logic formulas. These techniques are inspired by similar techniques from the field of optimizing compilers, suggesting the potential presence of underlying connections between optimization problems from two very different domains. Our experimental results ...
Darko Marinov, Sarfraz Khurshid, Suhabe Bugrara, L
Added 28 Jun 2010
Updated 28 Jun 2010
Type Conference
Year 2005
Where SAT
Authors Darko Marinov, Sarfraz Khurshid, Suhabe Bugrara, Lintao Zhang, Martin C. Rinard
Comments (0)