×

zbMATH — the first resource for mathematics

Propagation based local search for bit-precise reasoning. (English) Zbl 1377.68134
Summary: Many applications of computer-aided verification require bit-precise reasoning as provided by satisfiability modulo theories (SMT) solvers for the theory of quantifier-free fixed-size bit-vectors. The current state-of-the-art in solving bit-vector formulas in SMT relies on bit-blasting, where a given formula is eagerly translated into propositional logic (SAT) and handed to an underlying SAT solver. Bit-blasting is efficient in practice, but may not scale if the input size can not be reduced sufficiently during preprocessing. A recent score-based local search approach lifts stochastic local search from the bit-level (SAT) to the word-level (SMT) without bit-blasting and proved to be quite effective on hard satisfiable instances, particularly in the context of symbolic execution. However, it still relies on brute-force randomization and restarts to achieve completeness. Guided by a completeness proof, we simplified, extended and formalized our propagation-based variant of this approach. We obtained a clean, simple and more precise algorithm that does not rely on score-based local search techniques and does not require brute-force randomization or restarts to achieve completeness. It further yields substantial gain in performance. In this article, we present and discuss our complete propagation based local search approach for bit-vector logics in SMT in detail. We further provide an extended and extensive experimental evaluation including an analysis of randomization effects.

MSC:
68Q60 Specification and verification (program logics, model checking, etc.)
03B70 Logic in computer science
68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Balint A, Belov A, Heule MJH, Järvisalo M (eds) (2013) SAT competition 2013, Department of Computer Science Series of Publications B, vol B-2013-1. University of Helsinki
[2] Balint, A; Belov, A; Järvisalo, M; Sinz, C, Overview and analysis of the SAT challenge 2012 solver competition, Artif Intell, 223, 120-155, (2015)
[3] Balint A, Schöning U (2012) Choosing probability distributions for stochastic local search and the role of make versus break. In: SAT, Lecture Notes in Computer Science, vol 7317, pp 16-29. Springer · Zbl 1273.68333
[4] Barrett C, Conway CL, Deters M, Hadarean L, Jovanovic D, King T, Reynolds A, Tinelli C (2011) CVC4. In: CAV, Lecture Notes in Computer Science, vol 6806, pp 171-177. Springer
[5] Barrett C, Fontaine P, Tinelli C (2015) The SMT-LIB standard: version 2.5. Technical report, Department of Computer Science, The University of Iowa. https://www.SMT-LIB.org
[6] Barrett C, Stump A, Tinelli C (2010) SMT-LIB. https://www.SMT-LIB.org · Zbl 1182.68272
[7] Belov A, Heule MJH, Järvisalo M (eds) (2014) SAT competition 2014, Department of Computer Science Series of Publications B, vol B-2014-2. University of Helsinki
[8] Biere A (2016) Splatz, Lingeling, Plingeling, Treengeling, YalSAT Entering the SAT Competition 2016. In: SAT competition 2016—solver and benchmark descriptions, Department of Computer Science Series of Publications B, vol B-2016-1, pp 44-45. University of Helsinki
[9] Brummayer R (2009) Efficient SMT solving for bit-vectors and the extensional theory of arrays. Ph.D. thesis, Johannes Kepler University Linz · Zbl 1187.68168
[10] Bruttomesso R (2008) RTL verification: from SAT to SMT(BV). Ph.D. thesis, University of Trento
[11] Bruttomesso R, Cimatti A, Franzén A, Griggio A, Hanna Z, Nadel A, Palti A, Sebastiani R (2007) A lazy and layered SMT(BV) solver for hard industrial verification problems. In: CAV, Lecture Notes in Computer Science, vol 4590, pp 547-560. Springer
[12] Bruttomesso R, Pek E, Sharygina N, Tsitovich A (2010) The OpenSMT solver. In: TACAS, Lecture Notes in Computer Science, vol 6015, pp 150-153. Springer
[13] Cimatti A, Griggio A, Schaafsma BJ, Sebastiani R (2013) The MathSAT5 SMT solver. In: TACAS, Lecture Notes in Computer Science, vol 7795, pp 93-107. Springer · Zbl 1381.68153
[14] de Moura LM, Bjørner N (2008) Z3: an efficient SMT solver. In: TACAS, Lecture Notes in Computer Science, vol 4963, pp 337-340. Springer
[15] de Moura LM, Jovanovic D (2013) A model-constructing satisfiability calculus. In: VMCAI, Lecture Notes in Computer Science, vol 7737, pp 1-12. Springer · Zbl 1426.68251
[16] Dutertre B (2014) Yices 2.2. In: CAV, Lecture Notes in Computer Science, vol 8559, pp 737-744. Springer
[17] Franzen A (2010) Efficient solving of the satisfiability modulo bit-vectors problem and some extensions to SMT. Ph.D. thesis, University of Trento
[18] Fröhlich A, Biere A, Wintersteiger CM, Hamadi Y (2015) Stochastic local search for satisfiability modulo theories. In: Bonet B, Koenig S (eds) Proceedings of the twenty-ninth AAAI conference on artificial intelligence, Jan 25-30, 2015, Austin, Texas, USA, pp 1136-1143. AAAI Press
[19] Ganesh V (2007) Decision procedures for bit-vectors, arrays and integers. Ph.D. thesis, Stanford University
[20] Ganesh V, Dill DL (2007) A decision procedure for bit-vectors and arrays. In: CAV, Lecture Notes in Computer Science, vol 4590, pp 519-531. Springer · Zbl 1135.68472
[21] Godefroid P, Levin MY, Molnar DA (2008) Automated whitebox fuzz testing. In: NDSS. The Internet Society
[22] Goel, P, An implicit enumeration algorithm to generate tests for combinational logic circuits, IEEE Trans Comput, 30, 215-222, (1981) · Zbl 0455.94038
[23] Griggio A, Phan Q, Sebastiani R, Tomasi S (2011) Stochastic local search for SMT: combining theory solvers with walksat. In: FroCoS, Lecture Notes in Computer Science, vol 6989, pp 163-178. Springer · Zbl 1348.68227
[24] Hadarean L, Bansal K, Jovanovic D, Barrett C, Tinelli C (2014) A tale of two solvers: eager and lazy approaches to bit-vectors. In: CAV, Lecture Notes in Computer Science, vol 8559, pp 680-695. Springer
[25] Hansen TA (2012) A constraint solver and its application to machine code test generation. Ph.D. thesis, University of Melbourne
[26] Hoos HH (1999) On the run-time behaviour of stochastic local search algorithms for SAT. In: AAAI/IAAI, pp 661-666. AAAI Press/The MIT Press
[27] Huang C, Cheng K (2000) Assertion checking by combined word-level ATPG and modular arithmetic constraint-solving techniques. In: DAC, pp 118-123
[28] Iyer MA (2003) Race: a word-level ATPG-based constraints solver system for smart random simulation. In: ITC, pp 299-308. IEEE Computer Society
[29] Jovanović D, Barrett C, de Moura L (2013) The design and implementation of the model constructing satisfiability calculus. In: Formal methods in computer-aided design, FMCAD 2013, Portland, OR, USA, Oct 20-23, 2013, pp 173-180. IEEE
[30] Kroening D, Strichman O (2008) Decision procedures—an algorithmic point of view. Texts in theoretical computer science. An EATCS series. Springer, Heidelberg · Zbl 1149.68071
[31] Kuehlmann, A; Paruthi, V; Krohm, F; Ganai, MK, Robust Boolean reasoning for equivalence checking and functional property verification, IEEE Trans CAD Integr Circuits Syst, 21, 1377-1394, (2002)
[32] Kunz W, Stoffel D (1997) Reasoning in Boolean networks: logic synthesis and verification using testing techniques. Kluwer Academic Publishers, Norwell · Zbl 0884.68007
[33] Naveh, Y; Rimon, M; Jaeger, I; Katz, Y; Vinov, M; Marcus, E; Shurek, G, Constraint-based random stimuli generation for hardware verification, AI Mag, 28, 13-30, (2007)
[34] Niemetz, A; Preiner, M; Biere, A, Boolector 2.0, JSAT, 9, 53-58, (2015)
[35] Niemetz A, Preiner M, Biere A (2016) Precise and complete propagation based local search for satisfiability modulo theories. In: CAV (1), Lecture Notes in Computer Science, vol 9779, pp 199-217. Springer · Zbl 1377.68134
[36] Niemetz A, Preiner M, Biere A, Fröhlich A (2015) Improving local search for bit-vector logics in SMT with path propagation. In: DIFTS@FMCAD, pp 1-10
[37] Selman B, Kautz HA, Cohen B (1994) Noise strategies for improving local search. In: AAAI, pp 337-343. AAAI Press/The MIT Press
[38] Tillmann N, Schulte W (2005) Parameterized unit tests. In: ESEC/SIGSOFT FSE, pp 253-262. ACM
[39] Xu, L; Hutter, F; Hoos, HH; Leyton-Brown, K, Satzilla: portfolio-based algorithm selection for SAT, J Artif Intell Res (JAIR), 32, 565-606, (2008) · Zbl 1182.68272
[40] Yuan J, Pixley C, Aziz A (2006) Constraint-based verification. Springer, Berlin · Zbl 1093.68058
[41] Zeljic A, Wintersteiger CM, Rümmer P (2016) Deciding bit-vector formulas with mcSAT. In: SAT, Lecture Notes in Computer Science, vol 9710, pp 249-266. Springer · Zbl 06623516
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.