June 17th, 2026

Problem 1. (21 points)

Instruction

Let be the propositional formula:

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

Which atoms are pure in ? Justify your answer.

• impure:
• negatively pure:

The root has positive polarity. An implication reverses polarity in its antecedent and preserves it in its consequent; negation reverses polarity. Both operands of an equivalence have mixed polarity.

• has negative polarity. Thus has positive polarity and its occurrence of has negative polarity.
• has positive polarity. Its inner implication has negative polarity, so has positive polarity and the second occurrence of has negative polarity.
• Consequently, has negative polarity, but its operands and have mixed polarity. Hence and are impure, whereas both occurrences of are negative.

(2) CNF transformation with naming and polarity-based optimisation

Assign names in breadth-first order, reusing for both occurrences of . For a positive subformula , generate ; for a negative subformula , generate . Assert the root name .

Label	Subformula with named children	Polarity	Generated constraint
		positive
		negative
		positive
		positive
		negative at both occurrences
		negative
		positive
		negative

The mixed polarity of and inside the equivalence does not make mixed: the whole subformula occurs only negatively.

Converting the generated constraints to CNF gives:

Thus the clause set, including the root unit clause, is

The naming transformation gives : an assignment to satisfies exactly when it extends to an assignment satisfying all clauses of .

(3) DPLL with coloured cancellations

After selecting , unit propagation follows the chain

All clauses are removed, leaving the empty clause set , not an empty clause. Thus is satisfiable, with no backtracking needed. Restricting the assignment to the original atoms gives the model

Problem 2. (10 points)

Instruction

Consider a finite set of clauses such that no clause contains a positive literal. Is satisfiability of decidable without splitting? If yes, give an algorithm and argue for its correctness. If no, give a counterargument.

Solution

Yes. The following algorithm tests satisfiability for without splitting in polynomial running time:

def is_satisfiable(clauses: list[Clause]) -> bool:  # clauses = S
	for clause in clauses:
		if len(clause) == 0:
				return false  # UNSAT
	return true;  # SAT

The algorithm over clauses once. Therefore, it’s running time is

A clause is satisfiable if we find an interpretation that makes any literal or true, and is not the empty clause. The algorithm checks for the latter and if there’s an empty clause, return UNSAT immediately. The first case is simpler in this case: every only has negative literals, i.e., every literally only occurrs negatively in all ; hence, there are never conflicts, i.e., we can set every variable to false and call it a day, which is what the algorithmm does by immediately returning SAT.

Problem 3. (12 points)

Does the following entailment hold?

• If a robot completed a task, then, if robot reached the charging station, then robot delivered the package.
• Robot reached the charging station.
• Thus, either robot does not complete the task or robot delivered the package (or robot does not complete the task and robot delivered the package).

Give a proof or provide a countermodel.

Solution

We want to show that

By refutation, test whether there exists an interpretation such that

The unit forces . Simplify the first term to

Consider the negated conclusion, and notice that

which means the condition simplifies to

which is a contradiction, i.e., no such exists. Hence no countermodel exists, so the entailment holds.

Problem 4. (15 points)

Instruction

Consider the first-order theory

and the following formula :

Does the theory entail the formula ? Answer yes or no.
If yes, provide a first-order tableau proof.
If no, give and explain a countermodel that supports your answer.

• :

  • :
    • branched
  • :
    • branched

• :

  • :
    • :
      • branched
    • :
      • branched
  • :
    • :
      • branched
    • :
      • branched

• :

  • introduce
  • :
    • :
    • :
      • :

• B: :

  • L: :
    • closes
  • R: :
    • introduce
    • :
    • B: :
      • L: :
        • B: :
          • L: :
            • B: :
              • L: :
                • closes
              • R: :
                • B: :
                  • L: :
                    • :
                    • closes
                  • R: :
                    • :
                    • B: :
                      • L: :
                        • B:
                          • L: :
                            • open
                            • countermodel
                          • R: :
                            • …
                      • R: :
                        • …
          • R: :
            • …
      • R: :
        • …

Quite a mess. We obtain a countermodel with

Check whether is true under :

The premise is true under . Now evaluate the conclusio :

The conclusion is false under . Therefore, we found a countermodel for this. Yay.

Problem 5. (15 points)

Instruction

Let be a signature, where is a unary function symbol and is a constant. Let be the theory axiomatised by the axioms:

where are variables and thus the above axioms are implicitly universally quantified. The symbol denotes the standrad equality predicate, axiomatised accordingly by the axioms of the theory of equality .

Is stably infinite? If so, prove it. If not, disprove it.

Solution

To understand it first, write the axioms explicitly quantified:

The interesting part is . Both and are universally quantified. So, if we keep fixed, we can still choose any domain element for , and the equality must hold.

Suppose is a model of . We have the constant , so try fixing . The first axiom then says

Read it as every domain element must equal the same output. What about itself? It is also a domain element, so choosing gives . Using the axioms of equality, we obtain

Therefore, our domain can only consist of , i.e., . This is more restrictive than just saying that is constant: every possible value of must equal that constant output as well.

Does a one-element domain actually work for both axioms? Try

The first axiom holds because both and denote . The second holds because is true for the only possible value of . So the theory does have a model, but we cannot enlarge its domain: the first axiom would force every added element to equal again.

Now check the definition of stable infiniteness: every -satisfiable quantifier-free formula must also have an infinite -model. We can choose the simple formula . It is true in our one-element model, but no infinite -model exists.

Therefore, the theory is not stably infinite.

Problem 6. (27 points)

Instruction

Let be the formula

where

with being integer constants, being a unary function, being an integer array, and being interpreted in the standard way over the integers. Further, and are interpreted over the theory of arrays.

When considering the propositional structure of , assume that DPLL returns the following truth value assignments over the literals of :

• and .
• and .

For each , is satisfiable when considering the truth value assignment of to the literals of ? If it is, provide a theory model of . If not, describe the next step for checking the satisfiability of using DPLL(T).

When reasoning about theory literals to determine satisfiability of , use the Nelson-Oppen decision procedure to reason in the combination of theories. Use the decision procedures for the theory of uninterpreted functions and the one for arrays, and use simple mathematical reasoning for deriving new equalities among the constants in the theory of linear integer arithmetic. Provide sufficient details on your steps; importantly, state which theory decision procedure you use and detail the steps of each decision procedure. In particular, write down the congruence closures/classes and how you came up with them.

must hold under both assignments. First, separate these literals into their theories, introducing fresh constants for the arithmetic terms and function outputs.

Theory of linear integer arithmetic :

Theory of equality :

The equality is between constants shared with arithmetic, so it is also available to . The constant prepares the purification of below.

Theory of arrays :

In , the equalities and put the following terms in one congruence class:

In particular, we obtain .

There is also an equality we can obtain from arithmetic already, before considering either assignment. Since ,

Pass to . Congruence gives , merging their output classes. The congruence classes are now

Thus is available to under both and .

Consider

Here and , so add

In , use the definitions of the output constants:

The merged congruence class is now

Pass to . Both writes in address the same position, so the outer write of overwrites the inner write of :

Thus the array constraint simplifies to

The read-over-write rule has two cases:

But the shared state gives , and gives . Hence is already forced. No split is needed: only the first case applies.

Current state

Constraints collected under , with propagated to each theory.

Theory of linear integer arithmetic:

Theory of equality:

Theory of arrays:

Now arithmetic contains both and . Combining them gives

which is a contradiction over the integers. Therefore, is theory-inconsistent: no theory model of realises this assignment. This rules out , not yet itself.

Consider

Here and . Start from the shared state, not the state obtained under .

Current state

Theory of linear integer arithmetic:

Theory of equality:

and are constrained to have different values by ; their separation is not merely an absence of a known equality.

Theory of arrays:

The simplified read retains the inner write of . It does not constrain to equal .

Now the remaining write is at , and we read at . These positions are equal, so the read returns the value just written:

Thus reduces to and adds no further restriction. The original array still needs to satisfy because of .

Can we choose concrete values satisfying everything? Start with . Then requires , and . We need but . One choice is

Use the standard integers and integer arrays, with the usual arithmetic, read and write operations. Check the literals under this interpretation:

For , the first write puts at position . The second write puts at position , leaving position unchanged. Reading position therefore returns .

Hence realises : are true and is false. Therefore, is satisfiable.