Questions: Literals and Clauses in Conjunctive Normal Form

Question 1

Which of the following formulas is in conjunctive normal form (CNF)?

• A. P ∧ (Q ∨ (R ∧ S)) — because it uses only ∧ and ∨ with literals
• B. (P ∨ ¬Q) ∧ (¬R ∨ S ∨ P) — because it is a conjunction of clauses, each a disjunction of literals
• C. (P ∧ Q) ∨ R — because it uses both connectives
• D. ¬(P ∨ Q) ∧ R — because it begins with a conjunction

Answer: (B)

CNF requires the formula to be a conjunction (AND) of clauses, where each clause is a disjunction (OR) of literals (atoms or their negations). Option B fits: it is a conjunction of two clauses, each being a disjunction of literals. Option A violates CNF because the second conjunct (Q ∨ (R ∧ S)) contains a conjunction *inside* a disjunction — clauses must be pure disjunctions of literals. Option C is (AND inside OR), which is DNF structure. Option D has ¬(P ∨ Q) — a negated disjunction, not a literal; De Morgan's would expand it to ¬P ∧ ¬Q, which is itself a conjunction, not a literal.

Question 2

Tseitin's transformation converts a propositional formula to CNF in linear time, but the result is only *equisatisfiable*, not logically *equivalent*, to the original. What does this distinction mean in practice?

• A. Tseitin CNF may give different truth values for some assignments — it is less accurate than full CNF conversion
• B. Tseitin CNF introduces fresh auxiliary variables; it is satisfiable if and only if the original is, but their satisfying assignments differ because the Tseitin version has extra variables
• C. Equisatisfiable formulas can be substituted for one another in any logical proof without consequence
• D. Tseitin CNF is only an approximation and should be avoided when correctness is critical

Answer: (B)

Logical equivalence means the same truth value under *all* variable assignments. Equisatisfiability is weaker: the two formulas agree only on whether a satisfying assignment *exists*. Tseitin's transformation introduces fresh auxiliary variables not present in the original; the expanded CNF has satisfying assignments involving those variables that have no direct counterpart in the original formula. For SAT solving — which only asks 'is the formula satisfiable?' — equisatisfiability is sufficient. But if you need to enumerate all models of the original formula, you must project out (discard) the auxiliary variables from the Tseitin output.

Question 3

The formula (A ∨ B) ∧ C is already in conjunctive normal form and requires no conversion.

• T. True
• F. False

Answer: True

A formula is in CNF if it is a conjunction of clauses, where each clause is a disjunction of literals. (A ∨ B) ∧ C fits exactly: the first clause is (A ∨ B) — a disjunction of two positive literals — and the second clause is (C) — a single positive literal (unit clause). No conversion is needed. Recognizing when a formula is already in CNF (or very nearly so) is a useful practical skill that avoids unnecessary transformation steps.

Question 4

Converting any propositional formula to CNF using distributive laws (distributing ∨ over ∧) generally produces a result of the same size or smaller than the original formula.

• T. True
• F. False

Answer: False

Distributing ∨ over ∧ can cause exponential blowup. Each application of A ∨ (B ∧ C) ≡ (A ∨ B) ∧ (A ∨ C) can double the number of clauses. A formula with n nested alternations of ∨ and ∧ can produce a CNF with 2ⁿ clauses. This is precisely why Tseitin's transformation is preferred in practice: it avoids the blowup by introducing auxiliary variables, producing a CNF of linear size at the cost of equisatisfiability rather than full equivalence.

Question 5

In resolution-based automated theorem proving, why must the input formula be converted to CNF before the resolution rule can be applied?

Model answer: Resolution operates on pairs of *clauses* that share a complementary literal pair (P and ¬P). A clause is a disjunction of literals — a unit that CNF directly provides. The resolution rule produces a new clause (the resolvent) by joining the remaining literals from both input clauses. Without CNF, the formula is in an arbitrary shape with no 'clauses' to resolve against each other; the rule has no defined inputs.

CNF transforms any formula into a uniform set of constraints (clauses), each independently required to be satisfied. Resolution works by deriving new constraints from existing ones: if (A ∨ P) and (B ∨ ¬P) are both required, then (A ∨ B) must also hold. Applying this repeatedly until either a contradiction (the empty clause) or a solution is found is the basis of DPLL and CDCL — the algorithms powering modern SAT solvers. CNF is the interface that makes this uniform application possible.