# Are there any implementations of Cook-Levin?

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.

• You can look at some (advanced) tools that translates CSP instances to SAT (e.g. stp, sugar, csp2sat4j, FznTini, Spec2SAT, Bee); encoding a problem using a Constraint Programming language is not as easy as writing a small verifier program in C, but it's surely easier than encoding directly the SAT instances (a few times I wrote an high-level program that converts a problem instance into a CSP intance and then use one of the above tools to get a CNF file). I think (but I'm not an expert) that the Cook-Levin approach would introduce too-much complexity and lead to unmanageable long formulas. – Marzio De Biasi Apr 20 '14 at 21:48
• Thanks @Marzio. By any chance, do you know if there is any program that can translate (sharply) bounded arithmetic formulas to Boolean circuits? – Kaveh Apr 22 '14 at 9:19
• sorry, no; the above programs use CNF format as intermediate files – Marzio De Biasi Apr 22 '14 at 10:08
• @Joshua, I want CNF formulas as the final output (or at least Boolean circuits). A compiler from C to any format of Turing machines (or any other machine model) is fine as long as there is also an implementation of Cook-Levin for that format. (I will probably write one if I see there is not a clean open-source implementation.) – Kaveh Apr 22 '14 at 22:54
• @PhilipWhite when you are unsure about an user's intentions with a question, a good way to orient yourself is to check their history of contributions. From looking at Kaveh's previous posts, it is relatively clear that he is not a crank and probably not asking the question in bad faith. As such, your rude comments are completely unjustified (and I will delete them) and I would urge you to be more constructive with your continued feedback. – Artem Kaznatcheev Apr 23 '14 at 15:56