June 26th, 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:

1. Which atoms are pure in the above formula?
2. Compute a clausal normal form of the above formula by applying the CNF transformation algorithm with naming and optimisation based on polarities of subformulas.
3. Decide the satisfiability of the computed CNF formula by applying the DPLL method to . If is satisfiable, give an interpretation which satisfies it.

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

• (positive)
  • (positive)
    • (positive)
      • (negative)
    • (positive)
  • (positive)
    • (negative)
      • (negative)
        • (mixed)
        • (mixed)
      • (negative)
        • (positive)
        • (negative)
• : negatively pure
• : impure
• impure

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

Label	Subformula	Polarity	Generated
		positive
		positive
		negative
		negative
		negative
		positive
		positive

Convert to CNF clauses:

The clausal normal form is

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

Select the unit clause , forcing :

Two new unit clauses appeared, forcing :

More unit clauses! Force , .

Well… more unit clauses! They force . and , i.e., a contradiction.

Therefore, the aforementioned formula is UNSAT.

Problem 2. (20 points)

Problem 2. (20 points)

Formalise the following arguments and verify whether they are correct:

1. I must be punished only if I am guilty; I am guilty. Thus, I must be punished.
2. If I am guilty, I must be punished; I am not guilty. Thus, I must not be punished.

Verifying whether an argument is correct means proving a statement of the following form: from the hypotheses , the conclusion follows. That is, either formally prove , or exhibit a counterexample to the statement.

Solution

Formalise:

Consider the first statement. By duality

&\text{iff} \
{punished \to guilty, guilty, \lnot punished} &\text{ is unsat}.

\end{align}

{\lnot punished}.

I = {guilty \mapsto 1, punished \mapsto 0}.

\begin{aligned}
guilty \to punished, \lnot guilty &\models \lnot punished \
\text{iff} \
{guilty \to punished, \lnot guilty, punished} &\text{ is unsat}.
\end{aligned}

{ punished }.

I = { guilty \mapsto 0, punished \mapsto 1 }.

Problem 3. (20 points)

Problem 3. (20 points)

Let be a propositional, well-formed formula using propositional variables such that

• is not a propositional atom; and
• is built from propositional atoms using only and .

How many branches does a splitting tree of have? Provide a sufficiently detailed explanation of your answer.

Solution

Let denote the number of branches in a splitting tree for .

For , splitting on the single propositional variable produces one child for each of its two possible truth values. Since no variables remain, both children simplify to constants. Hence,

Now suppose that contains propositional variables. Splitting on any variable produces the two children

Neither nor can terminate a branch while another variable remains. In particular,

For , the repeated binary splitting has the following shape:

Thus, each child still requires splitting on the remaining variables. Both subtrees therefore have branches, giving

Together with , this yields

Therefore, the splitting tree has branches, one for each possible interpretation of its propositional variables.

Problem 4. (10 points)

Problem 4. (10 points)

Provide either a tableau proof or a counterexample for the statement

If you provide a counterexample, you have to show that it is in fact a counterexample.

Solution

• (premise)

• (conclusion)

• • (L) Branch
    • • contradicts
      • (L) branch closes
  • (R) Branch
    • • contradicts
      • (R) branch closes

All branches of the tableau close, i.e., there’s no countermodel for the above statement.

Problem 5. (25 points)

Problem 5. (25 points)

Consider the formula:

where are integer constants, is a unary function symbol, is an array constant, and are interpreted in the array theory, and 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 it.

Let be the formula

Consider first.

Theory of linear integer arithmetic ():

Theory of equality with uninterpreted functions ():

emits

Propagate .

Theory of linear integer arithmetic ():

Theory of equality with uninterpreted functions ():

infers

But according to the theory’s fragments. Contradiction. Hence, is UNSAT.

Consider .

Theory of linear integer arithmetic ():

Theory of equality with uninterpreted functions ():

Theory of arrays ():

infers

Given that and , i.e., (under the standard interpretation over integers), the left branch cannot be true. Propagate the latter branch.

Theory of linear integer arithmetic ():

Theory of equality with uninterpreted functions ():

Theory of arrays ():

with sort for and .