Quiz. Converting to DNF [000l]

November 22, 2025

Convert the following formula into Disjunctive Normal Form (DNF):

\[ (q \lor \neg \neg p) \land (\neg r \to s) \]

Solution.

November 22, 2025

Context

VU-VFS-2025. Lecture 2 - Normal Forms & DPLL [000b]

November 22, 2025

Formula Equivalence

November 22, 2025

Definition. Equivalence of Formulae [000c]

November 22, 2025

Two formulas \(F\) and \(G\) are said to be equivalent, written \(F \equiv G\), if they have the same truth value under every interpretation. In other words, for every interpretation \(I\), \(I \models F\) if and only if \(I \models G\).

\[ F \equiv G \iff \forall I (I \models F \iff I \models G) \]

Quiz. Normal Forms & DPLL - Equivalence [000d]

November 22, 2025

Which of the following equivalences hold?

\(\bot \equiv \bot \)
\(\top \equiv \top \)
\(\neg \top \equiv \neg \bot \)
\(\neg (p \land q) \equiv \neg p \lor \neg q\)
\(p \equiv p \lor q\)
\(\neg \neg p \equiv p\)

Solution.

November 22, 2025

True. Both sides are always false.
True. Both sides are always true.
False. Left side is always false, right side is always true.
True. This is De Morgan's law. Good to remember \[ \neg (p \land q) \equiv \neg p \lor \neg q \]
False. Left side is true when p is true, right side is true when either p or q is true.
True. Double negation elimination.

Negation Normal Forms

November 22, 2025

Definition. Negation Normal Form (NNF) [000e]

November 22, 2025

A formula \(F\) is in Negation Normal Form (NNF) if the negation operator \(\neg \) is only applied to literals (i.e., propositional variables or their negations), and the only other allowed operators are conjunction \(\land \) and disjunction \(\lor \). A nice way to think about it is that we can never have the case where we need to apply De Morgan's laws to push negations further down the formula tree. So all negations come pre-distributed to the literals.

Quiz. Negation Normal Form (NNF) [000f]

November 22, 2025

Which of the following formulas are in Negation Normal Form (NNF)?

\(p \to q\)
\(p \lor (\neg q \land (r \lor \neg s))\)
\(p \lor (\neg q \land \neg (\neg r \land s))\)
\(p \lor (\neg q \land (\neg \neg r \lor \neg s)) \)

Solution.

November 22, 2025

No. The implication operator \(\to \) is not allowed in NNF.
Yes. Negations are only applied to literals, and only \(\land \) and \(\lor \) are used.
No. The negation operator \(\neg \) is applied to a non-literal formula \((\neg r \land s)\).
No. The double negation \(\neg \neg r\) is not allowed in NNF. Important to remember since that can trip you up.

Disjunctive Normal Form

November 22, 2025

Definition. Distributing Conjunction [000k]

November 22, 2025

The distributive law of conjunction over disjunction states that for any formulas \(F\), \(G\), and \(H\), the following equivalence holds:

\[ \begin {align*} F \land (G \lor H) &\equiv (F \land G) \lor (F \land H) \\ (F \lor G) \land H &\equiv (F \land H) \lor (G \land H) \end {align*} \]

Definition. Eliminating Implications and Biconditionals [000j]

November 22, 2025

To eliminate implications (\(\to \)) and biconditionals (\(\leftrightarrow \)) from a formula \(F\), we can use the following equivalences:

\[ \begin {align*} p \to q &\equiv \neg p \lor q \\ p \leftrightarrow q &\equiv (p \land q) \lor (\neg p \land \neg q) \end {align*} \]

Definition. Disjunctive Normal Form (DNF) [000h]

November 22, 2025

A formula \(F\) is in Disjunctive Normal Form (DNF) if it is a disjunction of one or more conjunctions of one or more literals. In other words, \(F\) can be expressed as a series of clauses connected by disjunctions (\(\lor \)), where each clause is a series of literals connected by conjunctions (\(\land \)). A literal is either a propositional variable or its negation.

\[ F = C_1 \lor C_2 \lor ... \lor C_n \]

Where each clause \(C_i\) is of the form:

\[ C_i = L_{i1} \land L_{i2} \land ... \land L_{im} \]

Quiz. Converting to DNF [000l]

November 22, 2025

Convert the following formula into Disjunctive Normal Form (DNF):

\[ (q \lor \neg \neg p) \land (\neg r \to s) \]

Solution.

November 22, 2025

Equisatisfiability

November 22, 2025

Definition. Equisatisfiability [000q]

November 22, 2025

Two formulas are said to be equisatisfiable if either both formulas are satisfiable or both are unsatisfiable. In other words, there exists an assignment of truth values to the variables that makes one formula true if and only if there exists; not necessarily the same assignment; that makes the other formula true. Equisatisfiability is a weaker condition than logical equivalence, as equisatisfiable formulas may not have the same truth values under all assignments, but they share the same satisfiability status.

\[ \texttt {equisat}(F, G) \iff (\exists I.\ I \models F) \iff (\exists J.\ J \models G) \]

Quiz. Equisatisfiability [000r]

November 22, 2025

If a formula \(F\) and \(G\) are equisatisfiable, then are they equivalent?

Solution.

November 22, 2025

No. We can answer this in a few different ways. In the most direct sense they are just definitionally not the same thing, in that equivalence requires that both formulas have the same truth value under all interpretations, whereas equisatisfiability only requires that both formulas have a satisfying interpretation or both be unsatisfiable. Another way to see it is that in an abstract sense equivalence describes an object-level relationship between formulas, whereas equisatisfiability describes a meta-level relationship about the existence of satisfying interpretations. Thus, they are fundamentally different kinds of relationships.

Tseitin Transformation

November 22, 2025

Definition. Conjunctive Normal Form (CNF) [000n]

November 22, 2025

A formula is in Conjunctive Normal Form (CNF) if it is expressed as a conjunction of disjunctions of literals. In other words, a CNF formula is a series of clauses (disjunctions) connected by AND operators. Each clause contains literals (variables or their negations) connected by OR operators. For example, the formula \((p \lor \neg q) \land (r \lor s \lor \neg t)\) is in CNF.

\[ F = C_1 \land C_2 \land ... \land C_n \]

Where each clause \(C_i\) is of the form:

\[ C_i = L_{i1} \lor L_{i2} \lor ... \lor L_{im} \]

Definition. Exponential Blow up problem [000m]

November 22, 2025

When converting a formula to Disjunctive Normal Form (DNF) or Conjunctive Normal Form (CNF), the size of the resulting formula can grow exponentially in the worst case. This is known as the exponential blow up problem. For example, a formula with \(n\) variables can result in a DNF or CNF with up to \(2^n\) clauses.

Definition. Tseytin's Transformation [000s]

November 22, 2025

Tseytin's transformation is a method used in propositional logic to convert any given formula into an equisatisfiable formula in Conjunctive Normal Form (CNF). The key idea behind Tseytin's transformation is to introduce new variables to represent subformulas of the original formula, thereby avoiding an exponential increase in size that can occur with naive CNF conversion methods. There are two key properties of Tseytin's for a formula \(F\) and its Tseytin transformation \(F'\):

unsatisfiability: \(F\) is unsatisfiable if and only if \(F'\) is unsatisfiable.
model correspondence: For every satisfying assignment (model) of \(F'\), there exists a corresponding satisfying assignment of \(F\), and vice versa, when restricted to the original variables of \(F\).

To demonstrate how it works lets consider the following formula

\[ \phi = ((p \lor q ) \land r) \to (\neg s) \]

Subformula identification: Identify the subformulas of \(\phi \) and assign a new variable to each subformula. For our example, we can identify the following subformulas and assign new variables: \[ \begin {align*} & \neg s \\ & p \lor q \\ & (p \lor q) \land r \\ & ((p \lor q) \land r) \to (\neg s) \end {align*} \]
Variable assignment: Assign new variables to each subformula: \[ \begin {align*} & x_1 \text { for } \neg s \\ & x_2 \text { for } p \lor q \\ & x_3 \text { for } (p \lor q) \land r \\ & x_4 \text { for } ((p \lor q) \land r) \to (\neg s) \end {align*} \]
Equivalence clauses: For each subformula, create clauses that enforce the equivalence between the new variable and the subformula it represents. For our example, we would create the following clauses: \[ \begin {align*} & (x_1 \leftrightarrow \neg s) \\ & (x_2 \leftrightarrow (p \lor q)) \\ & (x_3 \leftrightarrow (x_2 \land r)) \\ & (x_4 \leftrightarrow (x_3 \to x_1)) \end {align*} \]
Conjunct of clauses: Combine all the equivalence clauses into a single formula in CNF. The final formula \(\phi '\) will be the conjunction of all these clauses along with the clause that asserts the truth of the variable representing the entire formula (in this case, \(x_4\)): \[ \phi ' = (x_1 \leftrightarrow \neg s) \land (x_2 \leftrightarrow (p \lor q)) \land (x_3 \leftrightarrow (x_2 \land r)) \land (x_4 \leftrightarrow (x_3 \to x_1)) \land x_4 \]
Conversion to CNF: Finally, convert the combined formula into CNF using standard techniques (like distributing disjunctions over conjunctions). The resulting formula will be in CNF and equisatisfiable to the original formula \(\phi \). For example if we consider the clause \[ x_2 \leftrightarrow (p \lor q) \] this can be converted to CNF as \[ (x_2 \lor \neg p) \land (x_2 \lor \neg q) \land (\neg x_2 \lor p \lor q) \]

Quiz. Tseytin's Transformation [000t]

November 22, 2025

Lets consider the following formula

\[ F \triangleq (p \land q) \lor (p \land \neg r \land s) \]

Using Tseytin's transformation, convert the formula \(F\) into an equisatisfiable formula in CNF.

Solution.

November 22, 2025

For the sake of brevity, let's skip assume the subformula extraction is already done, and we created the following equivalence clauses: \[ \begin {align*} F_1 &\triangleq t_1 \leftrightarrow (\neg r \land s) \\ F_2 &\triangleq t_2 \leftrightarrow (p \land t_1) \\ F_3 &\triangleq t_3 \leftrightarrow (p \land q) \\ F_4 &\triangleq t_4 \leftrightarrow (t_2 \lor t_3) \end {align*} \] This gives us the following conjunct for the transformed formula: \[ F' \triangleq F_1 \land F_2 \land F_3 \land F_4 \land t_4 \]