95 Complexity — Three SAT To Clique
95.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.
95.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\).
For any two literals \(l_1\) and \(l_2\), \(\mathtt{literalsConflict}\, l_1\, l_2 \iff \mathtt{literalsConflict}\, l_2\, l_1\).
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\).
If an assignment \(\alpha \) makes both \(l_1\) and \(l_2\) true, then \(l_1\) and \(l_2\) do not conflict: \(\mathtt{evalLiteral}\, \alpha \, l_1 \to \mathtt{evalLiteral}\, \alpha \, l_2 \to \neg \, \mathtt{literalsConflict}\, l_1\, l_2\).
If \(s\) is a set of \(m\) vertices forming a clique in the conflict graph of a formula \(f\) with \(m\) clauses, then for every clause index \(i : \mathrm{Fin}\, m\) there is exactly one vertex \(u \in s\) with \(u.c\_ idx = i\).
If \(v\) is a clique vertex with \(v.c\_ idx = i\), then the literal \(\mathtt{getLitAt}\, f\, v\) is one of the three literals \(l_1\), \(l_2\), \(l_3\) of clause \(f[i]\).
If a 3-CNF formula \(f\) with \(m\) clauses is satisfiable, then the conflict graph \(\mathtt{toCliqueGraph}\, f\) contains an \(m\)-clique: \(\mathtt{is3Satisfiable}\, f \to \mathtt{hasClique}\, (\mathtt{toCliqueGraph}\, f)\, f.\mathtt{length}\).
If the conflict graph of a 3-CNF formula \(f\) with \(m\) clauses contains an \(m\)-clique, then \(f\) is satisfiable: \(\mathtt{hasClique}\, (\mathtt{toCliqueGraph}\, f)\, f.\mathtt{length} \to \mathtt{is3Satisfiable}\, f\).
A 3-CNF formula \(f\) is satisfiable if and only if its conflict graph contains a clique of size \(f.\mathtt{length}\):