# Homework 4

- Due 27 Sep 2018 by 10:15
- Points 2
- Submitting on paper

**Exercise 1**

Use the CDCL algorithm from the lecture slides to determine the (un)satisfiability of the following

boolean formula:

(x3 $\vee $ x4 $\vee $ ~x1 $\vee $ x5) $\wedge $ (~x3 $\vee $ x4 $\vee $ x5) $\wedge $ (x3 $\vee $ ~x4 $\vee $ ~x1) $\wedge $ (x1 $\vee $ x2) $\wedge $ (x1 $\vee $ ~x2) $\wedge $ (~x1 $\vee $ ~x5) $\wedge $ (~x3 $\vee $ ~x4 $\vee $ x5)

Note: Symbol ~ denotes the boolean negation operator.

**Exercise 2**

Use the congruence closure algorithm from the lecture slides to determine the (un)satisfiability

of the following SMT formulae:

- F
_{1}= {a = c, d = f(f(c)), f(c) = f(f(f(b))), f(b) = a, d ≠ f(c)} - F
_{2}= {a = b, c = f(d), f(b) = g(a), d = c, g(b) = d, g(c) ≠f(f(a))}

**Exercise 3 **

Use the Z3 SMT solver to encode and check (un)satisfiability of formulae in Exercise 1 and 2.

Print out your solution and bring it to the peer review session.

(cf. Z3 web interface and Z3 tutorial)

**NOTE:** Unfortunately, the Z3 website is currently down. If the Z3 web interface is still down by next Tuesday, this exercise becomes optional and you don't have to do it.