sat2vc

The program sat2vc transforms instances of the SAT problem [1] given in the DIMACS format [4] into instances of the Vertex Cover [2] problem in the PACE graph format [5]. The transformation uses a the standard reduction by Richard Karp [3]. It reduces instances from CNF-SAT to 3CNF-SAT and then reduces directly to SAT by concatenated the reductions by Karp.

(The reduction does additionally produce an instance of the clique problem, which was the case in the original reduction by reducing SAT-> CLIQUE, CLIQUE -> VC).

Download:

git clone git@github.com:daajoe/sat2vc.git

References

1. SAT Problem
2. Vertex Cover Problem
3. Richard M. Karp (1972). "Reducibility Among Combinatorial Problems" (PDF). In R. E. Miller; J. W. Thatcher; J.D. Bohlinger (eds.). Complexity of Computer Computations. New York: Plenum. pp. 85–103. doi:10.1007/978-1-4684-2001-2_9.
4. DIMACS CNF format .cnf
5. PACE graph format .gr