Satisfiability Modulo Theories Sinan Hanay 1 Boolean Satisfiability (SAT) Is there an assignment to the p1, p2, …, pn variables such that evaluates to 1? Slide taken from [Barret09] 2 Satisfiability Modulo Theories (SMT) Is there an assignment to the x,y,z,w variables s.t. evaluates to 1? Slide taken from [Barret09] 3 SAT vs SMT SMT extends SAT solving by adding extensions An SMT solver can solve a SAT problem, but not vice-versa. SMT Applications Analog Circuit Verification RTL Verification Software Model Checking 4 Overview Introduction SMT Theories Example: Difference Logic Combining Theories SMT Solvers and SMT Libraries. Conclusion 5 SMT Theories Real or Integer Arithmetic Equality and Uninterpreted Functions Example: If x1 = x2, then f(x1) = f(x2) else f(x1) ≠ f(x2) Bitvectors and Arrays Properties: Decidable: An effective procedure exists to check if a formula is a member of a theory T. Often Quantifier-free: Free from quantifiers such as (∃, ∀ ) 6 SMT Theories Core Theory Type: Boolean Constants: {TRUE, FALSE} Functions: {AND, OR, XOR} Functions: Implication (=>) Integer Theory (Ints) Type: Int All numerals are Int constants Functions: { + , - , x, mod, div, abs} 7 SMT Theories Reals Theory Type: Real Functions: { +, -, x, / } Functions: { <, > } Arrays with Extentionality Theory (ArraysEx) Type: type of index and type of values Functions: {select, store} 8 Overview Introduction SMT Theories Case Study: Difference Logic Theory SMT Solvers SMT-LIB Conclusion 9 SMT Example I– Difference Logic Can solve problems such as: Is there a solution {x,y} satisfying x-y < 20 and x -y > 4 x,y can be integers or reals If x,y are integers (QF_IDL: Integer Difference Logic) If x,y are reals (QF_RDL : Real Difference Logic) QF: Quantifier-free 10 SMT Theories– Difference Logic In difference logic [NO05], we are interested in the satisfiability of a conjunction of arithmetic atoms. Each atom is of the form x − y OP c, where x and y are variables, c is a numeric constant, and OP ∈ {=,<,≤,>,≥}. Examples: x-y > 10, y-x < 12 The variables can range over either the integers (QF_IDL) or the reals (QF_RDL). Slide taken from [Barret09] 11 Difference Logic The first step is to rewrite everything in terms of ≤: x−y=c⇒x−y≤c∧x−y≥c x − y ≥ c ⇒ y − x ≤ −c x − y > c ⇒ y − x < −c x − y < c ⇒ x − y ≤ c − 1 (integers) x − y < c ⇒ x − y ≤ c − δ (reals) Slide adopted from [Barret09] 12 Difference Logic Now we have a conjunction of literals, all of the form x − y ≤ c. From these literals, we form a weighted directed graph with a vertex for each variable. c For each literal x − y ≤ c, create an edge x y The set of literals is satisfiable iff there is no cycle for which the sum of the weights on the edges is negative. There are a number of efficient algorithms for detecting negative cycles in graphs [CG96]. Slide adopted from [Barret09] 13 Difference Logic x−y = 5 ∧ z −y ≥ 2 ∧ z −x > 2 ∧ w −x = 2 ∧ z −w < 0 1. 2. 3. 4. 5. x− y = 5 z−y≥2 z−x>2 w−x=2 z−w<0 1. Transform to a-b ≤ c Slide adopted from [Barret09] 2. 3. 4. 5. x − y ≤ 5 ∧ y − x ≤ −5 y − z ≤ −2 x − z ≤ −3 w − x ≤ 2 ∧ x − w ≤ −2 z − w ≤ −1 14 Difference Logic Is there a negative cycle? Satisfiable if there is not any. Slide taken from [Barret09] 15 Combining Theories QF_UFLIA 1 ≤ x ∧ x ≤ 2 ∧ f(x) ≠ f(1) ∧ f(x) ≠ f(2) Linear Integer Arithmetic (LIA) Uninterpreted Functions(UF) How to Combine Theory Solvers? 16 Combining Theory Solvers Theory solvers become much more useful if they can be used together. mux_sel = 0 → mux_out = select(regfile, addr) mux_sel = 1 → mux_out = ALU(alu0, alu1) For such formulas, we are interested in satisfiability with respect to a combination of theories. Fortunately, there exist methods for combining theory solvers. The standard technique for this is the Nelson-Oppen method [NO79, TH96]. Slide taken from [Barret09] 17 The Nelson-Oppen Method 1. 2. 3. Suppose that T1 and T2 are theories and that Sat 1 is a theory solver for T1-satisfiability and Sat 2 for T2-satisfiability. We wish to determine if φ is T1∪T2-satisfiable. Convert φ to its separate form φ1 ∧ φ2. Let S be the set of variables shared between φ1 and φ2. For each arrangement D of S: 1. Run Sat 1 on φ1 ∪ D . 2. Run Sat 2 on φ2 ∪ D. Slide taken from [Barret09] 18 Combining Theories QF_UFLIA φ =1 ≤ x ∧ x ≤ 2 ∧ f(x) ≠ f(1) ∧ f(x) ≠ f(2) We first convert φ to a separate form: φUF = f(x) ≠ f(y) ∧ f(x) ≠ f(z) φLIA = 1 ≤ x ∧ x ≤ 2 ∧ y = 1 ∧ z = 2 Slide taken from [Barret09] 19 Combining Theories φUF = f(x) ≠ f(y) ∧ f(x) ≠ f(z) φLIA = 1 ≤ x ∧ x ≤ 2 ∧ y = 1 ∧ z = 2 {x, y, z} can have 5 possible arrangements based on equivalence classes of x, y, and z 1. 2. 3. Assume All Variables Equal: 1. {x = y, x = z, y = z} inconsistent with φUF Assume Two Variables Equal, One Different 1. {x = y, x ≠ z, y ≠ z} inconsistent with φUF 2. {x ≠ y, x = z, y ≠ z} inconsistent with φUF 3. {x ≠ y, x ≠ z, y = z} inconsistent with φLIA Assume All Variables Different: 1. {x ≠ y, x ≠ z, y ≠ z} inconsistent with φLIA Slide adopted from [Barret09] Φ IS UNSAT 20 Overview Introduction SMT Theories Case Study: Difference Logic Theory SMT Solvers and Libraries Summary 21 SMT-LIB SMT Library Provides standard rigorous descriptions of background theories Common input and output languages for SMT solvers Provides a library of benchmarks Ref: The SMT-LIB Standard 22 SMT Solvers Proprietary Open Source Z3, Yices, Barcelogic, MathSAT Open-SMT, CVC3, Boolector Some SMT-LIB Compatibility Solvers (Even partially) CVC3, Open-SMT, MathSAT5, Sonolar 23 SMT-LIB Example Check if (p AND p’) is satisfiable? UNINTERPRETED FUNCTIONS UNSATISFIABLE Ref: SMT-LIB Tutorial by David R. Cok and GrammaTech Inc. 24 SMT-LIB Example Is there a solution to x+2y = 20 and x-y = 2 LINEAR INTEGER ARITHMETIC SATISFIABLE x=8, y= 6 25 SUMMARY SMT problems include a wider range of problems than SAT. SMT-LIB initiative to bring standards to solvers. SMT Applications Include: Analog, Mixed-Signal Circuit Checker [Walter07] Software Testing RTL Verification Nelson-Oppen Method for Combining Theory Solvers 26 Trivia SMT Competition (SMT-COMP) SMT Solvers Competition Since 2005 2010 Winners: CVC3, OpenSMT, MathSAT 5, test_pmathsat, MiniSmt, simplifyingSTP. First International SAT/SMT Solver Summer School 2011 June 12- 17 at MIT. Free for students. 27 References [Barret09] Clark Barrett, Sanjit A. Seshia, ICCAD Tutorial 2009 [NO79] Greg Nelson and Derek C. Oppen. Simplification by cooperating decision procedures. ACM Trans. on Programming Languages and Systems, 1(2):245–257, October 1979 [Walter07] David Walter, Scott Little, Chris Meyers, “Bounded model checking of analog and mixedsignal circuits using an SMT solver”, Proceeding ATVA'07. 28 Questions Thank you. 29 Equivalence Checking of Programs int fun1(int y) { int x, z; z = y; y = x; x = z; return x*x; } int fun2(int y) { return y*y; } SMT formula Using SAT to check equivalence (w/ Satisfiable iff programs non-equivalent Minisat) 32 bits for y: Did not finish in over 5 hours ( zbits = yfor ∧ y1 = x ∧ x1 = z ∧ ret1 = x1*x1) 16 y: 37 sec. 8 bits for∧y: 0.5 sec. ( ret2Using = y*yEUF ) solver: 0.01 sec SMT: ∧ ( ret1 ret2 ) What if we use SAT to check equivalence? Slide adopted from [Barret09] 30

Descargar
# Satisfiability Modulo Theories (SMT)