Tuning SMT Solvers for Solving Optimization Problems
Solvers for satisfiability modulo theories (SMT) usually handle decision problems with high efficiency.However,in some applications,it is hopeful for SMT solvers to have the ability to find the best solution.In this paper,we propose a novel method to tune a SMT solver for solving optimization problems.Our inspiration conies from the necessary conditions for extrema of multivariable functions.In our work,such necessary conditions are added to the clause library of the Boolean abstraction of the SMT problem.All extrema are enumerated through the DPLL procedure among which the optimal one can be acquired.The feasibility of the method is demonstrated by experiments.
optimization satisfiability SMT
Xiang Huo Weimin Wu
School of Computer and Information Technology Beijing Jiaotong University,Beijing,China
国际会议
太原
英文
437-441
2011-02-26（万方平台首次上网日期，不代表论文的发表时间）