×

zbMATH — the first resource for mathematics

Stochastic local search for SMT: combining theory solvers with WalkSAT. (English) Zbl 1348.68227
Tinelli, Cesare (ed.) et al., Frontiers of combining systems. 8th international symposium, FroCoS 2011, Saarbrücken, Germany, October 5–7, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-24363-9/pbk). Lecture Notes in Computer Science 6989. Lecture Notes in Artificial Intelligence, 163-178 (2011).
Summary: 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}\) (\(\mathcal{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 \(\mathcal{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 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.
For the entire collection see [Zbl 1223.68012].

MSC:
68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
Software:
MathSAT; UBCSAT
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] http://disi.unitn.it/ rseba/frocos11/tests.tar.gz
[2] Armando, A., Castellini, C., Giunchiglia, E.: SAT-based procedures for temporal reasoning. In: Proc. European Conference on Planning, CP 1999 (1999) · Zbl 1098.68693
[3] 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) · Zbl 1072.68562 · doi:10.1007/3-540-45620-1_17
[4] 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) · Zbl 1306.68138 · doi:10.1007/978-3-642-16242-8_34
[5] 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)
[6] 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) · Zbl 05576291 · doi:10.1007/978-3-642-02777-2_25
[7] 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) · Zbl 05301118 · doi:10.1007/978-3-540-70545-1_28
[8] 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) · Zbl 1187.68537 · doi:10.1007/11814948_19
[9] 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) · Zbl 05187406 · doi:10.1007/11817963_11
[10] Hoos, H.H., Stutzle, T.: Local Search Algorithms for SAT: An Empirical Evaluation. Journal of Automated Reasoning 24(4) (2000) · Zbl 0961.68039 · doi:10.1023/A:1006350622830
[11] Hoos, H.H., Stutzle, T.: Stochastic Local Search Foundation And Application. Morgan Kaufmann, San Francisco (2005)
[12] 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) · Zbl 0782.90054 · doi:10.1016/0004-3702(92)90007-K
[13] Sebastiani, R.: Lazy Satisfiability Modulo Theories. Journal on Satisfiability, Boolean Modeling and Computation, JSAT 3 (2007) · Zbl 1145.68501
[14] Selman, B., Kautz, H.A., Cohen, B.: Noise strategies for improving local search. In: Proc. AAAI. MIT Press, Cambridge (1994) · Zbl 0864.90093
[15] Tomasi, S.: Stochastic Local Search for SMT. Technical report, DISI-10-060, DISI, University of Trento (2010), http://eprints.biblio.unitn.it/
[16] Tompkins, D., Hoos, H.: Novelty+ and Adaptive Novelty+. In: SAT 2004 Competition Booklet (2004)
[17] 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) · Zbl 1122.68620 · doi:10.1007/11527695_24
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.