3-SAT reduction to vertex cover (source code)

= 3-SAT reduction to vertex cover
{c}

A <polynomial-time many-one reduction> represents each variable by an adjacent literal pair and each clause by a <triangle in a graph>. Connect each occurrence vertex to its corresponding literal vertex. A <vertex cover> of size $n+2m$ must choose one literal vertex per variable and two vertices per clause, and its omitted clause vertex forces a true literal. Conversely a satisfying <Boolean valuation> supplies such a cover. This establishes <NP-hardness> of the vertex-cover decision problem from <3-SAT>.