208 Complexity — CNF
208.1 Overview
This module supplies the conjunctive-normal-form layer used by the development of \(\mathrm{SAT}\), \(3\mathrm{SAT}\) and the Cook–Levin theorem [AB09, Section 2.3.1]: satisfiability of a CNF formula, the variable count of a formula, clause-width bounds (\(k\)CNF), the fact that evaluation reads only the variables below the variable count, and CNF universality [AB09, Claim 2.13], namely that every Boolean function on \(\ell \) bits is computed by a CNF formula with at most \(2^\ell \) clauses, each of width at most \(\ell \).
Throughout this chapter a CNF formula is a finite list of clauses, each clause a finite list of literals; a literal \(x_v^b\) consists of a variable \(v\) and a polarity \(b \in \{ 0,1\} \) and is satisfied by an assignment \(a\) exactly when \(a(v) = b\). A formula evaluates to true under \(a\) when every clause contains a satisfied literal, so the formula with no clauses is true and an empty clause is false.
208.2 Declarations
Let \(\alpha \) be a type of variables and let \(\varphi \) be a CNF formula over \(\alpha \), that is, a conjunction of clauses, each a disjunction of literals \(x_v^b\) (\(v \in \alpha \), \(b \in \{ 0,1\} \)), where \(x_v^b\) is satisfied by an assignment \(a\) exactly when \(a(v) = b\). The formula \(\varphi \) is satisfiable if there exists an assignment \(a : \alpha \to \{ 0,1\} \) under which \(\varphi \) evaluates to true [AB09, Section 2.3.1].
Let \(\varphi \) be a CNF formula whose variables are indexed by natural numbers. Its variable count \(N(\varphi )\) is one plus the largest index of a variable occurring in some literal of \(\varphi \), and \(0\) if no literal occurs in \(\varphi \) (for instance when \(\varphi \) has no clauses, or only empty clauses). Equivalently, \(N(\varphi )\) is the least \(N \in \mathbb {N}\) such that every variable occurring in \(\varphi \) has index less than \(N\).
Let \(\alpha \) be a type of variables, let \(\varphi \) be a CNF formula over \(\alpha \), and let \(k \in \mathbb {N}\). The formula \(\varphi \) has width at most \(k\) (is a \(k\)CNF) if every clause of \(\varphi \) contains at most \(k\) literals [AB09, Section 2.3.1]. In particular, a formula with no clauses has width at most \(k\) for every \(k\).
For a finite list \(s\) of natural numbers, write \(\max (s)\) for the right fold of \(\max \) over \(s\) with initial value \(0\) (so the empty list has maximum \(0\)). If \(n\) is a member of \(s\), then \(n \le \max (s)\).
Let \(\varphi \) be a CNF formula whose variables are indexed by natural numbers, and let \(N(\varphi )\) be one plus the largest variable index occurring in \(\varphi \) (\(0\) if no variable occurs). If two assignments \(a, b : \mathbb {N} \to \{ 0,1\} \) satisfy \(a(v) = b(v)\) for every \(v \lt N(\varphi )\), then \(\varphi \) evaluates to the same truth value under \(a\) as under \(b\).
Let \(s\) be a finite list of natural numbers, write \(\max (s)\) for the right fold of \(\max \) over \(s\) with initial value \(0\), and let \(n \in \mathbb {N}\). If every member of \(s\) is at most \(n\), then \(\max (s) \le n\); in particular this holds when \(s\) is empty.
Let \(\ell \in \mathbb {N}\) and \(v = (v_0, \dots , v_{\ell -1}) \in \{ 0,1\} ^\ell \). The clause excluding \(v\) is
the disjunction, in order of \(i\), of \(\ell \) literals on the variables \(x_0, \dots , x_{\ell -1}\), where the literal \(x_i^{\neg v_i}\) is satisfied by an assignment \(a : \mathbb {N} \to \{ 0,1\} \) exactly when \(a(i) \ne v_i\) [AB09, Claim 2.13].
Let \(\ell \in \mathbb {N}\), let \(v \in \{ 0,1\} ^\ell \), and let \(C_v = \bigvee _{i\lt \ell } x_i^{\neg v_i}\) be the clause on the variables \(x_0, \dots , x_{\ell -1}\) whose \(i\)-th literal is satisfied by an assignment \(a\) exactly when \(a(i) \ne v_i\). For every assignment \(a : \mathbb {N} \to \{ 0,1\} \), the clause \(C_v\) evaluates to false under \(a\) if and only if \(a(i) = v_i\) for all \(i \lt \ell \) [AB09, Claim 2.13].
Let \(\ell \in \mathbb {N}\) and let \(f : \{ 0,1\} ^\ell \to \{ 0,1\} \). The truth-table CNF \(\varphi _f\) of \(f\) is the conjunction, over all \(v \in \{ 0,1\} ^\ell \) with \(f(v) = 0\), of the clause \(C_v = \bigvee _{i\lt \ell } x_i^{\neg v_i}\), whose \(i\)-th literal is satisfied by an assignment \(a : \mathbb {N} \to \{ 0,1\} \) exactly when \(a(i) \ne v_i\) [AB09, Claim 2.13].
Let \(\ell \in \mathbb {N}\), let \(f : \{ 0,1\} ^\ell \to \{ 0,1\} \), and let \(\varphi _f\) be the CNF formula that is the conjunction, over all \(v \in \{ 0,1\} ^\ell \) with \(f(v) = 0\), of the clause \(\bigvee _{i\lt \ell } x_i^{\neg v_i}\) whose \(i\)-th literal is satisfied by an assignment \(a\) exactly when \(a(i) \ne v_i\). Then every variable occurring in \(\varphi _f\) has index less than \(\ell \); that is, one plus the largest variable index occurring in \(\varphi _f\) (or \(0\) if none occurs) is at most \(\ell \).
Let \(\ell \in \mathbb {N}\), let \(f : \{ 0,1\} ^\ell \to \{ 0,1\} \), and let \(\varphi _f\) be the CNF formula that is the conjunction, over all \(v \in \{ 0,1\} ^\ell \) with \(f(v) = 0\), of the clause \(\bigvee _{i\lt \ell } x_i^{\neg v_i}\) whose \(i\)-th literal is satisfied by an assignment \(a\) exactly when \(a(i) \ne v_i\). Then \(\varphi _f\) has at most \(2^\ell \) clauses.
Let \(\ell \in \mathbb {N}\), let \(f : \{ 0,1\} ^\ell \to \{ 0,1\} \), and let \(\varphi _f\) be the CNF formula that is the conjunction, over all \(v \in \{ 0,1\} ^\ell \) with \(f(v) = 0\), of the clause \(\bigvee _{i\lt \ell } x_i^{\neg v_i}\) whose \(i\)-th literal is satisfied by an assignment \(a\) exactly when \(a(i) \ne v_i\). Then every clause of \(\varphi _f\) contains at most \(\ell \) literals, i.e. \(\varphi _f\) is an \(\ell \)CNF.
Let \(\ell \in \mathbb {N}\), let \(f : \{ 0,1\} ^\ell \to \{ 0,1\} \), and let \(\varphi _f\) be the CNF formula that is the conjunction, over all \(v \in \{ 0,1\} ^\ell \) with \(f(v) = 0\), of the clause \(\bigvee _{i\lt \ell } x_i^{\neg v_i}\) whose \(i\)-th literal is satisfied by an assignment \(a\) exactly when \(a(i) \ne v_i\). Then for every assignment \(a : \mathbb {N} \to \{ 0,1\} \), the formula \(\varphi _f\) evaluates under \(a\) to \(f(a(0), a(1), \dots , a(\ell -1))\).
For every \(\ell \in \mathbb {N}\) and every Boolean function \(f : \{ 0,1\} ^\ell \to \{ 0,1\} \) there exists a CNF formula \(\varphi \) over variables indexed by natural numbers such that: every variable occurring in \(\varphi \) has index less than \(\ell \) (one plus the largest occurring index, or \(0\) if none occurs, is at most \(\ell \)); \(\varphi \) has at most \(2^\ell \) clauses; every clause of \(\varphi \) contains at most \(\ell \) literals; and for every assignment \(a : \mathbb {N} \to \{ 0,1\} \), the formula \(\varphi \) evaluates under \(a\) to \(f(a(0), a(1), \dots , a(\ell -1))\) [AB09, Claim 2.13].