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)