Lukas' Notes

Search titles, aliases and note text. Use # for tags.

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

15 min read

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?

  • : impure
  • : impure
  • : pure

(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.

LabelCounterpartPolarityRaw
+
-
+
-
-
+
+,

The clausal normal form of the above is therefore:

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

First, select the unit clause , forcing , and propagate:

Unit propagation resulted in two new unit clauses, forcing :

Unit propagation yielded a new unit clause, forcing :

We have no more unit clauses left. Further, there are no pure literals, meaning we have to branch. Branch on :

Branching resulted in two new unit clauses, forcing :

Select the pure literal :

Select another pure literal :

The set of clauses is now empty. The algorithm terminates with an interpretation :

which satisfies the formula above. The interpretation for the original formula is

Plugging into the formula:

shows that 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:

  1. If I stay late at work today, then I finish my assignments.
  2. Either I stay late at work or I walk my dog, and I cannot do both.
  3. 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 , the conclusion follows. That is, you need either to formally prove or exhibit a counterexample for the statement.

Solution

Formalising:

Transforming:

forces . Assuming simplifies both and :

which are contradictory statements, meaning is UNSAT. Therefore, the entailment holds:

Problem 3. (20 points)

Problem 3. (20 points)

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

Solution

Let be a clause. Given our constraint, has one of two forms:

  1. ;
  2. .

In the first case, we can rewrite as the implication

If all are false, the clause reduces to and therefore forces .

Algorithm:

  1. Let be the set of atoms which have been forced to be false.
  2. For every negative unit clause , add to .
  3. Repeat until no longer changes:
    • If a clause satisfies , add to .
    • If a positive clause satisfies , return UNSAT.
  4. Define the interpretation by

Return SAT with the interpretation .

Correctness: Whenever the algorithm adds an atom to , every model of must assign . This follows by induction over the additions to .

  • Initially, is added only if . Every model of must therefore assign .
  • Suppose that the claim holds for all atoms already in . If the algorithm adds because

and , then every model assigns all by the induction hypothesis. The clause can then only be satisfied by , so every model must assign .

If the algorithm returns UNSAT, it has found a positive clause

with . Every model would have to assign all literals in this clause to false, contradicting that it satisfies the clause. Hence, is unsatisfiable.

Otherwise, consider the interpretation returned by the algorithm:

  • Every positive clause contains some ; otherwise, the algorithm would have returned UNSAT. Therefore, and the clause is satisfied.
  • Consider a clause . If , then and satisfies the clause. If , then some ; otherwise, the propagation rule would have added to . Thus, and the clause is again satisfied.

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

Polynomial-time decidability: Let be the set of atoms in and let be the total number of literal occurrences. One complete scan of takes time. Every scan either adds at least one new atom to or terminates, and each atom can be added to at most once. Therefore, there are at most scans, giving the running time

which is polynomial time.

Problem 4. (15 points)

Problem 4. (15 points)

Provide either a proof or a counterexample for the following statement:

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:

where are constants, is a unary function symbol, is an array constant, 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 the formula.

Solution

Let be the formula above, i.e.,

We have to branch. First, neglect and only take care of :

First, consider the branch in which holds.

Theory of linear integer arithmetic ():

Theory of equality with uninterpreted functions ():

The shared variables are .

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 ():

Theory of equality with uninterpreted functions ():

Both theory solvers report SAT with model , i.e., .