From SAT to SMT and back.
There is a Gist, see references [@gist].
Is a given formula (i.e. $\lnot A \land (B \lor C)$) satisfiable?
Is there an assignment such that the formula evaluates to true?
- From propositional logic to CNF [@proptocnf]
- DPLL algorithm for CNF-SAT [@cnfsat]
Standardized format for CNF formulae.
- Lines starting with "c" are comments
- Formula has to be in conjunctive normal form (CNF)
- CNF: conjunction of clauses, with a clause being disjunctions of literals
Syntax:
c Comment
p cnf numVariables numClauses
...
- Literal numering starts at 1
- Positive literals (1 represents
$A$ ), negative literals (-1 represents$\lnot A$ ) - Terminate line with 0
Example:
c this is a dimacs file
p cnf 3 2
1 3 0
-2 0
Are the following two formulae satisfiable? If so, give a model!
$\lnot A \land (B \lor C)$ $(A \lor B) \land (\lnot B \lor C \lor \lnot D) \land (D \lor \lnot E)$
Generalization of SAT. Knows about so called theories (theory of integers, reals, arrays, bitvectors, ...) and their rules (e.g. associativity of plus, ...).
- Int: mathmatical integers, not machine types
- Real: mathmatical real, not floats
- BitVec: vector of bits, signed and unsigned two's-complement calculations
- Array: select and store axioms, represent state
Standard and tutorial PDFs [@smtlib].
Example:
(set-option :produce-models true)
(set-logic QF_LIA)
(declare-fun x () Int)
(declare-fun y () Int)
(assert (= x 10))
(assert (< 0 y 10))
(check-sat)
(get-value (x))
(get-value (y))
(exit)
For this you need nuZ, included in the Z3 \textbf{opt} branch.
nuZ introduced maximize, minimize for theory of Int, Real, BitVec:
(declare-const x Int)
(declare-const y Int)
(assert (<= 0 x 10))
(assert (<= 0 y 10))
(maximize (+ x y))
(check-sat)
(get-model)
Soft assertions, and combining objectives:
(set-option :opt.priority box)
;(set-option :opt.priority pareto)
;(set-option :opt.priority lex)
(declare-const x Int)
(declare-const y Int)
(assert (<= 0 x 10))
(assert (<= 0 y 10))
(assert-soft (not (= x y)))
(maximize (+ x y))
(minimize (+ x y))
(check-sat)
(get-model)
- You have four nodes, with power consumption
$x_{0}, ... x_{3}$ - They need power in Watts, i.e.
$1 < x_{i} < 10 $ -
$x_{0}$ and$x_{1}$ draw from same source, should respect:$15 < x_{0} + x_{1} < 20$ -
$x_{2}$ depends on$x_{1}$ , i.e. if you give$x_{2}$ more than 5 Watts you have to give$x_{1}$ also more than 5 Watts - minimize the total power consumption
$\sum_{i} x_{i}$
Useful interval type:
(declare-datatypes (BeginT EndT) ((IntervalT (makeInterval (begin BeginT) (end EndT)))))
(define-sort Interval () (IntervalT Int Int))Implement:
(define-fun intervalExpandsIntoFuture? ((interval Interval)) (Bool))
(define-fun intervalDuration ((interval Interval)) (Int))
(define-fun intervalRequiresIntervalOver ((lhs Interval) (rhs Interval)) (Bool))
(define-fun intervalDuringInterval? ((lhs Interval) (rhs Interval)) (Bool))Now write the constraints for the following Pizza recipe:
(declare-const schedule Interval)
(declare-const makeDough Interval)
(declare-const sliceOnions Interval)
(declare-const sliceTomatos Interval)
(declare-const bakeInOven Interval)
(declare-const servePizza Interval)
(declare-const pourWine Interval)
And minimize the overall time it takes.
Point and Box types:
(declare-datatypes (X Y) ((PointT (makePoint (x X) (y Y)))))
(define-sort Point () (PointT Int Int))
(declare-datatypes (P0 P1 P2 P3) ((BoxT (makeBox (p0 P0) (p1 P1) (p2 P2) (p3 P3)))))
(define-sort Box () (BoxT Point Point Point Point))Implement:
(define-fun boxAxisAligned? ((box Box)) (Bool))
(define-fun boxExpandsTopRight? ((box Box)) (Bool))
(define-fun makeBoxFromAnchorPoints ((p0 Point) (p2 Point)) (Box))
(define-fun boxWidth ((box Box)) (Int))
(define-fun boxHeight ((box Box)) (Int))
(define-fun boxOverlapsBox? ((b0 Box) (b1 Box)) (Bool))
(define-fun boxInsideBox? ((b0 Box) (b1 Box)) (Bool))
(define-fun boxLeftOfBox? ((b0 Box) (b1 Box)) (Bool))
(define-fun boxRightOfBox? ((b0 Box) (b1 Box)) (Bool))
(define-fun boxAboveBox? ((b0 Box) (b1 Box)) (Bool))
(define-fun boxBelowBox? ((b0 Box) (b1 Box)) (Bool))
Now write the constraints for the following environment:
(define-fun laptopView () (Box))
(declare-const box0 (Box))
(declare-const box1 (Box))
With box1 to the top right of box0. Maximize the heigth, width of the boxes.
- Z3 [@z3]
- $\nu$Z [@nuzmax], [@nuzopt]