OAI.VertexCover.explicit_cover_gap

The theorem states that for every natural number m with m ≥ 4, the type GapReduction(m) is nonempty, i.e. a gap reduction from 3-SAT to vertex cover with parameter m exists. Such a reduction consists of a map construct sending each bit-string input to an explicit graph on n vertices Fin n, given as a duplicate-free list of edges (i,j) with i<j, together with a proof that construct is computable by a polynomial-time two-stack Turing machine (TM2) whose output is read via the graph's binary encoding, and whose machine has a finite alphabet at every stack. Here 3-SAT of an input means that the input decodes, under the prefix-framed binary encoding of clauses of three literals, to a satisfiable formula. The reduction must satisfy completeness: if the input is a satisfiable 3-SAT instance, the minimum vertex cover size of the constructed graph is strictly less than (1/2 + 1/m)·n. It must also satisfy soundness: if the input is not satisfiable (including inputs that fail to decode), the minimum vertex cover size is strictly greater than (1 − 1/m)·n.