IA085: Satisfiability and Automated Reasoning
Seminar 5
Exercise 1 If you didn’t write the bounded model checking exercise using
incremental smt calls, rewrite it as such. Finish the k-induction exercise
from the last seminar.
Exercise 2 You know the problem of Satisfiability Modulo Theories (smt),
where the task is to compute any model of the given formula. There is a
related problem of Optimization Modulo Theories (omt), where the task is
to compute for a given formula φ and a term t a model that minimizes the
value of t.
For example, given a formula
φ = (x = 0 ∧ y ≥ 10) ∨ (x = 2 ∧ y ≥ 5)
over LIA and a term t = x + y, the solution of optimization modulo theories
problem would be a model µ(x = 2), µ(y = 5).
Design an algorithm that solves the omt problem using potentially
multiple queries to an smt solver and implement it in pySMT.
Exercise 3 Use the congruence closure algorithm to determine which of the
following conjunctions of UF-literals are satisfiable. Also identify some of the
implied equalities and disequalities.
1. x = y ∧ f (x) ̸= f (y),
2. f (x) ̸= x ∧ f2(x) = x ∧ f4(x) = x,
3. f (x) ̸= x ∧ f3(x) = x ∧ f5(x) = x.
Exercise 4 Use the algorithm from the lecture to determine which of the following
conjunctions of literals in difference logic over integers are satisfiable.
Also identify some of the implied inequalities.
1. x − y = 5 ∧ z − y ≤ 3 ∧ x − z < 4,
2. a − b ≤ 3 ∧ c − b ≤ 10 ∧ d − a ≤ 1 ∧ a − d ≤ 5 ∧ c − a ≤ 1 ∧ d − c ≥
3 ∧ d − b ≥ 2.