Sciweavers

FROCOS
2011
Springer

Stochastic Local Search for SMT: Combining Theory Solvers with WalkSAT

12 years 3 months ago
Stochastic Local Search for SMT: Combining Theory Solvers with WalkSAT
A dominant approach to Satisfiability Modulo Theories (SMT) relies on the integration of a Conflict-Driven-Clause-Learning (CDCL) SAT solver and of a decision procedure able to handle sets of atomic constraints in the underlying theory T (T -solver). In pure SAT, however, Stochastic Local-Search (SLS) procedures sometimes are competitive with CDCL SAT solvers on satisfiable instances. Thus, it is a natural research question to wonder whether SLS can be exploited successfully also inside SMT tools. In this paper we investigate this issue. We first introduce a general procedure for integrating a SLS solver of the WalkSAT family with a T -solver. Then we present a group of techniques aimed at improving the synergy between these two components. Finally we implement all these techniques into a novel SLSbased SMT solver for the theory of linear arithmetic over the rationals, combining UBCSAT/UBCSAT++ and MathSAT, and perform an empirical evaluation on satisfiable instances. The results ...
Alberto Griggio, Quoc-Sang Phan, Roberto Sebastian
Added 22 Dec 2011
Updated 22 Dec 2011
Type Journal
Year 2011
Where FROCOS
Authors Alberto Griggio, Quoc-Sang Phan, Roberto Sebastiani, Silvia Tomasi
Comments (0)