Skip to content

DPLL(T)

SAT solver with decision procedure (DP) for first-order theory.

First-order theory is a restriction of the syntax of first-order logic

Lazy and Basic

Assume that \(DP_T\) returns a formula \(t\) through a procedure DEDUCTION with the following properties:

  • \(t\) is T-valid
  • \(t\) contains only atoms that already appear in the original formula
  • The encoding of \(t\) contradicts the original assignment

Further Improvement on DPLL(T)

At each iteration, the formula is "stronger" (because we are adding more clauses)

We can reuse what we have learned in previous steps.

We can benefit from an incremental SAT solver

Examples of Theories

Uninterpreted functions with equality (EUF): No relation symbols, no quantifiers.

E.g. if \(t_1=t_1'\land\cdots\land t_k=t_k')\), then \(f(t_1,\cdots,t_k)=f(t_1',\cdots,t_k')\)

Applications: Proving equivalence of programs/circuits.

Linear Arithmetic

Syntax

formula \(\varphi:\varphi\land\varphi\vert(\varphi)\vert\)atom

atom: sum \(op\) sum

op: \(=\vert<\vert\leq\)

sum: term | sum+term

term: identifier| constant | constant identifier

E.g. \(2x_1+1\leq x_2+4\), \((3x_1+4\leq x_3)\land(x_3<x_2)\)

Solvers and Applications

Decision procedures: Simplex/Linear Programming. Integer Programming/Branch and Bound...

Applications: verification of certain properties of software.

Another variant: difference logic

formula: formula \(\land\) formula | atom

atom: identifier \(-\) identifier \(op\) constant

op: \(<|\leq\) (Equality can be obtained by rewriting the expression)

Bit Vectors

Decision procedure for bit vectors can be reduced to SAT.

formula: formula \(\land\) formula | \(\neg\)formula | (formula) atom

atom: term rel term | Bool - identifier | term[constant]

rel: \(<|=\)

term: term op term | identifier | ~term | constant | atom?term:term | term[constant:constant] | ext(term)

op: \(+|-|\cdot|/|\ll|\gg|\And|||\oplus|\circ\)

Logic for Pointers

formula: formula \(\land\) formula | \(\neg\)formula | (formula) | atom

atom: pointer=pointer | term=term | pointer¡pointer | term¡term

pointer: pointer-identified | pointer+term | (pointer) | &identifier | &*pointer | *pointer | NULL

term: identifier | *pointer | term op term | (term) | integer-constant | identifier[term]

op: \(+|-\)

Well-formed expressions:

  • \(*(p+1)=1\)
  • \(*(p+*p)=0\)
  • \(p=q\land(*p=5)\)
  • \(p<q\)

Notice that the model for this theory requires a model for the memory

  • \(M:A\to D\) mapping addresses to data
  • \(L:V\to A\) mapping variables to addresses

Combining Theories

In some cases, when we reason about bit vectors and pointers, we need two theories \(T_1\) and \(T_2\).

If we have decision procedures for both, the problem may not be decidable even if \(T_1\) and \(T_2\) are decidable.

Under certain circumstances, we can build a decision procedure for the combination. (Nelson-Oppen Combination Procedure)

SMT-LIB

A library for SMT.

S-expressions

aka symbolic expression, Polish notation

\(3+4\to+3\ 4\)

\(3+4*5\to+3*(4\ 5)\)

\((3+4)*5\to*(+3\ 4)\ 5\)

A \(list[1,2,3]\) is \((list\ 1\ 2\ 3)\)