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:
- Which atom are pure in the above formula?
- Compute a clausal normal form
- Decide the satisfiable of the computed CNF formula
by applying the DPLL method to . If is satisfiable, give an interpretation which satisfies it.
makes both and impure , the rhs of the implication, remains positive is pure (negative)
(2) Compute a clausal normal form
Label Subformula Polarity Generated negative positive negative positive positive positive , Transforming into conjunctive normal forms:
Therefore:
(3) Decide the satisfiable of the computed CNF formula
by applying the DPLL method to . If is satisfiable, give an interpretation which satisfies it.
is a unit clause, which forces . Propagate unit: There are no unit clauses. Hence, select the pure literal
, which forces : There are no unit clauses nor any pure literal. We have to branch on
: Explore
. We found a new unit clause
, forcing : We found two new unit clauses, forcing
: The clause
is a unit clause, forcing : This produces the unit clause
, forcing : Finally, the unit clause
forces : The clause set is empty. Hence,
is satisfiable. A satisfying interpretation is: The naming transformation introduces fresh atoms
and satisfies Hence, an interpretation of
is translated back by projecting it onto the atoms of : discard the assignments to the naming atoms and retain the assignments to , , and . Here this gives Indeed,
Thus, there is no need to substitute the definitions of
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:
- Premise:
- Premise:
- Premise:
- Conclusion:
- By refutation:
We can simplify given we have two unit clauses
forcing
Both branches in the semantic tableau:
, contradicting the fourth propositon , contradicting the first proposition Therefore, the formula is unsat, i.e., the entailment holds:
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 is built from propositional atoms using only and . Let
be the set of clauses obtained from by applying the standard conjunctive normal form transformation (that is, without naming clauses). Let be an atom occurring in . Show that is pure in if and only if one of the literals or is pure in .
Solution
Let
be an atom occurring in , and define to be the set of polarities of in . The standard conjunctive normal form transformation first eliminates implications: which does not change the polarity of any occurrence.
Next, the transformation pushes negations inwards using De Morgan and double negation, i.e.,
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
over which only duplicates occurrences, never changes their polarities.
Therefore, none of the operations changes the polarity of any atom
, i.e., no transformation of in causes polarity changes in .
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 have to show that it is in fact a counterexample.
Solution
Problem 5. (25 points)
Problem 5. (25 points)
Consider the formula:
where
are integer constants, is an array constant, is a unary function, 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 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
be the formula Consider
first. Theory of linear integer arithmetic (
): Theory of equality with uninterpreted functions (
): Theory of arrays (
):
yields Propagate
to the other theories. Theory of linear integer arithmetic (
): Theory of equality with uninterpreted functions (
): Theory of arrays (
):
yields Propagate it to the other theories.
Theory of linear integer arithmetic (
): Theory of equality with uninterpreted functions (
): Theory of arrays (
):
reports UNSAT as it found the contradiction Therefore,
is UNSAT. Consider
. Theory of linear integer arithmetic (
): Theory of equality with uninterpreted functions (
):
yields Propagate it to the other theory.
Theory of linear integer arithmetic (
): Theory of equality with uninterpreted functions (
):
reports UNSAT given it found the contradiction Therefore,
is also UNSAT. We therefore conclude that
is UNSAT.