92 Complexity — Three SAT To Clique
92.1 Overview
This module formalises the classical NP-hardness reduction from 3-SAT to the Clique problem. Given a 3-CNF formula \(f\) with \(m\) clauses, a conflict graph is constructed whose vertices are pairs (clause index, literal position) and whose edges connect vertices from different clauses whose literals are not complementary; the main results establish that \(f\) is satisfiable if and only if the conflict graph contains an \(m\)-clique.
92.2 Declarations
A clause is a list of literals over a variable type \(V\); it represents a disjunction of those literals.
A CNF formula over \(V\) is a list of clauses, representing the conjunction of those clauses.
Given a truth assignment \(\alpha : V \to \mathrm{Prop}\), the evaluation of a literal \(\ell \) under \(\alpha \) is \(\alpha (v)\) when \(\ell = \texttt{pos}\, v\) and \(\neg \, \alpha (v)\) when \(\ell = \texttt{neg}\, v\).
A clause \(c\) is satisfied by assignment \(\alpha \) if at least one literal \(\ell \in c\) satisfies \(\mathtt{evalLiteral}\, \alpha \, \ell \).
A CNF formula \(f\) is satisfied by \(\alpha \) if every clause \(c \in f\) is satisfied by \(\alpha \).
A CNF formula \(f\) is satisfiable if there exists an assignment \(\alpha \) that satisfies \(f\).
A 3-clause over \(V\) is a structure with exactly three literals \(l_1, l_2, l_3 : \mathtt{Literal}\, V\), representing a disjunction of precisely three literals.
A 3-CNF formula over \(V\) is a list of 3-clauses, representing their conjunction.
A 3-clause \(c\) is satisfied by \(\alpha \) if at least one of its three literals \(c.l_1\), \(c.l_2\), \(c.l_3\) evaluates to true under \(\alpha \).
A 3-CNF formula \(f\) is satisfied by \(\alpha \) if every 3-clause \(c \in f\) is satisfied by \(\alpha \).
A 3-CNF formula \(f\) is satisfiable if there exists an assignment \(\alpha \) such that \(\alpha \) satisfies \(f\).
A vertex of the conflict graph for a formula with \(m\) clauses is a pair \(\langle c\_ idx, l\_ idx \rangle \) where \(c\_ idx : \mathrm{Fin}\, m\) is a clause index and \(l\_ idx : \mathrm{Fin}\, 3\) is a literal position within that clause.
Given a 3-clause \(c\) and a position \(p : \mathrm{Fin}\, 3\), returns the \(p\)-th literal of \(c\): \(c.l_1\) at position \(0\), \(c.l_2\) at position \(1\), and \(c.l_3\) at position \(2\).
Given a 3-CNF formula \(f\) and a vertex \(v : \mathtt{CliqueVertex}\, f.\mathtt{length}\), returns the literal at position \(v.l\_ idx\) within clause \(f[v.c\_ idx]\). The type of \(v\) guarantees the index is always in bounds.
Two literals \(l_1\) and \(l_2\) conflict if one is the positive and the other the negative occurrence of the same variable, i.e. \(l_1 = \texttt{pos}\, v\) and \(l_2 = \texttt{neg}\, v\) (or vice versa) for some \(v\).
Call two literals over a variable set *conflicting* when one is the positive and the other the negative occurrence of one and the same variable. For any two literals \(l_1\) and \(l_2\), \(l_1\) and \(l_2\) conflict if and only if \(l_2\) and \(l_1\) conflict; that is, the conflict relation is symmetric.
The conflict graph of a 3-CNF formula \(f\) is the simple graph on vertex set \(\mathtt{CliqueVertex}\, f.\mathtt{length}\) in which two vertices \(u\) and \(v\) are adjacent if and only if they come from different clauses (\(u.c\_ idx \ne v.c\_ idx\)) and their respective literals do not conflict.
A graph \(G\) on vertex type \(V\) has a \(k\)-clique if there exists a finite set \(s \subseteq V\) of \(k\) vertices that are pairwise adjacent in \(G\).
Let \(\alpha \) be a truth assignment on a set \(V\) of variables, and let \(\ell _1,\ell _2\) be literals over \(V\), each of the form \(\mathrm{pos}\, v\) (the variable \(v\)) or \(\mathrm{neg}\, v\) (its negation). If both \(\ell _1\) and \(\ell _2\) evaluate to true under \(\alpha \), then they do not conflict; that is, they are not the positive and negative occurrences of one and the same variable.
Let \(f\) be a 3-CNF formula with \(m\) clauses, and let \(s\) be a set of vertices of the conflict graph of \(f\). Suppose that \(s\) has exactly \(m\) elements and forms a clique, meaning any two distinct vertices of \(s\) are adjacent. Then for every clause index \(i \in \mathrm{Fin}\, m\) there is exactly one vertex \(u \in s\) whose clause component equals \(i\).
Let \(f\) be a 3-CNF formula, let \(v\) be a vertex of the conflict graph of \(f\), and let \(i\) be a clause index of \(f\) such that the clause component of \(v\) equals \(i\). Then the literal named by \(v\) is one of the three literals \(l_1, l_2, l_3\) of the clause \(f[i]\).
Let \(f\) be a 3-CNF formula consisting of \(m\) clauses, and let its conflict graph be the simple graph on the vertices \(\langle c, \ell \rangle \) (clause index \(c\), literal position \(\ell \)) in which two vertices are adjacent exactly when they belong to different clauses and their literals do not conflict. If \(f\) is satisfiable, then this conflict graph has an \(m\)-clique.
Let \(f\) be a 3-CNF formula consisting of \(m\) clauses. If the conflict graph of \(f\) has an \(m\)-clique, then \(f\) is satisfiable.
Let \(f\) be a 3-CNF formula with \(m\) clauses. Then \(f\) is satisfiable if and only if its conflict graph has a clique of size \(m\); that is, the graph whose vertices are the literal positions of \(f\), with two positions adjacent exactly when they lie in different clauses and their literals do not conflict, contains \(m\) pairwise-adjacent vertices precisely when some truth assignment satisfies every clause of \(f\).
92.3 Additional declarations
A literal over a variable type \(V\) is either a positive occurrence \(\mathrm{pos}\, v\) or a negative occurrence \(\mathrm{neg}\, v\) of a variable \(v \in V\): the former asserts the variable itself, the latter asserts its negation.