Abstract
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 \(\mathcal{T}\) (\({\ensuremath{\mathcal{T}} }\textit{-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 \({\ensuremath{\mathcal{T}} }\textit{-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 SLS-based 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 confirm the potential of the approach.
A. Griggio is supported by Provincia Autonoma di Trento and the European Community’s FP7/2007-2013 under grant agreement Marie Curie FP7 - PCOFUND-GA-2008-226070 “progetto Trentino”, project ADAPTATION. R. Sebastiani is supported in part by SRC/GRC under Custom Research Project 2009-TJ-1880 WOLFLING. We wish to thank H. Hoos, D. Tompkins, A. Belov and Z. Stachniak for their help with their tools and for useful insights.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Armando, A., Castellini, C., Giunchiglia, E.: SAT-based procedures for temporal reasoning. In: Proc. European Conference on Planning, CP 1999 (1999)
Audemard, G., Bertoli, P., Cimatti, A., Korniłowicz, A., Sebastiani, R.: A SAT Based Approach for Solving Formulas over Boolean and Linear Mathematical Propositions. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol. 2392, pp. 195–210. Springer, Heidelberg (2002)
Audemard, G., Lagniez, J.-M., Mazure, B., Sais, L.: Boosting local search thanks to cdcl. In: Fermüller, C.G., Voronkov, A. (eds.) LPAR-17. LNCS, vol. 6397, pp. 474–488. Springer, Heidelberg (2010)
Barrett, C.W., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability Modulo Theories. In: Handbook of Satisfiability. ch. 26, pp. 825–885. IOS Press, Amsterdam (2009)
Belov, A., Stachniak, Z.: Improving variable selection process in stochastic local search for propositional satisfiability. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584, pp. 258–264. Springer, Heidelberg (2009)
Bruttomesso, R., Cimatti, A., Franzén, A., Griggio, A., Sebastiani, R.: The mathSAT 4 SMT solver. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 299–303. Springer, Heidelberg (2008)
Cotton, S., Maler, O.: Fast and Flexible Difference Constraint Propagation for DPLL(T). In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 170–183. Springer, Heidelberg (2006)
Dutertre, B., de Moura, L.: A Fast Linear-Arithmetic Solver for DPLL(T). In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 81–94. Springer, Heidelberg (2006)
Hoos, H.H., Stutzle, T.: Local Search Algorithms for SAT: An Empirical Evaluation. Journal of Automated Reasoning 24(4) (2000)
Hoos, H.H., Stutzle, T.: Stochastic Local Search Foundation And Application. Morgan Kaufmann, San Francisco (2005)
Minton, S., Johnston, M.D., Philips, A.B., Laird, P.: Minimizing Conflicts: A Heuristic Repair Method for Constraint-Satisfaction and Scheduling Problems. Artificial Intelligence 58(1) (1992)
Sebastiani, R.: Lazy Satisfiability Modulo Theories. Journal on Satisfiability, Boolean Modeling and Computation, JSAT 3 (2007)
Selman, B., Kautz, H.A., Cohen, B.: Noise strategies for improving local search. In: Proc. AAAI. MIT Press, Cambridge (1994)
Tomasi, S.: Stochastic Local Search for SMT. Technical report, DISI-10-060, DISI, University of Trento (2010), http://eprints.biblio.unitn.it/
Tompkins, D., Hoos, H.: Novelty+ and Adaptive Novelty+. In: SAT 2004 Competition Booklet (2004)
Tompkins, D., Hoos, H.: UBCSAT: An Implementation and Experimentation Environment for SLS Algorithms for SAT and MAX-SAT. In: Hoos, H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol. 3542, pp. 306–320. Springer, Heidelberg (2005)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Griggio, A., Phan, QS., Sebastiani, R., Tomasi, S. (2011). Stochastic Local Search for SMT: Combining Theory Solvers with WalkSAT. In: Tinelli, C., Sofronie-Stokkermans, V. (eds) Frontiers of Combining Systems. FroCoS 2011. Lecture Notes in Computer Science(), vol 6989. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-24364-6_12
Download citation
DOI: https://doi.org/10.1007/978-3-642-24364-6_12
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-24363-9
Online ISBN: 978-3-642-24364-6
eBook Packages: Computer ScienceComputer Science (R0)