210 Complexity — DNF
210.1 Overview
In [AB09, Section 2.6.1, Example 2.21] the Cook–Levin CNF formula is negated and one asks whether the negation is a tautology; the negation of a CNF formula is a DNF formula, an OR of ANDs of literals. This module supplies that dual layer: DNF formulas over variables indexed by natural numbers, their evaluation and the tautology predicate, a binary encoding shared with CNF formulas, the size-preserving De Morgan duals between CNF and DNF formulas (which negate every literal in place), and the De Morgan bridge stating that the dual of a CNF formula is a tautology exactly when the CNF formula is unsatisfiable.
Throughout, a literal is a pair \((v,b)\) of a variable index \(v \in \mathbb {N}\) and a polarity bit \(b \in \{ 0,1\} \), satisfied by an assignment \(a : \mathbb {N} \to \{ 0,1\} \) exactly when \(a(v) = b\). A CNF formula is a finite list of clauses, each a finite list of literals, true under \(a\) when every clause contains a satisfied literal; a DNF formula is a finite list of terms, each a finite list of literals, true under \(a\) when some term has all its literals satisfied.
210.2 Declarations
A DNF formula over variables indexed by \(\mathbb {N}\) is a finite list of terms \((T_1, \dots , T_k)\), where each term \(T_i\) is a finite list of literals \((v, b)\) with variable index \(v \in \mathbb {N}\) and polarity bit \(b \in \{ 0,1\} \). Each term is read as the conjunction of its literals and the formula as the disjunction of its terms; the syntax is the same list-of-literal-lists shape as a CNF formula over \(\mathbb {N}\), but it carries this dual reading.
Let \(\psi = (T_1, \dots , T_k)\) be a DNF formula over variables indexed by \(\mathbb {N}\), each term \(T_i\) a finite list of literals \((v,b)\) with \(v \in \mathbb {N}\) and \(b \in \{ 0,1\} \), and let \(a : \mathbb {N} \to \{ 0,1\} \) be an assignment. The value \(\psi (a) \in \{ 0,1\} \) is true exactly when some term \(T_i\) has all of its literals satisfied by \(a\), a literal \((v,b)\) being satisfied when \(a(v) = b\):
In particular the formula with no terms evaluates to false under every assignment, and an empty term is satisfied by every assignment [AB09, Section 2.6.1].
Let \(\psi = (T_1, \dots , T_k)\) be a DNF formula over variables indexed by \(\mathbb {N}\), each term a finite list of literals \((v,b)\) with \(v \in \mathbb {N}\) and \(b \in \{ 0,1\} \). The formula \(\psi \) is a tautology if for every assignment \(a : \mathbb {N} \to \{ 0,1\} \) some term \(T_i\) has all of its literals satisfied by \(a\), where \((v,b)\) is satisfied when \(a(v) = b\); that is, \(\psi \) evaluates to true under every assignment [AB09, Section 2.6.1].
For a bit string \(x\), its DNF decoding is the DNF formula whose list of terms is the list of clauses of the CNF decoding \(\mathrm{dec}(x)\). Here \(\mathrm{dec}(x)\) is the list of literal lists obtained by parsing \(x\), with recursion fuel \(|x|\), according to the grammar \(\langle \text{formula}\rangle ::= 0 \mid 1\, \langle \text{clause}\rangle \, \langle \text{formula}\rangle \), \(\langle \text{clause}\rangle ::= 0 \mid \langle \text{literal}\rangle \, \langle \text{clause}\rangle \), \(\langle \text{literal}\rangle ::= 1^{k+1}\, 0\, b\) (the literal with variable index \(k \in \mathbb {N}\) and polarity \(b \in \{ 0,1\} \)) when this parse consumes all of \(x\), and the empty list otherwise; so a malformed string decodes to the DNF formula with no terms.
Let \(\psi = (T_1, \dots , T_k)\) be a DNF formula over variables indexed by \(\mathbb {N}\), each term a finite list of literals \((v,b)\) with \(v \in \mathbb {N}\) and \(b \in \{ 0,1\} \). Its binary encoding is the binary encoding of the same list of literal lists read as a CNF formula,
where a term \((\ell _1, \dots , \ell _m)\) is encoded as \(\mathrm{enc}(\ell _1)\cdots \mathrm{enc}(\ell _m)\, 0\) and a literal \((v,b)\) as \(1^{v+1}0b\).
For every DNF formula \(\psi \) over variables indexed by \(\mathbb {N}\), decoding its binary encoding as a DNF formula returns \(\psi \). Here a DNF formula \((T_1,\dots ,T_k)\), each term a list of literals \((v,b)\) with \(v \in \mathbb {N}\) and \(b \in \{ 0,1\} \), is encoded as \(1\, \mathrm{enc}(T_1)\cdots 1\, \mathrm{enc}(T_k)\, 0\), a term as the concatenation of its literal encodings \(1^{v+1}0b\) followed by \(0\); and a bit string \(x\) is decoded as the DNF formula whose terms are the literal lists obtained by parsing \(x\), with recursion fuel \(|x|\), according to the grammar \(\langle \text{formula}\rangle ::= 0 \mid 1\, \langle \text{clause}\rangle \, \langle \text{formula}\rangle \), \(\langle \text{clause}\rangle ::= 0 \mid \langle \text{literal}\rangle \, \langle \text{clause}\rangle \), \(\langle \text{literal}\rangle ::= 1^{k+1}\, 0\, b\) (the literal \((k,b)\)) when this parse consumes all of \(x\), and as the formula with no terms otherwise.
Let \(\varphi = (C_1, \dots , C_k)\) be a CNF formula over variables indexed by \(\mathbb {N}\), each clause a list of literals \((v,b)\) with \(v \in \mathbb {N}\) and \(b \in \{ 0,1\} \), with binary encoding \(\mathrm{enc}(\varphi ) = 1\, \mathrm{enc}(C_1)\cdots 1\, \mathrm{enc}(C_k)\, 0\), where a clause is encoded as the concatenation of its literal encodings \(1^{v+1}0b\) followed by \(0\). Then decoding \(\mathrm{enc}(\varphi )\) as a DNF formula yields the DNF formula whose terms are exactly \(C_1, \dots , C_k\). Here a bit string \(x\) is decoded as the DNF formula whose terms are the literal lists obtained by parsing \(x\), with recursion fuel \(|x|\), according to the grammar \(\langle \text{formula}\rangle ::= 0 \mid 1\, \langle \text{clause}\rangle \, \langle \text{formula}\rangle \), \(\langle \text{clause}\rangle ::= 0 \mid \langle \text{literal}\rangle \, \langle \text{clause}\rangle \), \(\langle \text{literal}\rangle ::= 1^{k+1}\, 0\, b\) when this parse consumes all of \(x\), and as the formula with no terms otherwise.
Let \(\psi = (T_1, \dots , T_k)\) be a DNF formula over variables indexed by \(\mathbb {N}\), each term a finite list of literals \((v,b)\) with \(v \in \mathbb {N}\) and \(b \in \{ 0,1\} \). Its De Morgan dual is the CNF formula \((T_1', \dots , T_k')\), where the clause \(T_i'\) is obtained from \(T_i\) by replacing every literal \((v,b)\) with \((v, \neg b)\), keeping the order. Thus if \(\psi = \bigvee _i \bigwedge _j \ell _{ij}\), its dual is the CNF formula \(\bigwedge _i \bigvee _j \neg \ell _{ij}\), of the same size.
Let \(\varphi = (C_1, \dots , C_k)\) be a CNF formula over variables indexed by \(\mathbb {N}\), each clause a finite list of literals \((v,b)\) with \(v \in \mathbb {N}\) and \(b \in \{ 0,1\} \). Its De Morgan dual is the DNF formula \((C_1', \dots , C_k')\), where the term \(C_i'\) is obtained from \(C_i\) by replacing every literal \((v,b)\) with \((v, \neg b)\), keeping the order. Thus if \(\varphi = \bigwedge _i \bigvee _j \ell _{ij}\), its dual is the DNF formula \(\bigvee _i \bigwedge _j \neg \ell _{ij}\); no distributive expansion takes place, and the dual has the same size as \(\varphi \).
Let \(\varphi = (C_1, \dots , C_k)\) be a CNF formula over variables indexed by \(\mathbb {N}\), each clause a finite list of literals \((v,b)\) with \(v \in \mathbb {N}\) and \(b \in \{ 0,1\} \), and let \(\varphi ^{\ast }\) be the DNF formula whose terms are obtained from \(C_1, \dots , C_k\) by replacing every literal \((v,b)\) with \((v, \neg b)\). Then for every assignment \(a : \mathbb {N} \to \{ 0,1\} \),
where \(\varphi (a)\) is true when every clause of \(\varphi \) contains a literal \((v,b)\) with \(a(v) = b\), and \(\varphi ^{\ast }(a)\) is true when some term of \(\varphi ^{\ast }\) has all of its literals \((v,b)\) satisfying \(a(v) = b\).
Let \(\varphi \) be a CNF formula over variables indexed by \(\mathbb {N}\), a finite list of clauses each a finite list of literals \((v,b)\) with \(v \in \mathbb {N}\) and \(b \in \{ 0,1\} \). Forming its De Morgan dual DNF formula, by replacing every literal \((v,b)\) with \((v,\neg b)\) and reading the clauses as terms, and then forming the De Morgan dual CNF formula of that DNF formula, by again replacing every literal \((v,b)\) with \((v,\neg b)\) and reading the terms as clauses, returns \(\varphi \).
Let \(\psi \) be a DNF formula over variables indexed by \(\mathbb {N}\), a finite list of terms each a finite list of literals \((v,b)\) with \(v \in \mathbb {N}\) and \(b \in \{ 0,1\} \). Forming its De Morgan dual CNF formula, by replacing every literal \((v,b)\) with \((v,\neg b)\) and reading the terms as clauses, and then forming the De Morgan dual DNF formula of that CNF formula, by again replacing every literal \((v,b)\) with \((v,\neg b)\) and reading the clauses as terms, returns \(\psi \).
Let \(\varphi = (C_1, \dots , C_k)\) be a CNF formula over variables indexed by \(\mathbb {N}\), each clause a finite list of literals \((v,b)\) with \(v \in \mathbb {N}\) and \(b \in \{ 0,1\} \), and let \(\varphi ^{\ast }\) be the DNF formula whose terms are obtained from \(C_1, \dots , C_k\) by replacing every literal \((v,b)\) with \((v, \neg b)\). Then \(\varphi ^{\ast }\) is a tautology, i.e. for every assignment \(a : \mathbb {N} \to \{ 0,1\} \) some term of \(\varphi ^{\ast }\) has all of its literals \((v,b)\) satisfying \(a(v) = b\), if and only if \(\varphi \) is unsatisfiable, i.e. no assignment makes every clause of \(\varphi \) contain a literal \((v,b)\) with \(a(v) = b\) [AB09, Section 2.6.1, Example 2.21].