209 Complexity — CNF Encoding
209.1 Overview
Since \(\mathrm{SAT}\) and \(3\mathrm{SAT}\) are languages of bit strings [AB09, Section 2.3.1], this module fixes a concrete binary encoding of CNF formulas over variables indexed by natural numbers: a literal \((v,b)\) is written as \(1^{v+1}0b\) (the variable index in unary), a clause as its literal encodings followed by \(0\), and a formula as its clause encodings, each prefixed by \(1\), followed by \(0\). It provides an exact-consumption parser for this grammar and a total decoder sending ill-formed strings to the empty formula [AB09, footnote 3], and proves that decoding inverts encoding and that the formula decoded from a string \(x\) has variable count at most \(|x|\).
Throughout, bit strings are finite words over \(\{ 0,1\} \) (with \(1\) standing for true and \(0\) for false), a literal is a pair \((v,b)\) of a variable index \(v \in \mathbb {N}\) and a polarity bit \(b \in \{ 0,1\} \), a clause is a finite list of literals, and a CNF formula is a finite list of clauses.
209.2 Declarations
For a literal \(\ell = (v, b)\), consisting of a variable index \(v \in \mathbb {N}\) and a polarity bit \(b \in \{ 0,1\} \), its binary encoding is the bit string \(\mathrm{enc}(\ell ) = 1^{v+1}\, 0\, b\) of length \(v+3\) (writing \(1\) for true and \(0\) for false): the index in unary as \(v+1\) ones, nonempty even when \(v = 0\), then a terminating \(0\), then the polarity bit \(b\).
Let \(C = (\ell _1, \dots , \ell _m)\) be a clause, i.e. a finite list of literals \(\ell _i = (v_i, b_i)\) with variable indices \(v_i \in \mathbb {N}\) and polarity bits \(b_i \in \{ 0,1\} \). Its binary encoding is the bit string
the concatenation of the literal encodings \(1^{v_i+1}0b_i\) followed by a closing \(0\); the closing bit is unambiguous because every literal encoding begins with \(1\).
Let \(\varphi = (C_1, \dots , C_k)\) be a CNF formula over variables indexed by \(\mathbb {N}\), given as a finite list of clauses, each a finite list of literals \((v,b)\) with \(v \in \mathbb {N}\) and \(b \in \{ 0,1\} \). Its binary encoding is
where a clause \((\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\). At the formula level a \(1\) announces another clause and a \(0\) ends the formula; in particular the empty formula is encoded as the single bit \(0\).
For a bit string \(x\), this operation returns the pair \((k, y)\) where \(k\) is the length of the longest prefix of \(x\) consisting only of \(1\)s and \(y\) is the rest of \(x\), so that \(x = 1^k y\) and \(y\) is either empty or begins with \(0\).
For a bit string \(x\), the literal parser succeeds exactly when \(x = 1^{k+1}\, 0\, b\, y\) for some \(k \in \mathbb {N}\), bit \(b \in \{ 0,1\} \) and bit string \(y\), in which case it returns the literal \((k, b)\), with variable index \(k\) and polarity \(b\), together with the unconsumed remainder \(y\). On every other input (one not beginning with \(1\), or one ending before the \(0\) and the polarity bit that follow its leading run of ones) it fails.
For a fuel bound \(f \in \mathbb {N}\) and a bit string \(x\), the clause parser with fuel \(f\) is defined by recursion on \(f\). If \(x = 0y\), it succeeds with the empty clause and remainder \(y\). If \(f = g + 1\) and \(x\) begins with \(1\), it reads one literal from the front of \(x\), which succeeds only when \(x = 1^{k+1}0by\) and then gives the literal \((k,b)\) and remainder \(y\); it then runs the clause parser with fuel \(g\) on \(y\), and if that returns a clause \(C\) with remainder \(z\), the result is the clause obtained by prepending \((k,b)\) to \(C\), with remainder \(z\). In every other case (empty input, fuel \(0\) on an input beginning with \(1\), or a failed sub-parse) it fails.
For a fuel bound \(f \in \mathbb {N}\) and a bit string \(x\), the formula parser with fuel \(f\) is defined by recursion on \(f\). If \(x = 0y\), it succeeds with the empty formula (no clauses) and remainder \(y\). If \(f = g+1\) and \(x = 1y\), it runs the clause parser with fuel \(g\) on \(y\) and, if this returns a clause \(C\) with remainder \(z\), runs the formula parser with fuel \(g\) on \(z\); if that returns a formula \(\psi \) with remainder \(w\), the result is the formula whose first clause is \(C\) followed by the clauses of \(\psi \), with remainder \(w\). In all other cases it fails. Here the clause parser with fuel \(g\) on a bit string \(u\) returns the empty clause and remainder \(u'\) when \(u = 0u'\); when \(g = h+1\) and \(u = 1^{j+1}0cu'\) it prepends the literal \((j,c)\) to the clause returned by the clause parser with fuel \(h\) on \(u'\), keeping that call’s remainder; and it fails otherwise.
For a bit string \(x\), the parser runs the fuel-bounded formula parser with fuel \(|x|\) on \(x\) and returns the resulting CNF formula \(\varphi \) if that run succeeds with empty remainder, i.e. consumes all of \(x\); it fails otherwise, in particular whenever trailing bits remain. The formula parser reads 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\) (read as the literal with variable index \(k \in \mathbb {N}\) and polarity \(b \in \{ 0,1\} \)), where the fuel bounds the recursion: with fuel \(g+1\), after reading the leading \(1\) of a clause the formula parser parses that clause and the remaining formula each with fuel \(g\), and after reading a literal the clause parser parses the rest of the clause with fuel \(g\); with fuel \(0\) only a terminating \(0\) can be read.
The fallback CNF formula over variables indexed by \(\mathbb {N}\) is the empty formula, consisting of no clauses; it is therefore satisfied by every assignment. It is the fixed formula to which bit strings that fail to parse are decoded, following [AB09, footnote 3].
For a bit string \(x\), its decoding \(\mathrm{dec}(x)\) is the CNF formula returned by the exact-consumption parser on \(x\) when that parse succeeds, and the empty formula (no clauses) otherwise. Here the parser reads \(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\} \)), and succeeds only if it consumes all of \(x\).
For every \(k \in \mathbb {N}\) and every bit string \(r\), splitting the bit string \(1^{k+1}\, 0\, r\) into its maximal leading run of \(1\)s and the remainder gives the run length \(k+1\) and the remainder \(0\, r\).
Let \(\ell = (v, b)\) be a literal with variable index \(v \in \mathbb {N}\) and polarity bit \(b \in \{ 0,1\} \), whose binary encoding is \(1^{v+1}0b\), and let \(r\) be any bit string. The literal parser, which on an input of the form \(1^{k+1}0cy\) returns the literal \((k,c)\) with remainder \(y\) and fails on every other input, succeeds on \(1^{v+1}0b\, r\) and returns \(\ell \) with remainder \(r\).
Let \(C = (\ell _1, \dots , \ell _m)\) be a clause of literals \(\ell _i = (v_i, b_i)\) with \(v_i \in \mathbb {N}\) and \(b_i \in \{ 0,1\} \), and let \(\mathrm{enc}(C) = 1^{v_1+1}0b_1\cdots 1^{v_m+1}0b_m\, 0\) be its binary encoding. For every bit string \(r\) and every fuel \(f \ge |\mathrm{enc}(C)|\), the clause parser with fuel \(f\) succeeds on \(\mathrm{enc}(C)\, r\) and returns \(C\) with remainder \(r\). Here the clause parser with fuel \(f\) on an input \(x\) returns the empty clause and remainder \(y\) when \(x = 0y\); when \(f = g+1\) and \(x = 1^{k+1}0cy\) it prepends the literal \((k,c)\) to the clause returned by the clause parser with fuel \(g\) on \(y\), keeping that call’s remainder and failing if it fails; and it fails on every other input.
Let \(\varphi = (C_1,\dots ,C_k)\) be a CNF formula over variables indexed by \(\mathbb {N}\), and let \(\mathrm{enc}(\varphi ) = 1\, \mathrm{enc}(C_1)\cdots 1\, \mathrm{enc}(C_k)\, 0\) be its binary encoding, where a clause with literals \((v_1,b_1),\dots ,(v_m,b_m)\) is encoded as \(1^{v_1+1}0b_1\cdots 1^{v_m+1}0b_m\, 0\). For every bit string \(r\) and every fuel \(f \ge |\mathrm{enc}(\varphi )|\), the formula parser with fuel \(f\) succeeds on \(\mathrm{enc}(\varphi )\, r\) and returns \(\varphi \) with remainder \(r\). Here the formula parser with fuel \(f\) on an input \(x\) returns the empty formula and remainder \(y\) when \(x = 0y\); when \(f = g+1\) and \(x = 1y\) it parses a clause \(C\) from \(y\) with fuel \(g\), leaving \(z\), then a formula \(\psi \) from \(z\) with fuel \(g\), leaving \(w\), and returns \(C\) followed by the clauses of \(\psi \) with remainder \(w\); and it fails otherwise. The clause parser with fuel \(g\) on \(u\) returns the empty clause and remainder \(u'\) when \(u = 0u'\), and when \(g = h+1\) and \(u = 1^{j+1}0cu'\) it prepends the literal \((j,c)\) to the clause parsed from \(u'\) with fuel \(h\), keeping that remainder; it fails otherwise.
For every CNF formula \(\varphi \) over variables indexed by \(\mathbb {N}\), the exact-consumption parser applied to the binary encoding \(\mathrm{enc}(\varphi )\) succeeds and returns \(\varphi \). Here a literal \((v,b)\) is encoded as \(1^{v+1}0b\), a clause as the concatenation of its literal encodings followed by \(0\), and a formula \((C_1,\dots ,C_k)\) as \(1\, \mathrm{enc}(C_1)\cdots 1\, \mathrm{enc}(C_k)\, 0\); the parser on a bit string \(x\) reads \(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)\)), and succeeds only if it consumes all of \(x\).
For every CNF formula \(\varphi \) over variables indexed by \(\mathbb {N}\), \(\mathrm{dec}(\mathrm{enc}(\varphi )) = \varphi \). Here a literal \((v,b)\) is encoded as \(1^{v+1}0b\), a clause as the concatenation of its literal encodings followed by \(0\), and a formula \((C_1,\dots ,C_k)\) as \(1\, \mathrm{enc}(C_1)\cdots 1\, \mathrm{enc}(C_k)\, 0\); and \(\mathrm{dec}(x)\) is the formula obtained by parsing the bit string \(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 the empty formula otherwise.
For every bit string \(x\), if \(k\) is the length of the longest prefix of \(x\) consisting only of \(1\)s and \(y\) is the remainder of \(x\) after that prefix, then \(k + |y| = |x|\).
Let \(x\) and \(r\) be bit strings and let \((v, b)\) be a literal with \(v \in \mathbb {N}\) and \(b \in \{ 0,1\} \). If the literal parser, which on an input \(1^{k+1}0cy\) returns the literal \((k,c)\) with remainder \(y\) and fails on every other input, returns \((v,b)\) with remainder \(r\) when applied to \(x\), then \(v + 3 + |r| = |x|\).
Let \(f \in \mathbb {N}\), let \(x\) and \(r\) be bit strings and let \(C\) be a clause of literals \((v,b)\) with \(v \in \mathbb {N}\) and \(b \in \{ 0,1\} \). Suppose the clause parser with fuel \(f\) succeeds on \(x\) and returns \(C\) with remainder \(r\). Then \(|r| \le |x|\), and every literal \((v,b)\) of \(C\) satisfies \(v + 1 + |r| \le |x|\). Here the clause parser with fuel \(f\) on \(x\) returns the empty clause and remainder \(y\) when \(x = 0y\); when \(f = g+1\) and \(x = 1^{k+1}0cy\) it prepends the literal \((k,c)\) to the clause returned by the clause parser with fuel \(g\) on \(y\), keeping that call’s remainder and failing if it fails; and it fails on every other input.
Let \(f \in \mathbb {N}\), let \(x\) and \(r\) be bit strings and let \(\varphi \) be a CNF formula over variables indexed by \(\mathbb {N}\). Suppose the formula parser with fuel \(f\) succeeds on \(x\) and returns \(\varphi \) with remainder \(r\). Then \(|r| \le |x|\), and every literal \((v,b)\) of every clause of \(\varphi \) satisfies \(v + 1 + |r| \le |x|\). Here the formula parser with fuel \(f\) on \(x\) returns the empty formula and remainder \(y\) when \(x = 0y\); when \(f = g+1\) and \(x = 1y\) it parses a clause \(C\) from \(y\) with fuel \(g\), leaving \(z\), then a formula \(\psi \) from \(z\) with fuel \(g\), leaving \(w\), and returns \(C\) followed by the clauses of \(\psi \) with remainder \(w\); and it fails otherwise. The clause parser with fuel \(g\) on \(u\) returns the empty clause and remainder \(u'\) when \(u = 0u'\), and when \(g = h+1\) and \(u = 1^{j+1}0cu'\) it prepends the literal \((j,c)\) to the clause parsed from \(u'\) with fuel \(h\), keeping that remainder; it fails otherwise.
Let \(\varphi \) be a CNF formula over variables indexed by \(\mathbb {N}\) and let \(n \in \mathbb {N}\). If every literal \((v,b)\) of every clause of \(\varphi \) satisfies \(v + 1 \le n\), then \(N(\varphi ) \le n\), where the variable count \(N(\varphi )\) is one plus the largest variable index occurring in a literal of \(\varphi \), or \(0\) if \(\varphi \) contains no literal.
For every bit string \(x\), the decoded formula satisfies \(N(\mathrm{dec}(x)) \le |x|\). Here the variable count \(N(\varphi )\) of a CNF formula \(\varphi \) is one plus the largest variable index occurring in a literal of \(\varphi \), or \(0\) if no literal occurs, and \(\mathrm{dec}(x)\) is the formula 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 formula otherwise.