A Strategy-Parallel SMT Solver

SMT solvers are automated software tools that decide the satisfiability of formulas of first-order logic over various background theories, e.g., linear arithmetic and lists. For instance, the formula x <= y and y <= x + head [0,1,2] and P (f x - f y) and not (P 0) is unsatisfiable over these background theories (why?). Due to substantial performance improvements in recent years, SMT solvers have become valuable tools for verification, optimization and many other applications.

Today, many different SMT solvers have been developed, based on different algorithms that vary considerably in performance. A regular competition evaluates the performance of SMT solvers on a large set of benchmark problems.

In this project, you will identify features of these benchmark problems that allow to predict which SMT solver(s) will perform well on a given problem. Based on your performance predictions, you will implement a strategy-parallel solver that briefly analyzes a problem and applies those SMT solvers that are likely to perform well.

Work environment:
Required knowledge/skills:
Machine learning, first-order logic, basic programming skills
Tjark Weber

Last modified: 2013-03-02