Create a gist now

Instantly share code, notes, and snippets.

What would you like to do?
SMT Solvers and Constraint Programming

On Logic Solvers

From SAT to SMT and back.

There is a Gist, see references [@gist].

Satisfiability (SAT)

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]

DIMACS

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: $(A \lor C) \land (\lnot B)$

c this is a dimacs file
p cnf 3 2
1 3 0
-2 0

Assignment

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)$

Satisfiability Modulo Theories (SMT)

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

SMT-LIB 2.0

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)

Optimizing SMT

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)

Assignment

  • 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}$

Parallel Cooking

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.

Constraint-based layouting

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 and nuZ Paper

  • Z3 [@z3]
  • $\nu$Z [@nuzmax], [@nuzopt]

References

c !A and (B or C)
p cnf 3 2
-1 0
2 3 0
c (A or B) and (!B or C or !D) and (D or !E)
p cnf 5 3
1 2 0
-2 3 -4 0
4 -5 0
(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)
(declare-const x Int)
(declare-const y Int)
(assert (<= 0 x 10))
(assert (<= 0 y 10))
(maximize (+ x y))
(check-sat)
(get-model)
(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)
(declare-const x0 Int)
(declare-const x1 Int)
(declare-const x2 Int)
(declare-const x3 Int)
(assert (< 1 x0 10))
(assert (< 1 x1 10))
(assert (< 1 x2 10))
(assert (< 1 x3 10))
(assert (< 15 (+ x0 x1)) 20)
(assert (implies (> x2 5) (> x1 5)))
(minimize (+ x0 x1 x2 x3))
(check-sat)
(get-model)
;; Abstractions for Point2d(Int, Int) and Box2d(Int, Int, Int, Int)
;; on which we build a constraint-based layouting engine.
;;
;; grep "define" thisfile; for a quick overview what's there.
;; Point(x, y)
(declare-datatypes (X Y) ((PointT (makePoint (x X) (y Y)))))
(define-sort Point () (PointT Int Int))
;; Box(p0, p1, p2, p3)
;;
;; p3--p2
;; | |
;; p0--p1
;;
(declare-datatypes (P0 P1 P2 P3) ((BoxT (makeBox (p0 P0) (p1 P1) (p2 P2) (p3 P3)))))
(define-sort Box () (BoxT Point Point Point Point))
;; Axis aligned constructor from (p0, p2)
(define-fun makeBoxFromAnchorPoints ((p0 Point) (p2 Point)) (Box)
(makeBox p0 (makePoint (x p2) (y p0)) p2 (makePoint (x p0) (y p2))))
;; Precondition: (and (boxAxixAligned? box) (boxExpandsTopRight? box))
(define-fun boxWidth ((box Box)) (Int)
(- (x (p1 box)) (x (p0 box))))
;; Precondition: (and (boxAxixAligned? box) (boxExpandsTopRight? box))
(define-fun boxHeight ((box Box)) (Int)
(- (y (p3 box)) (y (p0 box))))
;; +
;; ^
;; | Origin (0, 0) at bottom left, expands (i.e. not empty box)
;; ---> +
;;
(define-fun boxExpandsTopRight? ((box Box)) (Bool)
(and
(> (x (p1 box)) (x (p0 box)))
(> (x (p2 box)) (x (p3 box)))
(> (y (p3 box)) (y (p0 box)))
(> (y (p2 box)) (y (p1 box)))))
;; Axis alignment for x-axis, y-axis
(define-fun boxAxisAligned? ((box Box)) (Bool)
(and
(= (x (p0 box)) (x (p3 box)))
(= (x (p1 box)) (x (p2 box)))
(= (y (p0 box)) (y (p1 box)))
(= (y (p3 box)) (y (p2 box)))))
;; Precondition: (and (boxAxisAligned? b0) (boxAxisAligned? b1)
;; (boxExpandsTopRight? b0) (boxExpandsTopRight? b1))
(define-fun boxOverlapsBox? ((b0 Box) (b1 Box)) (Bool)
(not (or
(> (x (p0 b1)) (x (p1 b0)))
(< (x (p1 b1)) (x (p0 b0)))
(< (y (p3 b1)) (y (p0 b0)))
(> (y (p0 b1)) (y (p3 b0))))))
;; Checks if b1 is inside b0
;;
;; Precondition: (and (boxAxisAligned? b0) (boxAxisAligned? b1)
;; (boxExpandsTopRight? b0) (boxExpandsTopRight? b1))
(define-fun boxInsideBox? ((b0 Box) (b1 Box)) (Bool)
(and
(> (x (p0 b1)) (x (p0 b0)))
(> (y (p0 b1)) (y (p0 b0)))
(< (x (p2 b1)) (x (p2 b0)))
(< (y (p2 b1)) (y (p2 b0)))))
;; Checks where b1 is located relative to b0
;;
;; Precondition: (and (boxAxisAligned? b0) (boxAxisAligned? b1)
;; (boxExpandsTopRight? b0) (boxExpandsTopRight? b1))
(define-fun boxLeftOfBox? ((b0 Box) (b1 Box)) (Bool)
(< (x (p1 b1)) (x (p0 b0))))
(define-fun boxRightOfBox? ((b0 Box) (b1 Box)) (Bool)
(> (x (p0 b1)) (x (p1 b0))))
(define-fun boxAboveBox? ((b0 Box) (b1 Box)) (Bool)
(> (y (p0 b1)) (y (p3 b0))))
(define-fun boxBelowBox? ((b0 Box) (b1 Box)) (Bool)
(< (y (p3 b1)) (y (p0 b0))))
;; Environment
(define-fun laptopView () (Box)
(makeBoxFromAnchorPoints (makePoint 0 0) (makePoint 1366 768)))
(define-fun phoneView () (Box)
(makeBoxFromAnchorPoints (makePoint 0 0) (makePoint 768 1280)))
(declare-const box0 (Box))
(declare-const box1 (Box))
;; Constraining the layout
(assert (and
(boxAxisAligned? box0)
(boxAxisAligned? box1)
(boxExpandsTopRight? box0)
(boxExpandsTopRight? box1)
(< 100 (boxWidth box0) 400)
(< 200 (boxHeight box0) 800)
(< 200 (boxWidth box1) 800)
(< 100 (boxHeight box1) 400)
(boxAboveBox? box0 box1)
(boxRightOfBox? box0 box1)
(boxInsideBox? laptopView box0)
(boxInsideBox? laptopView box1)
;(boxInsideBox? phoneView box0)
;(boxInsideBox? phoneView box1)
(not (boxOverlapsBox? box0 box1))
true))
(maximize (+
(boxWidth box0) (boxHeight box0)
(boxWidth box1) (boxHeight box1)))
(check-sat)
(get-model)
;; vim: set filetype=clojure:
;; Interval(begin, end)
(declare-datatypes (BeginT EndT) ((IntervalT (makeInterval (begin BeginT) (end EndT)))))
(define-sort Interval () (IntervalT Int Int))
(define-fun intervalExpandsIntoFuture? ((interval Interval)) (Bool)
(< (begin interval) (end interval)))
(define-fun intervalDuration ((interval Interval)) (Int)
(- (end interval) (begin interval)))
(define-fun intervalRequiresIntervalOver ((lhs Interval) (rhs Interval)) (Bool)
(> (begin lhs) (end rhs)))
(define-fun intervalDuringInterval? ((lhs Interval) (rhs Interval)) (Bool)
(and
(> (begin lhs) (begin rhs))
(< (end lhs) (end rhs))))
(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)
(assert (and
(= 0 (begin schedule))
(intervalExpandsIntoFuture? schedule)
(intervalExpandsIntoFuture? makeDough)
(intervalExpandsIntoFuture? sliceOnions)
(intervalExpandsIntoFuture? sliceTomatos)
(intervalExpandsIntoFuture? bakeInOven)
(intervalExpandsIntoFuture? servePizza)
(intervalExpandsIntoFuture? pourWine)
(intervalDuringInterval? makeDough schedule)
(intervalDuringInterval? sliceOnions schedule)
(intervalDuringInterval? sliceTomatos schedule)
(intervalDuringInterval? bakeInOven schedule)
(intervalDuringInterval? servePizza schedule)
(intervalDuringInterval? pourWine schedule)
(< 3 (intervalDuration makeDough))
(< 2 (intervalDuration sliceOnions))
(< 2 (intervalDuration sliceTomatos))
(= 35 (intervalDuration bakeInOven))
(< 2 (intervalDuration servePizza))
(< 2 (intervalDuration pourWine))
(intervalRequiresIntervalOver bakeInOven makeDough)
(intervalRequiresIntervalOver bakeInOven sliceOnions)
(intervalRequiresIntervalOver bakeInOven sliceTomatos)
(intervalRequiresIntervalOver servePizza bakeInOven)
true))
(minimize (intervalDuration schedule))
(check-sat)
(get-model)
;; vim: set filetype=clojure:
<!DOCTYPE html>
<html lang="en">
<head>
<meta charset="utf-8">
<title>box</title>
<style>
#view {
position:fixed;
left: 0px;
bottom: 0px;
width: 1366px;
height: 768px;
background-color: #dcdcdc;
}
#box0 {
position:fixed;
left: 1px;
bottom: 12px;
width: 399px;
height: 355px;
background-color: #ffcccc;
}
#box1 {
position:fixed;
left: 401px;
bottom: 368px;
width: 799px;
height: 399px;
background-color: #ccccff;
}
</style>
</head>
<body>
<div id="view">view</div>
<div id="box0">box0</div>
<div id="box1">box1</div>
</body>
</html>
@article{nuzopt,
title={$\nu$Z-An Optimizing SMT Solver},
author={Bj{\o}rner, Nikolaj and Phan, Anh-Dung and Fleckenstein, Lars}
}
@article{nuzmax,
title={$\nu$Z-Maximal Satisfaction with Z3},
author={Bj{\o}rner, Nikolaj and Phan, Anh-Dung}
}
@incollection{z3,
title={Z3: An efficient SMT solver},
author={De Moura, Leonardo and Bj{\o}rner, Nikolaj},
booktitle={Tools and Algorithms for the Construction and Analysis of Systems},
pages={337--340},
year={2008},
publisher={Springer}
}
@misc{proptocnf,
title={From propositional logic to CNF},
url={http://en.wikipedia.org/wiki/Conjunctive_normal_form#Conversion_into_CNF}
}
@misc{cnfsat,
title={Davis–Putnam–Logemann–Loveland},
url={http://en.wikipedia.org/wiki/DPLL_algorithm}
}
@misc{smtlib,
title={SMT-LIB 2.0 Standard},
url={http://smtlib.cs.uiowa.edu/language.shtml}
}
@misc{gist,
title={Workshop Material},
url={https://gist.github.com/daniel-j-h/09c772b706db7a7240a4}
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment