Optimizations for compiling declarative models into boolean formulas

SAT'05 Proceedings of the 8th international conference on Theory and Applications of Satisfiability Testing(2005)

引用 31|浏览0
暂无评分
摘要
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 show that our techniques can deliver substantial performance improvement results—in some cases, they reduce the solving time by an order of magnitude.
更多
查看译文
关键词
sat solver technology,semantically identical sat problem,reasoning tool,sat solvers,sat problem,declarative model,solvable sat problem,efficient sat solver,optimization problem,sat formula,input problem,boolean formula,optimizing compiler,first order logic,sat solver
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要