Stochastic Local Search for SMT: A Preliminary Report

A popular approach to SMT is based on the integration of a DPLL 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 outperform DPLL on satisfiable instances, in particular when dealing with unstructured problems. Therefore, it is a natural research question to wonder whether SLS can be exploited successfully also inside SMT tools. The purpose of this paper is to start investigating this issue. First, we present an algorithm integrating a Boolean SLS solver (based on the WalkSAT paradigm) with a T-solver, resulting in a basic SLS-based SMT solver. Second, we introduce a group of techniques aimed at improving the synergy between the Boolean and the T-specific component, and discuss the differences between the integration of T-solvers with a DPLL-based and a SLS-based SAT solver. Finally, we perform a preliminary experimental evaluation of our implementation (based on the integration of the UBCSAT SLS platform with the LA(Q)-solver of MathSAT) by comparing it against MathSAT, a state-of-the-art DPLL-based SMT solver, on both structured industrial problems coming from the SMT-LIB and randomly-generated unstructured problems. From this preliminary analysis we have that the performance of the SLS-based tool (i) is far from that of the DPLL-based one on SMT-LIB problems and (ii) is comparable on random problems.