<p>Does anyone know if there is an implementation of Cook-Levin?<br />
A program that gets an input like the following:</p>
<ul>
<li><span class="math-container">$M$</span>: the code of a machine model/simple program in a programming language like C,</li>
<li><span class="math-container">$\vec{n}$</span>: binary integers for the size of the inputs (in bits),</li>
<li><span class="math-container">$t$</span>: a binary integer as a bound on the number of steps (if it is needed),</li>
<li><span class="math-container">$m$</span>: a binary integer as a bound on the amount of memory (if it is needed),</li>
</ul>
<p>and outputs a Boolean circuit <span class="math-container">$C$</span> that computes <span class="math-container">$M$</span> on inputs of size <span class="math-container">$\vec{n}$</span>?</p>
<p>Or a compiler from simple programs in a language like C to Turing machines,
plus an implementation of Cook-Levin for Turing machines.</p>
<p>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, ...).</p>
<hr />
<h3>Motivation:</h3>
<p>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.</p>

CC BY-SA 3.0
2014-04-20T21:48:09.563Z
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
CC BY-SA 3.0
2014-04-22T09:19:40.373Z
Thanks @Marzio. By any chance, do you know if there is any program that can translate (sharply) bounded arithmetic formulas to Boolean circuits?
Kaveh
CC BY-SA 3.0
2014-04-22T10:08:25.693Z
sorry, no; the above programs use CNF format as intermediate files
Marzio De Biasi
CC BY-SA 3.0
2014-04-22T20:36:44.963Z
What format do you want the output in? Presumably a standard *compiler* (which compiles C code to the "Turing machine" assembly code) isn't what you're looking for, or you wouldn't have asked the question...
Joshua Grochow
CC BY-SA 3.0
2014-04-22T22:54:26.193Z
@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
CC BY-SA 3.0
2014-04-23T15:12:19.003Z
@Philip White, it is not off-topic. As discussed before and you can see in the wiki of [tag:software] tag asking for software related TCS research are on-topic.
Kaveh
CC BY-SA 3.0
2014-04-23T15:56:49.790Z
@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
<cc.complexity-theory><software><cook-levin>
Are there any implementations of Cook-Levin?
Kaveh
# Are there any implementations of Cook-Levin?

(Asked by: username_0 on 2014-04-20)

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.

**Tags:** cc.complexity-theory, software, cook-levin

> **Comments:**
> **username_1**: 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.  
> **username_0**: Thanks @Marzio. By any chance, do you know if there is any program that can translate (sharply) bounded arithmetic formulas to Boolean circuits?  
> **username_1**: sorry, no; the above programs use CNF format as intermediate files  
> **username_2**: What format do you want the output in? Presumably a standard *compiler* (which compiles C code to the "Turing machine" assembly code) isn't what you're looking for, or you wouldn't have asked the question...  
> **username_0**: @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.)  
> **username_0**: @Philip White, it is not off-topic. As discussed before and you can see in the wiki of [tag:software] tag asking for software related TCS research are on-topic.  
> **username_3**: @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 username_0'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.  

---

## 0 answers

