Talk:Cook–Levin theorem

Different proof

My proof in this article differs from the one given by Garey and Johnson. My Boolean expression B contains the disjunction of the possible transitions for a tape position/computation step (thus requiring at least one transition), whereas the G&J proof contains the conjunction (thus requiring all transitions, which seems wrong). See the definition of group G6, page 43 of the 1997 edition. I think this is a trivial mistake on G&J's part as G&J make it clear what they mean in the table on page 42. But I would appreciate someone to check my working. Gdr 21:00, 2004 Jul 21 (UTC)

In December 2008 your proof was edited, and at present there is no disjunction over possible transitions for a given state-symbol pair. That means the formula states that all applicable transitions must be satisfied (instead of one of them). Hence the construction is correct only for deterministic machines, which of course does not cover NP :) Jochgem (talk) 10:30, 22 April 2011 (UTC) (added:) I just noted this is what Jjldj already noted on 17 February 2009 under Clause Conjunction Table below.

Wrong definition

Isn't the first sentence under "Definitions" in the Cook's Theorem page wrong? Shouldn't it read as follows: "A decision problem is in NP if a deterministic Turing machine can verify a proposed solution of the decision problem in polynomial time. Equivalently, a decision problem is in NP if a non-deterministic Turing machine can solve the decision problem in polynomial time." This is more consistent with the definitions on the "NP" page. Rodney Topor 04:59, 29 October 2006 (UTC)

CSAT

I believe that the actual Cook-Levin theorem, at least as taught at GU, MIT, and Columbia, and as written in the seminal algorithms textbook CLRS, is actually the CSAT problem, for which no entry on Wikipedia even exists. After CSAT was shown to be NP-Complete, they reduced SAT to CSAT, and then 3SAT to SAT. Perhaps I'm mistaken, but I think that this article is incorrect. I noticed this b/c I'm a student taking algorithms at MIT, and what they taught us contradicts this article. 18.224.0.172 (talk) 01:14, 17 November 2009 (UTC)

Currently, there is a page on Circuit-SAT (=CSAT). Note that the approach to show that an NP-complete problem exists in CLRS is not the Cook-Levin theorem. A difference is that the Cook-Levin theorem shows NP-hardness of SAT with respect to logspace reductions, while CLRS uses polynomial time reductions to show NP-hardness of CSAT. As a logspace reduction can be performed in polynomial time, the Cook-Levin theorem is a bit stronger than the result in CLRS. I think CLRS have chosen to use polynomial time reductions because it allows them to prove all results within the RAM model and avoids the introduction of Turing machines. This makes the presentation simpler when coming from an algorithmic perspective. ShearedLizard (talk) 10:10, 22 May 2018 (UTC)

Merge

I agree that the Proof that Boolean satisfiability problem is NP-complete page should be merged into the Cook's Theorem page. There already is a proof in the the Cook's Theorem page that is more concise, more precise, and more complete. The other proof ignores the polynomial-time requirement of the reduction. I would go further and recommend the "Proof" page be deleted as it is redundant. Rodney Topor 05:47, 29 October 2006 (UTC)

I was poking around on Leonid Levin's page and noticed there is also an article titled Cook-Levin Theorem, which I think should also be merged into here. Note the capital "T" - currently Cook-Levin theorem (small "t") is a redirect, but the capital T page is not. I haven't checked out all of the differences yet, but I will try and move some over if I have time. --Culix 08:39, 10 December 2006 (UTC)

Yay. The theorems are the exact same, and the correct name of the Article should be the Cook-Levin theorem, because even though Cook discovered it first, Levin independently discovered it on the USSR front, and I think some credit should be given to him and to the discoveries he made in that part of the world. Can anyone edit this to make them look nice together??? Charlesblack 16:26, 16 December 2006 (UTC)

Support as per above. Either This article and Proof that Boolean satisfiability problem is NP-complete should both be merged into Cook-Levin Theorem, or Cook's theorem and Cook-Levin theorem should both be merged into Proof that Boolean satisfiability problem is NP-complete. "Cook's Theorem" is an unacceptable title as it does not give the theorem's creators equal merit for their work. However, the proof on this page is certainly the more concise one and should form the bulk of the future article's structure. Allispaul 12:28, 5 March 2007 (UTC)

Support. I think we should merge everything from Cook's theorem and Proof that Boolean satisfiability problem is NP-complete into Cook-Levin theorem, to give proper credit, and keep the most concise proof as the main bulk of the article. Cook-Levin theorem will have to be changed from a redirect into an actual page, and this page will have to be changed to a redirect. Cook-Levin Theorem (capital 'T') will have to be merged into Cook-Levin theorem (small 't') as well (and then turned into a redirect). --Culix 20:46, 7 March 2007 (UTC)

Strong oppose Cook was the first, and the theorem is known by his name all over the world. `'Míkka>t 21:01, 27 November 2007 (UTC)

Merge complete

I moved this article to Cook–Levin theorem and turned the other two articles into redirects. I decided not to merge any content: Proof that Boolean satisfiability problem is NP-complete had essentially the same proof presented here but in a slightly less systematic way, while Cook-Levin Theorem had a less direct proof. If someone cares enough about these alternative presentations of the proof then they can add them as extra sections. Gdr 13:40, 8 May 2007 (UTC)

Thanks Gdr, it looks great. --Culix 15:08, 19 June 2007 (UTC)

I agree with Culix, Charlesblack, Allispaul, and Gdr. In modern literature, the name Cook-Levin Theorem is only slightly more common than Cook's Theorem: see http://scholar.google.com/scholar?as_epq=%22Cook%27s+Theorem%22&as_ylo=2000 http://scholar.google.com/scholar?as_epq=%22Cook-Levin+Theorem%22&as_ylo=2000 http://www.claymath.org/millennium/P_vs_NP Still, it is more accurate and neutral, so the move to Cook-Levin Theorem was right. --Svnsvn 16:51, 2 November 2007 (UTC)

I agree that the proper name of the theorem is Cook-Levin theorem. Cook and Levin had basically no way of knowing that the other was developing the same idea. Also, both developed it in slightly different ways (Cook asked whether a solution exists; Levin asked what the solution was). Both are interesting and noteworthy.

Levin published only two years after Cook, which at that moment in mathematics, was simultaneous. I have seen a few other theorems or ideas commonly named after two people who developed it in "parallel", but who published many years apart. For example, I have been working on an article about Szasz-Mirakyan operators where the gap between Szasz' and Mirakjan's paper was 9 years. Again, this is "simultaneous" for the time period.

One cannot use Google Scholar to accurately search for the proper name of something unless you also run the search in Russian. Levin was Russian and his paper was seen by Russians. His name will probably need to be the Russian one in the search, too.

« D Trebbien (talk) 16:52 2008 January 4 (UTC)

Rename was reverted

User:Mikkalai moved the page back to Cook's theorem with no discussion here. I've undone that for the moment. Let's go over the arguments again. Gdr 12:59, 30 November 2007 (UTC)

User:Mikkalai moved the page (again!) to Cook-Levin theorem with no discussion here. (He or she moved it to CookLevin theorem first, which had the side-effect that a non-administrator would have been unable to move it back, but I prefer to hope that that was a mistake rather than deliberate obfuscation.) WP:MOSDASH#Dashes says that the en-dash is to be preferred for linking names (cf. Michelson–Morley experiment, Knuth–Morris–Pratt algorithm etc). Again, if there's an argument, let's consider it. Gdr 15:08, 19 January 2008 (UTC)

Dtrebbien - the two statements are *exactly* equivalent!

Re the revert by User:Dtrebbien, it should be pointed out that "solvable by a nondeterministic Turing machine in polynomial time" is exactly equivalent to "verifiable by a deterministic Turing machine in polynomial time", and the proof is textbook material. In fact, as the article on NP (complexity) states: The two definitions of NP as the class of problems solvable by a nondeterministic Turing machine (TM) in polynomial time and the class of problems verifiable by a deterministic Turing machine in polynomial time are equivalent. The proof is described by many textbooks, for example Sipser's Introduction to the Theory of Computation, section 7.3.

It is really a matter of personal preference whether one goes with "verifiable in polynomial time by a deterministic Turing machine" or "solvable in polynomial time by a nondeterministic Turing machine". However, keep in mind that the current statement in the article reads: SAT is intuitively in NP because a nondeterministic Turing machine can, in polynomial time, guess an assignment of truth values to the variables, determine the value of the expression under that assignment, and accept this if the assignment makes the entire expression true.[vague]. Many of my students have initially equated "nondeterministic Turing machine" to "guess-and-check", which leads to trouble since a guess-and-check approach for a difficult but satisfiable SAT instance in N variables should take an expected time around half of 2^N, with worst case around 2^N. My recommendation here would be to go with the "verifiable in polynomial time" statement for purposes of effective pedagogy, because it is intuitively obvious even for beginners that calculating the value of a Boolean expression with N variables and M gates should take no more time than evaluating each gate's result in sequence and storing the result. -- Brhaspati\^talk/_contribs 23:19, 6 April 2008 (UTC)

Based on the above reasons, I've reverted the revert, but kept both the definitions in the article. -- Brhaspati\^talk/_contribs 23:27, 6 April 2008 (UTC)

Hi Brhaspati,

I didn't like the idea of a non-deterministic Turing machine as "guess-and-checker", either, which is why {{vague}} was there in the first place.

Thanks for providing a reference for a proof that the two classes are equivalent, as it has been something that was alluded to in several sources, but which never seemed to be stated as a defining characteristic.

« D. Trebbien (talk) 04:42 2008 April 7 (UTC)

CNF

First you use De Morgan's laws to get the formula into conjunctive normal form

This isn't really accurate, since simply reducing a formula to CNF may cause an exponential increase in the size of the formula. We have to use a more sophisticated algorithm which (among other things) introduces new variables.--Taejo|대조 13:21, 23 June 2008 (UTC)

You are right. That sentence must be removed, and we need to replace it. Does anyone have a quick reference? Since it's wrong it must be removed immediately, even if we don't find a replacement immediately. Vegasprof (talk) 10:12, 31 October 2008 (UTC)

Sipser solves this by modifying the proof to create a formula that is already in CNF. Unfortunately, I don't have a copy of Sipser at hand for a reference, but it's fairly easy to do. It necessitates a bit of a rewrite, though. --Taejo|대조 10:35, 31 October 2008 (UTC)

I don't have access to the reference works at the moment, but it is my field, so I'll see what suggestions I can make. Let me introduce (original) notation.

1. Let me denote the problem as written by SAT.
2. Let me denote DSAT is the satisfiability problem for the conjunction of disjunctions of boolean variables and their negations. (I think this is the one actually used in the original source, but I'm not sure.)
3. Let me denote kSAT as the satisfiability problem for the conjunction of clauses, each of which has at most k boolean variables.
4. Let me denote kDSAT as the satisfiability problem for the conjunction of clauses, each of which is the disjunctions of at most k bookean variables and their negations. 3DSAT is what we now call 3SAT in the article. (The duplication method noted toward the end makes it clear we can make this exactly k.)

Together with the obvious implications, kSAT can be reduced to kDSAT in 2^k linear time by a brute force reduction of each clause to conjunctive normal form, and kDSAT can be reduced to 3DSAT by the introduction of structure variables, as described in the text. If we remove the disjunctions from the Turing machine simulation reduction table, where they don't belong, we can easily see that we've reduce any NP problem to 6SAT (and, with a little more effort, 4DSAT), and we're done. Does this help? — Arthur Rubin (talk) 16:20, 31 October 2008 (UTC)

I just looked at Sipser, which is the text I'm using for my course. Just as Taejo said, he proves directly that 3SAT is NP-complete, rather than by reducing SAT to it. I guess there are two questions here. Should the Wikipedia page contain a proof that 3SAT is NP-complete, or just a hint as to how it's done (which is what it now contains, although it's the wrong hint)? If a proof, which proof? Personally, I like the proof by reduction of SAT to 3SAT better. But in any case, I think we should remove the incorrect hint immediately. Vegasprof (talk) 16:27, 31 October 2008 (UTC)

There's a subtle error in my "proof" in that the final satisfiability clause is a long disjunction, so the reduction is to (6+D)SAT, Nonetheless, it is possible to reduce SAT to 3SAT by "disassociating" (making all connectives binary connectives), and assigning a new boolean variable to each connective. But we still need a reference. — Arthur Rubin (talk) 16:51, 31 October 2008 (UTC)

There's an explicit reduction from SAT to 3SAT in Beigel and Floyd, The Language of Machines: An Introduction to Computability and Formal Languages, Computer Science Press 1994, pp. 634–636. But a few pages earlier it defines SAT as only referring to CNF formulae. —David Eppstein (talk) 18:35, 31 October 2008 (UTC)

Since no one else has acted, I will modify the sentence as little as possible, using Sipser, to make it correct. We can decide later whether we should include an explicit polynomial time reduction of SAT to 3SAT. Vegasprof (talk) 18:20, 1 November 2008 (UTC)

Strictly speaking, the following equivalence is false: (A ∨ B ∨ C ∨ D) ≡ (A ∨ B ∨ Z) ∧ (¬Z ∨ C ∨ D) since that means that the two formulae have the same truth value for every assignment of the 5 variables. What we need to say is that an assignment of the variables A, B, C, D satisfies the first expression if and only if that assignment can be extended to an assignment of A, B, C, D, Z which satisfies the second expression. Vegasprof (talk) 12:54, 3 November 2008 (UTC)

Since no one has objected, I will make that change. Vegasprof (talk) 17:32, 5 November 2008 (UTC)

Clause Conjunction Table

The row describing conjunction clauses needed for transitions (containing (H_ik ∧ Q_qk ∧ T_iσk) → (H_(i+d)(k+1) ∧ Q_q′(k+1) ∧ T_iσ′(k+1))) seems incomplete. Since we are using a non-deterministic Turing machine, we should have a separate clause for every (q, σ), each consisting of a disjunction of all expressions conforming to (q, σ, q′, σ′, d) ∈ δ.

That is, in a non-deterministic machine we may have multiple transitions which result in different actions (q′, σ′, d) corresponding to the same state/symbol pair (q, σ), and so must account for that possibility. If we don't account for this, we end up potentially requiring the machine to have multiple symbols in the same position on the tape at the same time (same problem for states and head position), which clearly violates the conditions enforced by prior clauses.

Does that sound correct? Any suggestions on how to modify the table concisely to reflect this? Perhaps I'm not thinking through it properly, but is it even correct to say that a non-deterministic Turing machine is only in one state at a time? Jjldj (talk) 04:16, 17 February 2009 (UTC)

The above-mentioned problem has been addressed with the addition of the disjunction to the formula. The proof still seems wrong to me, though:

• Nothing ensures that there's at least one symbol per cell. Maximum of one symbol per cell *is* ensured, though.
• Halting is not handled; halted machine can do anything.

The proof in Garey and Johnson does deal with these explicitly, but their presentation of the proof is sufficiently different that I'm unsure about how to fix this one. arcatan (talk) 17:46, 16 October 2014 (UTC)

The proof in Sipser's textbook (Thm.7.30, p.254-259) uses somewhat different notation. Translated to our article's notation, Sipser includes, for every 0≤i,k≤p(n), the formula T_i0k v ... v T_isk, where Σ={0,...,s}, for the first issue. For the second one, he changes "must finish in an accepting state" to "an accepting state must occur in some step", i.e. V_{f ∈ F} V_0≤k≤p(n) Q_fk. - Jochen Burghardt (talk) 22:40, 16 October 2014 (UTC)

I just implemented my above suggestions in the article; see line "At least one symbol per tape cell", and the last line. - Jochen Burghardt (talk) 17:55, 17 October 2014 (UTC)

Cook, Levin and Karp

There are three (not just two) different theorems about the "NP completeness" of SAT: Cook's version, Karp's version (which followed Cook) and Levin's version (which was independently found). Each of them uses different definitions, and therefore, they are not mathematically equivalent. Whether Cook's completeness notion and Karp's notion are equivalent is one of the major open problems in Complexity Theory. I cannot work on the article right now, but I thought it worthwhile to leave a note. AmirOnWiki (talk) 09:05, 5 October 2012 (UTC)

Known optimal algorithms?

"Additionally he found for each of these problems an algorithm that solves it in optimal time (in particular, these algorithms run in polynomial time if and only if P = NP)."

According to this statement the optimal algorithms have been found and by measuring their time complexity we can determine if P = NP. Surly something is wrong here. — Preceding unsigned comment added by Folket (talk • contribs) 14:44, 13 January 2015 (UTC)

The convergence of these algorithms running time to their asymptotic behavior is too slow to measure accurately, and anyway we need proofs not experiments. —David Eppstein (talk) 16:46, 13 January 2015 (UTC)

I'd like to see some of these algorithms. Maybe it's terribly naive, but I wonder why no sharp complexity bound could be proven for any of them up to now. However, I don't have access to a translation of Levin's paper; and e.g. Sipser's textbook doesn't mention such algorithms known to be optimal (unless I overlooked something, or these "algorithms" are just what we call reductions today). - Jochen Burghardt (talk) 19:48, 13 January 2015 (UTC)

Define a "searcher" to be a Turing machine with three tapes (input, witness, scratch) that halts if the witness tape ever holds a witness for the given NP-complete problem instance and does not halt otherwise. Then if the problem can be solved in polynomial time, there exists a searcher that solves it in polynomial time (for all positive instances, but fails to halt for negative instances). Additionally there exists a brute force searcher that ignores its input tape and just counts up in binary in the witness tape; this searcher solves all positive instances but will probably not take polynomial time. Then, to solve a given instance of length n, let f(n) be a sufficiently slowly growing function (log log n is probably good enough) and simulate, in parallel, the set of all possible searchers with at most f(n) states, including also the brute force searcher even if it has too many states. Keep running the simulation until one of the simulated searchers halts. Because of the inclusion of the brute force searcher, this algorithm will correctly halt on all yes instances and fail to halt on all no instances. If P≠NP, it will not take polynomial time (because nothing can). And if P=NP then there exists a polynomial time searcher that will be included in the parallel simulation for all large enough inputs and that will cause the whole algorithm to halt within polynomial time (because small instances don't count towards the asymptotic time bound and multiplying the time for the good searcher by the overhead for the parallel simulation of all the other searchers and for testing the witnesses at each step still gives a polynomial). Of course, this isn't a true polynomial time algorithm because it doesn't halt on the no-instances, and I haven't read Levin to find out whether and how he gets around this issue. —David Eppstein (talk) 20:25, 13 January 2015 (UTC)

Improved worst case number of clauses?

There is a paper here (https://www.cs.cmu.edu/~wklieber/papers/2007_efficient-cnf-encoding-for-selecting-1.pdf) that shows how to encode the "exactly one" constraint in O(n) clauses rather than O(n^2) clauses. The Cook–Levin reduction uses "exactly one" constraints multiple times. Does that mean the worst case is actually lower? Thanks

Complexity / Generalized versions

Could some expert please have a look at the 2nd paragraph in section Cook–Levin_theorem#Complexity, and provide some more context there? I guess, the paragraph describes some proof constructions similar to Cook's (maybe using QBFs and/or DQBFs to establish a theorem about PSPACE-completeness?), but I'm unable to comprehend the sentence. Nevertheless, the two given references (the 2nd one available open-source) seem to indicate that the paragraph deals with something important, imo. - Jochen Burghardt (talk) 18:08, 7 May 2023 (UTC)

One way of stating the Cook–Levin theorem is that SAT can be used to encode nondeterministic polynomial time Turing machine computations. Another is that there exists an NP-complete problem, SAT.

This paragraph is merely pointing to the similarity of this with other similar formulations of other complexity classes (both easier and harder). In particular, QBF (which looks a lot like SAT but adds quantifiers to the variables) can be used to encode polynomial space Turing machine computations, so there exists a PSPACE-complete problem, QBF. I'm pretty the part about DQBF is for corresponding results for nondeterministic logarithmic space complexity, NL (complexity), but its wording appears garbled. —David Eppstein (talk) 20:05, 7 May 2023 (UTC)

Missing Expressions

I'm a little confused on why the table does not contain some other expressions.

In order to account for the fact that at any time $k$ there needs to be exactly one symbol per tape cell we have two expressions $\neg T_{i,j,k}\lor \neg T_{i',j,k}$ and $\bigvee _{j\in \Sigma }T_{i,j,k}$ for at most and at least one symbol per cell respectively. Since we have $\neg Q_{q,k}\lor \neg Q_{q',k}$ and $\neg H_{i,k}\lor \neg H_{i',k}$ for at most one state and head position, since we need to have exactly one state and head position at time $k$ why aren't the expressions $\bigvee _{q\in Q}Q_{q,k}$ and $\bigvee _{-p(n)\leq i\leq p(n)}H_{i,k}$ included to denote at least one state and head at time $k$?

Furthermore, how come our expression for checking only one head position $\neg H_{i,k}\lor \neg H_{i',k}$ takes $O(n^{3})$? Aren't we just iterating through $-p(n)\leq i\leq p(n)$? CalMan2003 (talk) 01:34, 13 September 2023 (UTC)

I agree that $\bigvee _{q\in Q}Q_{q,k}$ and $\bigvee _{-p(n)\leq i\leq p(n)}H_{i,k}$ seem to be missing. Indeed, they are present in the source.  Done I added them to the table now.

As for the complexity, we need one disjunction for every possible combination of $i,i',k$, and there are $O(p(n)^{3})$ of them. - Jochen Burghardt (talk) 08:22, 13 September 2023 (UTC)