Does anyone know if there is an implementation of Cook-Levin?
A program that gets an input like the following:
- $M$: the code of a machine model/simple program in a programming language like C,
- $\vec{n}$: binary integers for the size of the inputs (in bits),
- $t$: a binary integer as a bound on the number of steps (if it is needed),
- $m$: a binary integer as a bound on the amount of memory (if it is needed),
and outputs a Boolean circuit $C$ that computes $M$ on inputs of size $\vec{n}$?
Or a compiler from simple programs in a language like C to Turing machines, plus an implementation of Cook-Levin for Turing machines.
By a simple program in C I mean a program that does not use libraries (using standard computational libraries can be fine), i.e. computes a function of its inputs and does not interact with the environment (file system, network, other processes, ...).
Motivation:
Sometimes we want to turn instances of other NP problems into SAT instances so we can run SAT solvers on them. In place of writing a reduction program for each NP problem we can use an implementation of Cook-Levin plus the code of a verifier for the NP problem.