IA085: Satisfiability and Automated Reasoning
Seminar 3
Exercise 1 Which of the following formulas are T-valid for the given the-
ory?
• ∃n. n · n = 2 for
– T = TNIA,
– T = TNRA,
– T = TLRA;
• x <u
[8]
x +[8] 1[8] for T = TBV;
• ∀n. ∃m. m ≥ n ∧ P(m) ∧ P(m + 2),
where T = TNIA and P(x) is defined by
P(x) ≡ x ≥ 2 ∧ ∀p. (p ≥ 1 ∧ ∃q. x = pq) → (p = 1 ∨ p = x);
Exercise 2 Which of the following T-entailments hold?
• x <u
[8]
128[8] |=BV x <u
[8]
x +[8] 1[8],
• a = b |=AX read(write(a, 0, 0), 1) = read(b, 1),
• x + 0 = x |=UF 0 + x = x,
• x + 0 = x |=UF x = x + 0,
For the following exercises, use the smt solver z3. For a quick
reference of the input language smt-lib, the following might be
helpful:
commands
• (declare-const name sort)
• (declare-fun name in_sorts out_sort)
• (assert φ)
• (check-sat)
• (get-model)
sorts
• Bool
• Int
• Real
• (_ BitVec 32)
logical operations
ia085: satisfiability and automated reasoning 2
• (not φ)
• (and φ ψ)
• (or φ ψ)
• (implies φ ψ)
• (iff φ ψ)
arithmetic operations
• (+ t1 t2)
• (- t1 t2)
• (* t1 t2)
• (div t1 t2)
• (/ t1 t2)
• (= t1 t2)
• (distinct t1 t2)
• (> t1 t2)
• (>= t1 t2)
if-then-else expression
• (ite φ t1 t2)
You might also need the corresponding operations for bit-vectors.
Look them up when you need them.
Exercise 3 Use z3 to prove the T-validity of the formulas from Exercise 1.
Further, prove that the entailments from Exercise 2 hold.
Exercise 4 You are the waiter in the xkcd comic strip https://xkcd.
com/287/. What can you bring to the guest? Are there more solutions than
one?
ia085: satisfiability and automated reasoning 3
Exercise 5 You are bored, browsing the Facebook, and found the following Or whatever social network is modern
these days.puzzle.
What theory is the puzzle using? What is the value of the triangle? Are
there multiple solutions?
Exercise 6 You are planning your weekend. You have 3 hours of free time
on Friday evening, 4 hours on Saturday, and 4 hours on Sunday. You have
to finish the following tasks and you want to work on them without interruptions
(i.e., once you start working on a task, you have to finish it).
• Finish a dpll solver for this course (takes 2 hours).
• Finish the two-watched literal scheme for the solver (takes 3 hours).
• Go to gym (takes 1 hour).
• Go jogging (takes 30 minutes).
• Rethink your life choices (takes 15 minutes).
• Cook a nice meal (takes 1 hour).
• Read a book (takes 3 hours).
You obviously cannot work on the two-watched literal scheme before finishing
the dpll solver. You also do not want to go to gym and go jogging on
the same day.
Is it feasible to finish all the tasks? Use z3 to come up with a feasible
schedule.
Hint: try using the if-then-else expression.
Exercise 7 You are trying to write a program for computing average of two
numbers and you came up with the following C program.
uint avg(uint x, uint y) {
return (x + y) / 2;
}
A friend of yours sees your code and tells you that it is not correct. Why?
Propose a fixed version.
You asked ChatGPT and it gave you the following weird solution
ia085: satisfiability and automated reasoning 4
uint avg(uint x, uint y) {
(x & y) + (x^y / 2);
}
Use z3 to prove that the solution is equivalent to your fixed version.