June 21st, 2024 (1st 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:
$(p \leftrightarrow \neg q) \to ((p \lor q) \land \neg (p \lor r))$

Which atom are pure in the above formula?

Compute a clausal normal form $C$

Decide the satisfiable 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 atom are pure in the above formula?

$(p \leftrightarrow \neg q)$ makes both $p$ and $q$ impure

$((p \lor q) \land \neg (p \lor r))$ , the rhs of the implication, remains positive

$r$ is pure (negative)

(2) Compute a clausal normal form $C$

$n_{6} n_{1} (p \leftrightarrow \neg q) \to n_{5} (n_{2} (p \lor q) \land \neg (n_{3} p \lor r) n_{4})$
Label Subformula Polarity Generated
$n_{1}$ $p \leftrightarrow \neg q$ negative $(p \leftrightarrow \neg q) \to n_{1}$
$n_{2}$ $p \lor q$ positive $n_{2} \to (p \lor q)$
$n_{3}$ $p \lor r$ negative $(p \lor r) \to n_{3}$
$n_{4}$ $\neg n_{3}$ positive $n_{4} \to \neg n_{3}$
$n_{5}$ $n_{2} \land n_{4}$ positive $n_{5} \to (n_{2} \land n_{4})$
$n_{6}$ $n_{1} \to n_{5}$ positive $n_{6}$ , $n_{6} \to (n_{1} \to n_{5})$

Transforming into conjunctive normal forms:
$(p \leftrightarrow \neg q) \to n_{1} n_{2} \to p \lor q (p \lor r) \to n_{3} n_{4} \to \neg n_{3} n_{5} \to n_{2} \land n_{4} n_{6} n_{6} \to (n_{1} \to n_{5}) \equiv [(p \to \neg q) \land (\neg q \to p)] \to n_{1} \equiv \neg [(\neg p \lor \neg q) \land (q \lor p)] \lor n_{1} \equiv \neg (\neg p \lor \neg q) \lor \neg (q \lor p) \lor n_{1} \equiv (p \land q) \lor (\neg q \land \neg p) \lor n_{1} \equiv ([(p \land q) \lor \neg q] \land [(p \land q) \lor \neg p]) \lor n_{1} \equiv (p \lor \neg q) \land ⊤ (q \lor \neg q) \land ⊤ (p \lor \neg p) \land (q \lor \neg p) \lor n_{1} \equiv [(p \lor \neg q) \land (q \lor \neg p)] \lor n_{1} \equiv (p \lor \neg q \lor n_{1}) \land (q \lor \neg p \lor n_{1}) \equiv \neg n_{2} \lor p \lor q \equiv \neg (p \lor r) \lor n_{3} \equiv (\neg p \land \neg r) \lor n_{3} \equiv (\neg p \lor n_{3}) \land (\neg r \lor n_{3}) \equiv \neg n_{4} \lor \neg n_{3} \equiv \neg n_{5} \lor (n_{2} \land n_{4}) \equiv (\neg n_{5} \lor n_{2}) \land (\neg n_{5} \lor n_{4}) \equiv n_{6} \equiv \neg n_{6} \lor \neg n_{1} \lor n_{5}$
Therefore:
$C = {} (p \lor \neg q \lor n_{1}), (q \lor \neg p \lor n_{1}), (\neg n_{2} \lor p \lor q), (\neg p \lor n_{3}), (\neg r \lor n_{3}), (\neg n_{4} \lor \neg n_{3}), (\neg n_{5} \lor n_{2}), (\neg n_{5} \lor n_{4}), (n_{6}) (\neg n_{6} \lor \neg n_{1} \lor n_{5})$

Label	Subformula	Polarity	Generated
$n_{1}$	$p \leftrightarrow \neg q$	negative	$(p \leftrightarrow \neg q) \to n_{1}$
$n_{2}$	$p \lor q$	positive	$n_{2} \to (p \lor q)$
$n_{3}$	$p \lor r$	negative	$(p \lor r) \to n_{3}$
$n_{4}$	$\neg n_{3}$	positive	$n_{4} \to \neg n_{3}$
$n_{5}$	$n_{2} \land n_{4}$	positive	$n_{5} \to (n_{2} \land n_{4})$
$n_{6}$	$n_{1} \to n_{5}$	positive	$n_{6}$ , $n_{6} \to (n_{1} \to n_{5})$

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

$(n_{6})$ is a unit clause, which forces $n_{6} \equiv ⊤$ . Propagate unit:
$C_{n_{6} \equiv ⊤} = {} (p \lor \neg q \lor n_{1}), (q \lor \neg p \lor n_{1}), (\neg n_{2} \lor p \lor q), (\neg p \lor n_{3}), (\neg r \lor n_{3}), (\neg n_{4} \lor \neg n_{3}), (\neg n_{5} \lor n_{2}), (\neg n_{5} \lor n_{4}), (n_{6}) (\neg n_{6} \lor \neg n_{1} \lor n_{5})$
There are no unit clauses. Hence, select the pure literal $\neg r$ , which forces $r \equiv ⊥$ :
$C_{n_{6} \equiv ⊤, r \equiv ⊥} = {} (p \lor \neg q \lor n_{1}), (q \lor \neg p \lor n_{1}), (\neg n_{2} \lor p \lor q), (\neg p \lor n_{3}), (\neg r \lor n_{3}), (\neg n_{4} \lor \neg n_{3}), (\neg n_{5} \lor n_{2}), (\neg n_{5} \lor n_{4}), (\neg n_{1} \lor n_{5})$
There are no unit clauses nor any pure literal. We have to branch on $n_{1}$ :

Explore $n_{1} \equiv ⊤$ .
$C_{n_{6} \equiv ⊤, r \equiv ⊥, n_{1} \equiv ⊤} = {} (p \lor \neg q \lor n_{1}), (q \lor \neg p \lor n_{1}), (\neg n_{2} \lor p \lor q), (\neg p \lor n_{3}), (\neg n_{4} \lor \neg n_{3}), (\neg n_{5} \lor n_{2}), (\neg n_{5} \lor n_{4}), (\neg n_{1} \lor n_{5})$
We found a new unit clause $(n_{5})$ , forcing $n_{5} \equiv ⊤$ :
$C_{n_{6} \equiv ⊤, r \equiv ⊥, n_{1} \equiv ⊤, n_{5} \equiv ⊤} = {} (\neg n_{2} \lor p \lor q), (\neg p \lor n_{3}), (\neg n_{4} \lor \neg n_{3}), (\neg n_{5} \lor n_{2}), (\neg n_{5} \lor n_{4}), (n_{5})$
We found two new unit clauses, forcing $n_{2} \equiv n_{4} \equiv ⊤$ :
$C_{n_{6} \equiv ⊤, r \equiv ⊥, n_{1} \equiv ⊤, n_{5} \equiv ⊤, n_{2} \equiv ⊤, n_{4} \equiv ⊤} = {(\neg n_{2} \lor p \lor q), (\neg p \lor n_{3}), (\neg n_{4} \lor \neg n_{3}), (n_{2}), (n_{4})}$
The clause $(\neg n_{3})$ is a unit clause, forcing $n_{3} \equiv ⊥$ :
$C_{n_{6} \equiv ⊤, r \equiv ⊥, n_{1} \equiv ⊤, n_{5} \equiv ⊤, n_{2} \equiv ⊤, n_{4} \equiv ⊤, n_{3} \equiv ⊥} = {(p \lor q), (\neg p \lor n_{3}), (\neg n_{3})}$
This produces the unit clause $(\neg p)$ , forcing $p \equiv ⊥$ :
$C_{n_{6} \equiv ⊤, r \equiv ⊥, n_{1} \equiv ⊤, n_{5} \equiv ⊤, n_{2} \equiv ⊤, n_{4} \equiv ⊤, n_{3} \equiv ⊥, p \equiv ⊥} = {(p \lor q), (\neg p)}$
Finally, the unit clause $(q)$ forces $q \equiv ⊤$ :
$C_{n_{6} \equiv ⊤, r \equiv ⊥, n_{1} \equiv ⊤, n_{5} \equiv ⊤, n_{2} \equiv ⊤, n_{4} \equiv ⊤, n_{3} \equiv ⊥, p \equiv ⊥, q \equiv ⊤} = {= {} (q)}$
The clause set is empty. Hence, $C$ is satisfiable. A satisfying interpretation is:
$I = {} n_{1} \to 1, n_{2} \to 1, n_{3} \to 0, n_{4} \to 1, n_{5} \to 1, n_{6} \to 1, q \to 1, p \to 0, r \to 0$
The naming transformation introduces fresh atoms $n_{1}, \dots, n_{6}$ and satisfies
$F \equiv \exists n_{1} \dots \exists n_{6} C .$
Hence, an interpretation of $C$ is translated back by projecting it onto the atoms of $F$ : discard the assignments to the naming atoms and retain the assignments to $p$ , $q$ , and $r$ . Here this gives
$I ↾_{{p, q, r}} = {p \to 0, q \to 1, r \to 0} .$
Indeed,
$(⊥ \leftrightarrow \neg⊤) \to ((⊥ \lor ⊤) \land \neg (⊥ \lor ⊥)) \equiv ⊤ \to (⊤ \land ⊤) \equiv ⊤.$
Thus, there is no need to substitute the definitions of $n_{1}, \dots, n_{6}$ back into the formula. They are auxiliary witnesses and can be discarded once a satisfying assignment has been found.

Problem 2. (15 points)

Problem 2. (15 points)

Suppose we know that:

If Paolo is thin, then Carlo is not blonde or Roberta is not tall.

If Roberta is tall, then Sandra is lovely.

If Sandra is lovely and Carlo is blonde, then Paolo is thin.

Carlo is blonde.

Can we conclude that Roberta is not tall? Formalise this problem in logic and argue whether the entailment holds.

Solution

Formalise using propositional logic:

Premise: $t hi n_{p a o l o} \to (\neg b l o n d e_{c a r l o} \lor \neg t a l l_{ro b er t a})$

Premise: $t a l l_{ro b er t a} \to l o v e l y_{s an d r a}$

Premise: $(l o v e l y_{s an d r a} \land b l o n d e_{c a r l o}) \to t hi n_{p a o l o}$

Premise: $b l o n d e_{c a r l o}$

Conclusion: $\neg t a l l_{ro b er t a}$

By refutation: $t a l l_{ro b er t a}$

We can simplify given we have two unit clauses
$b l o n d e_{c a r l o} t a l l_{ro b er t a}$
forcing
$t hi n_{p a o l o} \to ⊥ ⊤ \to l o v e l y_{s an d r a} (⊤ \land b l o n d e_{c a r l o}) \to t hi n_{p a o l o} b l o n d e_{c a r l o} t a l l_{ro b er t a} \equiv \neg t hi n_{p a o l o} \equiv l o v e l y_{s an d r a} \equiv b l o n d e_{c a r l o} \to t hi n_{p a o l o} \equiv b l o n d e_{c a r l o} \equiv t a l l_{ro b er t a}$
Both branches in the semantic tableau:

$f : b l o n d e_{c a r l o}$ , contradicting the fourth propositon

$t : t hi n_{p a o l o}$ , contradicting the first proposition

Therefore, the formula is unsat, i.e., the entailment holds:
$Γ ⊨ \neg t a l l_{ro b er t a}$

Problem 3. (20 points)

Problem 3. (20 points)

Let $A$ be a propositional, well-formed formula using $n \geq 1$ propositional variables such that

$A$ is not a propositional atom

$A$ is built from propositional atoms using only $\neg, \lor,$ and $\to$ .

Let $S$ be the set of clauses obtained from $A$ by applying the standard conjunctive normal form transformation (that is, without naming clauses). Let $p$ be an atom occurring in $A$ . Show that $p$ is pure in $A$ if and only if one of the literals $p$ or $\neg p$ is pure in $S$ .

Solution

Let $p$ be an atom occurring in $A$ , and define $pol_{p} (A) \subseteq {+ 1, - 1}$ to be the set of polarities of $p$ in $A$ . The standard conjunctive normal form transformation first eliminates implications:
$A \to B ⇝ \neg A \lor B,$
which does not change the polarity of any occurrence.

Next, the transformation pushes negations inwards using De Morgan and double negation, i.e.,
$\neg (A \land B) ⇝ \neg A \lor \neg B \neg (A \lor B) ⇝ \neg A \land \neg B \neg\neg A ⇝ A,$
However, none of those rules change the polarity of a single atom, given that the negations do not disappear in the first two cases, while the latter rule shortens the double-flip path to the atom.

Finally, the transformation distributes $\lor$ over $\land$
$(A \land B) \lor C A \lor (B \land C) ⇝ (A \lor C) \land (B \lor C) ⇝ (A \lor B) \land (A \lor C)$
which only duplicates occurrences, never changes their polarities.

Therefore, none of the operations changes the polarity of any atom $p$ , i.e., no transformation of $p$ in $A$ causes polarity changes in $S$ .

Problem 4. (15 points)

Problem 4. (15 points)

Provide either a proof or a counterexample for the following statement:
$\exists (A (x) \to \forall y A (y)) ⊨ \exists x A (x)$
If you provide a counterexample, you have to show that it is in fact a counterexample.

Solution

Semantic Tableau:

$f : \exists x A (x)$

$f : A (a)$

$t : \exists x (A (x) \to \forall y A (y))$

$t : A (a) \to \forall y A (y)$

L Branch:

$f : A (a)$

open

R Branch:

$t : \forall y A (y)$

$t : A (a)$ :

closed

Counterexample:
$D^{I} = {a} A^{I} = {}$

Problem 5. (25 points)

Problem 5. (25 points)

Consider the formula:
$a = b + 5 \land f (b + 2) = c \land (re a d (w r i t e (A, a + 1, 4), b + 6) = 2 \lor f (a - 3) \neq = c)$
where $a, b, c$ are integer constants, $A$ is an array constant, $f$ is a unary function, $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 theories. Use the decision procedures for the theory of arrays and the theory of uninterpreted functions, and use simple mathematical reasoning for deriving 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
$F \equiv φ_{1} a = b + 5 \land φ_{2} f (b + 2) = c \land (φ_{3} re a d (w r i t e (A, a + 1, 4), b + 6) = 2 \lor φ_{4} f (a - 3) \neq = c) \equiv φ_{1} \land φ_{2} \land (φ_{3} \lor φ_{4}) \equiv F^{(1)} (φ_{1} \land φ_{2} \land φ_{3}) \lor F^{(2)} (φ_{1} \land φ_{2} \land φ_{4}) \equiv F^{(1)} \lor F^{(2)}$
Consider $F^{(1)}$ first.

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

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

Theory of linear integer arithmetic ( $T_{Z}$ ):
$a ℓ_{1} ℓ_{2} ℓ_{3} ℓ_{4} ℓ_{5} ℓ_{2} ℓ_{5} = b + 5 = b + 2 = a + 1 = 4 = b + 6 = 2 = ℓ_{4} = ℓ_{3}$
Theory of equality with uninterpreted functions ( $T_{UE}$ ):
$f (ℓ_{1}) ℓ_{2} ℓ_{5} = c = ℓ_{4} = ℓ_{3}$
Theory of arrays ( $T_{A}$ ):
$re a d (w r i t e (A, ℓ_{2}, ℓ_{3}), ℓ_{4}) ℓ_{2} ℓ_{5} = ℓ_{5} = ℓ_{4} = ℓ_{3}$
$T_{Z}$ reports UNSAT as it found the contradiction
$ℓ_{3} = 4 = 2 = ℓ_{3} .$
Therefore, $F^{(1)}$ is UNSAT.

Consider $F^{(2)}$ .

Theory of linear integer arithmetic ( $T_{Z}$ ):
$a ℓ_{1} ℓ_{2} = b + 5 = b + 2 = a - 3$
Theory of equality with uninterpreted functions ( $T_{UE}$ ):
$f (ℓ_{1}) f (ℓ_{2}) = c \neq = c$
$T_{Z}$ yields
$ℓ_{1} = ℓ_{2} .$
Propagate it to the other theory.

Theory of linear integer arithmetic ( $T_{Z}$ ):
$a ℓ_{1} ℓ_{2} ℓ_{1} = b + 5 = b + 2 = a - 3 = ℓ_{3}$
Theory of equality with uninterpreted functions ( $T_{UE}$ ):
$f (ℓ_{1}) f (ℓ_{2}) ℓ_{1} = c \neq = c = ℓ_{2}$
$T_{UE}$ reports UNSAT given it found the contradiction
$ℓ_{1} = ℓ_{2} \to f (ℓ_{1}) = f (ℓ_{2}) \to f (ℓ_{2}) = c, f (ℓ_{2}) \neq = c$
Therefore, $F^{(2)}$ is also UNSAT.

We therefore conclude that $F$ is UNSAT.

Lukas' Notes

June 21st, 2024 (1st 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. (25 points)