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, ...).


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.

  • 8
    $\begingroup$ 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. $\endgroup$ Apr 20, 2014 at 21:48
  • $\begingroup$ Thanks @Marzio. By any chance, do you know if there is any program that can translate (sharply) bounded arithmetic formulas to Boolean circuits? $\endgroup$
    – Kaveh
    Apr 22, 2014 at 9:19
  • $\begingroup$ sorry, no; the above programs use CNF format as intermediate files $\endgroup$ Apr 22, 2014 at 10:08
  • 1
    $\begingroup$ @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.) $\endgroup$
    – Kaveh
    Apr 22, 2014 at 22:54
  • 4
    $\begingroup$ @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. $\endgroup$ Apr 23, 2014 at 15:56


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.