October 11, 2024 (2nd Exam for SS 2024)

This exam sheet consists of five problems, yielding a total of 100 points. Good luck!

Problem 1. (25 points)

Problem 1. (25 points)

Consider the formula:
$(\neg (p \land q) \to r) \land \neg ((r \leftrightarrow p) \land r)$

Which atoms are pure in the above formula?

Compute a clausal normal form $C$ of the above formula by applying the CNF transformation algorithm with naming and optimisation based on polarities of subformulas.

Decide the satisfiability of the computed CNF formula $C$ by applying the DPLL method to $C$ . If $C$ is satisfiable, give an interpretation which satisfies it.

(1) Which atoms are pure in the above formula?

$r$ : impure

$p$ : impure

$q$ : pure

(2) Compute a clausal normal form $C$ of the above formula by applying the CNF transformation algorithm with naming and optimisation based on polarities of subformulas.

Label Counterpart Polarity Raw
$n_{1}$ $p \land q$ + $n_{1} \to (p \land q)$
$n_{2}$ $\neg n_{1}$ - $\neg n_{1} \to n_{2}$
$n_{3}$ $n_{2} \to r$ + $n_{3} \to (n_{2} \to r)$
$n_{4}$ $r \leftrightarrow p$ - $(r \leftrightarrow p) \to n_{4}$
$n_{5}$ $n_{4} \land r$ - $(n_{4} \land r) \to n_{5}$
$n_{6}$ $\neg n_{5}$ + $n_{6} \to \neg n_{5}$
$n_{7}$ $n_{3} \land n_{6}$ + $n_{7}$ , $n_{7} \to (n_{3} \land n_{6})$

$n_{1} \to (p \land q) \neg n_{1} \to n_{2} n_{3} \to (n_{2} \to r) (r \leftrightarrow p) \to n_{4} (n_{4} \land r) \to n_{5} n_{6} \to \neg n_{5} n_{7} n_{7} \to (n_{3} \land n_{6}) \equiv \neg n_{1} \lor (p \land q) \equiv (\neg n_{1} \lor p) \land (\neg n_{1} \lor q) \equiv n_{1} \lor n_{2} \equiv \neg n_{3} \lor \neg n_{2} \lor r \equiv \neg [\neg (r \land \neg p) \land \neg (\neg r \land p)] \lor n_{4} \equiv [(r \land \neg p) \lor (\neg r \land p)] \lor n_{4} \equiv ([(r \land \neg p) \lor \neg r] \land [(r \land \neg p) \lor p]) \lor n_{4} \equiv [(r \lor \neg r) \land (\neg p \lor \neg r) \land (r \lor p) \land (\neg p \lor p)] \lor n_{4} \equiv (\neg p \lor \neg r \lor n_{4}) \land (r \lor p \lor n_{4}) \equiv \neg (n_{4} \land r) \lor n_{5} \equiv \neg n_{4} \lor \neg r \lor n_{5} \equiv \neg n_{6} \lor \neg n_{5} \equiv n_{7} \equiv \neg n_{7} \lor (n_{3} \land n_{6}) \equiv (\neg n_{7} \lor n_{3}) \land (\neg n_{7} \lor n_{6})$
The clausal normal form of the above is therefore:
$C = {(\neg n_{1} \lor p), (\neg n_{1} \lor q), (n_{1} \lor n_{2}), (\neg n_{3} \lor \neg n_{2} \lor r), (\neg p \lor \neg r \lor n_{4}), (r \lor p \lor n_{4}), (\neg n_{4} \lor \neg r \lor n_{5}), (\neg n_{6} \lor \neg n_{5}), (n_{7}), (\neg n_{7} \lor n_{3}), (\neg n_{7} \lor n_{6})}$

Label	Counterpart	Polarity	Raw
$n_{1}$	$p \land q$	+	$n_{1} \to (p \land q)$
$n_{2}$	$\neg n_{1}$	-	$\neg n_{1} \to n_{2}$
$n_{3}$	$n_{2} \to r$	+	$n_{3} \to (n_{2} \to r)$
$n_{4}$	$r \leftrightarrow p$	-	$(r \leftrightarrow p) \to n_{4}$
$n_{5}$	$n_{4} \land r$	-	$(n_{4} \land r) \to n_{5}$
$n_{6}$	$\neg n_{5}$	+	$n_{6} \to \neg n_{5}$
$n_{7}$	$n_{3} \land n_{6}$	+	$n_{7}$ , $n_{7} \to (n_{3} \land n_{6})$

(3) Decide the satisfiability of the computed CNF formula $C$ by applying the DPLL method to $C$ . If $C$ is satisfiable, give an interpretation which satisfies it.

First, select the unit clause $n_{7}$ , forcing $n_{7} \equiv ⊤$ , and propagate:
$C_{n_{7} \equiv ⊤} = {(\neg n_{1} \lor p), (\neg n_{1} \lor q), (n_{1} \lor n_{2}), (\neg n_{3} \lor \neg n_{2} \lor r), (\neg p \lor \neg r \lor n_{4}), (r \lor p \lor n_{4}), (\neg n_{4} \lor \neg r \lor n_{5}), (\neg n_{6} \lor \neg n_{5}), (n_{7}), (\neg n_{7} \lor n_{3}), (\neg n_{7} \lor n_{6})}$
Unit propagation resulted in two new unit clauses, forcing $n_{3} \equiv n_{6} \equiv ⊤$ :
$C_{n_{7} \equiv ⊤, n_{3} \equiv ⊤, n_{6} \equiv ⊤} = {(\neg n_{1} \lor p), (\neg n_{1} \lor q), (n_{1} \lor n_{2}), (\neg n_{3} \lor \neg n_{2} \lor r), (\neg p \lor \neg r \lor n_{4}), (r \lor p \lor n_{4}), (\neg n_{4} \lor \neg r \lor n_{5}), (\neg n_{6} \lor \neg n_{5}), (n_{3}), (n_{6})}$
Unit propagation yielded a new unit clause, forcing $n_{5} \equiv ⊥$ :
$C_{n_{7} \equiv ⊤, n_{3} \equiv ⊤, n_{6} \equiv ⊤, n_{5} \equiv ⊥} = {(\neg n_{1} \lor p), (\neg n_{1} \lor q), (n_{1} \lor n_{2}), (\neg n_{2} \lor r), (\neg p \lor \neg r \lor n_{4}), (r \lor p \lor n_{4}), (\neg n_{4} \lor \neg r \lor n_{5}), (\neg n_{5})}$
We have no more unit clauses left. Further, there are no pure literals, meaning we have to branch. Branch on $n_{1} \equiv ⊤$ :
$C_{n_{7} \equiv ⊤, n_{3} \equiv ⊤, n_{6} \equiv ⊤, n_{5} \equiv ⊥, n_{1} \equiv ⊤} = {(\neg n_{1} \lor p), (\neg n_{1} \lor q), (n_{1} \lor n_{2}), (\neg n_{2} \lor r), (\neg p \lor \neg r \lor n_{4}), (r \lor p \lor n_{4}), (\neg n_{4} \lor \neg r)}$
Branching resulted in two new unit clauses, forcing $p \equiv q \equiv ⊤$ :
$C_{n_{7} \equiv ⊤, n_{3} \equiv ⊤, n_{6} \equiv ⊤, n_{5} \equiv ⊥, n_{1} \equiv ⊤, p \equiv ⊤, q \equiv ⊤} = {(p), (q), (\neg n_{2} \lor r), (\neg p \lor \neg r \lor n_{4}), (r \lor p \lor n_{4}), (\neg n_{4} \lor \neg r)}$
Select the pure literal $n_{2} \equiv ⊥$ :
$C_{n_{7} \equiv ⊤, n_{3} \equiv ⊤, n_{6} \equiv ⊤, n_{5} \equiv ⊥, n_{1} \equiv ⊤, p \equiv ⊤, q \equiv ⊤, n_{2} \equiv ⊥} = {(\neg n_{2} \lor r), (\neg r \lor n_{4}), (\neg n_{4} \lor \neg r)}$
Select another pure literal $r = ⊥$ :
$C_{n_{7} \equiv ⊤, n_{3} \equiv ⊤, n_{6} \equiv ⊤, n_{5} \equiv ⊥, n_{1} \equiv ⊤, p \equiv ⊤, q \equiv ⊤, n_{2} \equiv ⊥, r = ⊥} = {(\neg r \lor n_{4}), (\neg n_{4} \lor \neg r)}$
The set of clauses $C = {}$ is now empty. The algorithm terminates with an interpretation $I$ :
$I = {n_{1} \to 1, n_{2} \to 0, n_{3} \to 1, n_{4} \to 0 (arbitrary), n_{5} \to 0, n_{6} \to 1, n_{7} \to 1, p \to 1, q \to 1, r \to 0}$
which satisfies the formula above. The interpretation $I^{'}$ for the original formula is
$I^{'} = I ↾_{p, q, r} = {p \to 1, q \to 1, r \to 0}$
Plugging $I^{'}$ into the formula:
$(\neg (1 \land 1) \to 0) \land \neg ((0 \leftrightarrow 1) \land 0) = (0 \to 0) \land \neg (0 \land 0) = 1 \land 1 = 1$
shows that $I^{'}$ is indeed a model of the formula.

Problem 2. (15 points)

Problem 2. (15 points)

Formalise the following argument and verify whether it is correct:

If I stay late at work today, then I finish my assignments.

Either I stay late at work or I walk my dog, and I cannot do both.

Therefore, I either walk my dog or finish my assignments.

Note that verifying whether an argument is correct means proving a statement of the form: from the hypotheses $P_{1}, \dots, P_{n}$ , the conclusion $Q$ follows. That is, you need either to formally prove $P_{1}, \dots, P_{n} ⊨ Q$ or exhibit a counterexample for the statement.

Solution

Formalising:
$P_{1} P_{2} Q := l a t e \to f ini s h := \neg (l a t e \leftrightarrow w a l k) := w a l k \lor f ini s h$
Transforming:
$P_{1} P_{2} \equiv \neg (\neg (l a t e \land \neg w a l k) \land \neg (\neg l a t e \land w a l k)) \neg Q \equiv \neg l a t e \lor f ini s h \equiv (l a t e \land \neg w a l k) \lor (\neg l a t e \land w a l k) \equiv \neg w a l k \land \neg f ini s h$
$\neg Q$ forces $w a l k \equiv f ini s h \equiv ⊥$ . Assuming $Q$ simplifies both $P_{1}$ and $P_{2}$ :
$P_{1} P_{2} \equiv \neg l a t e \equiv l a t e$
which are contradictory statements, meaning ${P_{1}, P_{2}, \neg Q}$ is UNSAT. Therefore, the entailment holds:

P_{1}, P_{2} ⊨ Q

Problem 3. (20 points)

Problem 3. (20 points)

Let $C$ be a set of clauses such that each clause in $C$ contains at most one negative literal. Give an algorithm that decides the satisfiability of $C$ in polynomial time. Justify the correctness of your algorithm and explain the polynomial-time decidability of your solution.

Solution

Let $c \in C$ be a clause. Given our constraint, $c$ has one of two forms:

$c \equiv p_{1} \lor p_{2} \lor \dots \lor p_{k} \lor \neg q$ ;

$c \equiv p_{1} \lor p_{2} \lor \dots \lor p_{k}$ .

In the first case, we can rewrite $c$ as the implication
$q \to (p_{1} \lor p_{2} \lor \dots \lor p_{k}) .$
If all $p_{i}$ are false, the clause reduces to $\neg q$ and therefore forces $q \equiv ⊥$ .

Algorithm:

Let $F := \emptyset$ be the set of atoms which have been forced to be false.

For every negative unit clause $(\neg q)$ , add $q$ to $F$ .

Repeat until $F$ no longer changes:

If a clause $p_{1} \lor \dots \lor p_{k} \lor \neg q$ satisfies $p_{1}, \dots, p_{k} \in F$ , add $q$ to $F$ .

If a positive clause $p_{1} \lor \dots \lor p_{k}$ satisfies $p_{1}^{'}, \dots, p_{k}^{'} \in F$ , return UNSAT.

Define the interpretation $I$ by

$I (p) = {01 if p \in F, if p \in / F .$
Return SAT with the interpretation $I$ .

Correctness: Whenever the algorithm adds an atom $q$ to $F$ , every model of $C$ must assign $q \equiv ⊥$ . This follows by induction over the additions to $F$ .

Initially, $q$ is added only if $(\neg q) \in C$ . Every model of $C$ must therefore assign $q \equiv ⊥$ .

Suppose that the claim holds for all atoms already in $F$ . If the algorithm adds $q$ because

$p_{1} \lor \dots \lor p_{k} \lor \neg q \in C$
and $p_{1}, \dots, p_{k} \in F$ , then every model assigns all $p_{i} \equiv ⊥$ by the induction hypothesis. The clause can then only be satisfied by $\neg q$ , so every model must assign $q \equiv ⊥$ .

If the algorithm returns UNSAT, it has found a positive clause
$p_{1} \lor \dots \lor p_{k}$
with $p_{1}, \dots, p_{k} \in F$ . Every model would have to assign all literals in this clause to false, contradicting that it satisfies the clause. Hence, $C$ is unsatisfiable.

Otherwise, consider the interpretation $I$ returned by the algorithm:

Every positive clause contains some $p_{i} \in / F$ ; otherwise, the algorithm would have returned UNSAT. Therefore, $I (p_{i}) = 1$ and the clause is satisfied.

Consider a clause $p_{1} \lor \dots \lor p_{k} \lor \neg q$ . If $q \in F$ , then $I (q) = 0$ and $\neg q$ satisfies the clause. If $q \in / F$ , then some $p_{i} \in / F$ ; otherwise, the propagation rule would have added $q$ to $F$ . Thus, $I (p_{i}) = 1$ and the clause is again satisfied.

Hence, $I$ satisfies every clause in $C$ , so $I$ is a model of $C$ . The algorithm therefore returns SAT if and only if $C$ is satisfiable.

Polynomial-time decidability: Let $V$ be the set of atoms in $C$ and let $L$ be the total number of literal occurrences. One complete scan of $C$ takes $O (L)$ time. Every scan either adds at least one new atom to $F$ or terminates, and each atom can be added to $F$ at most once. Therefore, there are at most $∣ V ∣ + 1$ scans, giving the running time
$O (∣ V ∣ \cdot L),$
which is polynomial time.

Problem 4. (15 points)

Problem 4. (15 points)

Provide either a proof or a counterexample for the following statement:
$\forall y \forall z (P (y) \land P (z)) ⊨ \forall x (P (x) \land Q (x))$
If you provide a counterexample, you must show that it is in fact a counterexample.

Problem 5. (20 points)

Problem 5. (20 points)

Consider the formula:
$a + 2 = b - 1 \land f (b + 1) = c - 2 \land (f (a + 3) \neq = c \lor re a d (w r i t e (A, a + 1, 3), b - 2) = 2)$
where $b, c$ are constants, $f$ is a unary function symbol, $A$ is an array constant, $re a d, w r i t e$ are interpreted in the array theory, and $+, -, 1, 2, 3, \dots$ are interpreted in the standard way over the integers.

Use the Nelson–Oppen decision procedure for reasoning in the combination of the theories of arrays, uninterpreted functions, and linear integer arithmetic. Use the decision procedures for the theory of arrays and the theory of uninterpreted functions, and use simple mathematical reasoning to derive new equalities among the constants in the theory of linear integer arithmetic. If the formula is satisfiable, give an interpretation that satisfies the formula.

Solution

Let $F$ be the formula above, i.e.,
$F \equiv φ_{1} a + 2 = b - 1 \land φ_{2} f (b + 1) = c - 2 \land (φ_{3} f (a + 3) \neq = c \lor φ_{4} re a d (w r i t e (A, a + 1, 3), b - 2) = 2) \equiv φ_{1} \land φ_{2} \land (φ_{3} \lor φ_{4})$
We have to branch. First, neglect $φ_{4}$ and only take care of $φ_{3}$ :
$F^{(1)} \equiv φ_{1} \land φ_{2} \land φ_{3}$
First, consider the branch in which $φ_{3}$ holds.

Theory of linear integer arithmetic ( $T_{Z}$ ):
$a + 2 ℓ_{1} ℓ_{2} ℓ_{3} = b - 1 = b + 1 = c - 2 = a + 3$
Theory of equality with uninterpreted functions ( $T_{UE}$ ):
$f (ℓ_{1}) f (ℓ_{3}) = ℓ_{2} \neq = c$
The shared variables are $ℓ_{1}, ℓ_{2}, ℓ_{3}, c$ .

There is no derivable equality between two shared constants that can be propagated. Test whether both branches are SAT individually:

Theory of linear integer arithmetic ( $T_{Z}$ ):
$a^{I} b^{I} c^{I} ℓ_{1}^{I} ℓ_{2}^{I} ℓ_{3}^{I} = 3 = 0 = 2 = 1 = 0 = 6$
Theory of equality with uninterpreted functions ( $T_{UE}$ ):
$f^{I} = {1 \mapsto 0, 6 \mapsto 69}$
Both theory solvers report SAT with model $I$ , i.e., $I ⊨_{T_{Z} \cup T_{UE} \cup T_{A}} F$ .

Consider the other branch.

$F^{(2)} \equiv φ_{1} \land φ_{2} \land φ_{4}$
Theory of linear integer arithmetic ( $T_{Z}$ ):
$a + 2 ℓ_{1} ℓ_{2} ℓ_{4} ℓ_{5} ℓ_{6} ℓ_{7} = b - 1 = b + 1 = c - 2 = a + 1 = 3 = b - 2 = 2$
Theory of equality with uninterpreted functions ( $T_{UE}$ ):
$f (ℓ_{1}) = ℓ_{2}$
Theory of arrays ( $T_{A}$ ):
$re a d (w r i t e (A, ℓ_{4}, ℓ_{5}), ℓ_{6}) = ℓ_{7}$
The shared variables are $ℓ_{1}, ℓ_{2}, ℓ_{4}, ℓ_{5}, ℓ_{6}, ℓ_{7}$ .

$T_{Z}$ yields
$a + 2 = b - 1 \to a - 1 = b - 2 \to ℓ_{4} = ℓ_{6}$
Propagate it to the other theories.

Theory of linear integer arithmetic ( $T_{Z}$ ):
$a + 2 ℓ_{1} ℓ_{2} ℓ_{4} ℓ_{5} ℓ_{6} ℓ_{7} ℓ_{4} = b - 1 = b + 1 = c - 2 = a + 1 = 3 = b - 2 = 2 = ℓ_{6}$
Theory of equality with uninterpreted functions ( $T_{UE}$ ):
$f (ℓ_{1}) ℓ_{4} = ℓ_{2} = ℓ_{6}$
Theory of arrays ( $T_{A}$ ):
$re a d (w r i t e (A, ℓ_{4}, ℓ_{5}), ℓ_{6}) ℓ_{4} = ℓ_{7} = ℓ_{6}$
Then, $T_{A}$ yields
$ℓ_{7} = ℓ_{5} .$
Propagate it to the other theories.

Theory of linear integer arithmetic ( $T_{Z}$ ):
$a + 2 ℓ_{1} ℓ_{2} ℓ_{4} ℓ_{5} ℓ_{6} ℓ_{7} ℓ_{4} ℓ_{7} = b - 1 = b + 1 = c - 2 = a + 1 = 3 = b - 2 = 2 = ℓ_{6} = ℓ_{5}$
Theory of equality with uninterpreted functions ( $T_{UE}$ ):
$f (ℓ_{1}) ℓ_{4} ℓ_{7} = ℓ_{2} = ℓ_{6} = ℓ_{5}$
Theory of arrays ( $T_{A}$ ):
$re a d (w r i t e (A, ℓ_{4}, ℓ_{5}), ℓ_{6}) ℓ_{4} ℓ_{7} = ℓ_{7} = ℓ_{6} = ℓ_{5}$
RESULT: $T_{Z}$ reports UNSAT due to the contradiction under the standard interpretation over integers
$ℓ_{7} = 2 = 3 = ℓ_{5} .$
Therefore, $F^{(2)}$ is UNSAT.

Lukas' Notes

October 11, 2024 (2nd Exam for SS 2024)

Table of Contents

Problem 1. (25 points)

Problem 2. (15 points)

Problem 3. (20 points)

Problem 4. (15 points)

Problem 5. (20 points)