1 of 31

Lecture 10 - SMT Solving

Real-Time Systems and Temporal Verification

COSC560

​

Stanley Bak

[Some Slides due to Sayan Mitra and Clark Barrett]

2 of 31

Goals and non-goals

Goal:

- Get intuitive understanding of the algorithms for SAT / SMT

- Be able to lookup and understand more detailed information

if desired / needed

​

Non-goal:

- Become a SAT / SMT Expert

3 of 31

What do these mean? Which one is SAT solving?

4 of 31

Recall: what’s a model (in first-order logic)?

5 of 31

Recall: what’s a model (in first-order logic)?

6 of 31

SAT solving

Assumption: Formulas are in Conjunctive Normal Form

​

DPLL Rules:

1. Decide (assign forced values)

  • Unit Propagation
  • Pure Literal

2. Propagate (guess)

3. Backtrack (guess the other way)

​

State-of-the-art: hundreds of thousands of variables

7 of 31

CDCL (Conflict Driven Clause Learning)

Learn new clauses (lemmas) to prevent repeated lines of reasoning finding the same contradictions

​

​

Relies on building an implication graph

​

​

Demo: https://en.wikipedia.org/wiki/Conflict-driven_clause_learning

​

​

7

8 of 31

Satisfiability modulo theories

 

9 of 31

Decision Prodedures for a Theory

A Decision Procedure is algorithm to determine if a formula (in theory T) is satisfiable. They usually work on conjunctions of literals.

10 of 31

Architecture of an SMT solver

​

Theory solvers/decision procedures

​

​

​

​

​

​

​

​

​

​

Arithmetic

​

Bitvectors

​

​

DPLL

​

Difference logic

​

…

​

Uninterpreted functions

​

Core

​

CNF formula in

real arithmetic

​

solution or

counterexample

boolean skeleton of problem

assertions

11 of 31

What is a theory in mathematical logic?

  • When we talk about well-formed formulas with non-binary variables, we have to say exactly what type of formulas are allowed
  • and, what it means for assignments to satisfy such formulas
  • This brings us to the notions theory and models in mathematical logic

12 of 31

Building up a theory

 

  •  

13 of 31

Terms to Formulas

 

 

14 of 31

Models for Theories

 

 

15 of 31

Decision procedures

16 of 31

Example theories

  •  

17 of 31

Example decision procedure: Uninterpreted functions (UF)

 

18 of 31

Example decision procedure: Uninterpreted functions (UF)

 

19 of 31

Example decision procedure 2: Difference logic

  •  

20 of 31

 

 

 

 

 

 

 

 

 

 

 

 

 

21 of 31

 

 

 

 

 

 

 

 

 

 

 

 

 

22 of 31

Return to SMT

​

Theory solvers/decision procedures

​

​

​

​

​

​

​

​

​

​

Arithmetic

​

Bitvectors

​

​

DPLL

​

Difference logic

​

…

​

Uninterpreted functions

​

Core

​

CNF formula in

real arithmetic

​

solution or

counterexample

boolean skeleton of problem

assertions

 

 

23 of 31

  •  

​

Theory solvers/decision procedures

​

​

​

​

​

​

​

​

​

​

Arithmetic

​

Bitvectors

​

​

DPLL

​

Difference logic

​

…

​

Uninterpreted functions

​

Core

​

CNF formula in

real arithmetic

​

solution or

counterexample

boolean skeleton of problem

assertions

24 of 31

Decidability Results

 

24

25 of 31

Decidability Results

25

26 of 31

Decidability Results

26

27 of 31

Decidability Results

  • Ok, if it there is no way to prove all the true statements in Integers, it’s not possible for rationals or reals.

​

27

28 of 31

Decidability Results

 

28

29 of 31

Decidability Results

 

29

30 of 31

30

31 of 31

If More Than Two Theories Are Involved?

Statement 𝝓 might contain elements from two different theories.

​

Solved using Nelson-Oppen procedure.

  1. Describes conditions on when can a formula with several theories is decidable.
  2. Provides decision procedures when possible.