8
$\begingroup$

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.

| cite | improve this question | |
$\endgroup$
  • 7
    $\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$ – Marzio De Biasi Apr 20 '14 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 '14 at 9:19
  • $\begingroup$ sorry, no; the above programs use CNF format as intermediate files $\endgroup$ – Marzio De Biasi Apr 22 '14 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 '14 at 22:54
  • 3
    $\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$ – Artem Kaznatcheev♦ Apr 23 '14 at 15:56

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.