# Cook–Levin theorem or Cook’s theorem

In computational complexity theory, the Cook–Levin theorem, also known as Cook’s theorem, states that the Boolean satisfiability problem is NP-complete. That is, it is in NP, and any problem in NP can be reduced in polynomial time by a deterministic Turing machine to the Boolean satisfiability problem.

*Stephen Arthur Cook and L.A. Levin in 1973 independently proved that the satisfiability problem(SAT) is NP-complete. Stephen Cook, in 1971, published an important paper titled ‘The complexity of Theorem Proving Procedures’, in which he outlined the way of obtaining the proof of an NP-complete problem by reducing it to SAT. He proved Circuit-SAT and 3CNF-SAT problems are as hard as SAT. Similarly, Leonid Levin independently worked on this problem in the then Soviet Union. The proof that SAT is NP-complete was obtained due to the efforts of these two scientists. Later, Karp reduced 21 optimization problems, such as Hamiltonian tour, vertex cover*,

*and clique, to the*

**SAT**and proved that those problems are NP-complete.Attention reader! Don’t stop learning now. Get hold of all the important DSA concepts with the **DSA Self Paced Course** at a student-friendly price and become industry ready. To complete your preparation from learning a language to DS Algo and many more, please refer **Complete Interview Preparation Course****.**

In case you wish to attend **live classes **with experts, please refer **DSA Live Classes for Working Professionals **and **Competitive Programming Live for Students**.

* Hence, *an

__SAT____is a significant problem and can be stated as follows:__Given a boolean expression **F** having **n **variables **x _{1},x_{2},….,x_{n},** and Boolean operators, is it possible to have an assignment for variables true or false such that binary expression

**F**is true?

This problem is also known as the **formula – SAT**. An **SAT(formula-SAT or simply SAT)** takes a Boolean expression F and checks whether the given expression(or formula) is satisfiable. A Boolean expression is said to be satisfactory for some valid assignments of variables if the evaluation comes to be true. Prior to discussing the details of SAT, let us now discuss some important terminologies of a Boolean expression.

A variable, say__Boolean variable:__**x**, that can have only two values, true or false, is called a boolean variableA literal can be a logical variable, say__Literal:__**x**, or the negation of it, that is**x**or**x̄**;**x**is called a positive literal, and**x̄**is called the negative literalA sequence of variables__Clause:__**(x**that can be separated by a logical_{1},x_{2},….,x_{n})**OR**operator is called a clause. For example,**(x**is a clause of three literals._{1}V x_{2}V x_{3})One can combine all the preceding clauses using a Boolean operator to form an expression.__Expressions:__An expression is in CNF form(conjunctive normal form) if the set of clauses are separated by an__CNF form:__**AND (^),**operator, while the literals are connected by an**OR (v)**operator. The following is an example of an expression in the CNF form:**f = (x**_{1}V x̄_{2}V x_{3)}∧ (x_{1}V x̄_{3}V x_{2})

An expression is said to be in 3-CNF if it is in the conjunctive normal form, and every clause has exact three literals.__3 – CNF:__

Thus, an **SAT** is one of the toughest problems, as there is no known algorithm other than the brute force approach. A brute force algorithm would be an exponential-time algorithm, as **2 ^{n}**

^{ }possible assignments need to be tried to check whether the given Boolean expression is true or not. Stephen Cook and Leonid Levin proved that the

**SAT**is NP-complete.

Cook demonstrated the reduction of other hard problems to SATs. Karp provided proof of 21 important problems, Such as Hamiltonian tour, vertex cover, and clique, by reducing it to SAT using Karp reduction.

Let us briefly introduce the three types of SATs. They are as follows:

A circuit-SAT can be stated as follows: given a Boolean circuit, which is a collection of gates such as__Circuit- SAT:__**AND**,**OR**, and**NOT**, and**n**inputs, is there any input assignments of Boolean variables so that the output of the given circuit is true? Again, the difficulty with these problems is that for**n**inputs to the circuit.**2**^{n}^{ }possible outputs should be checked. Therefore, this brute force algorithm is an exponential algorithm and hence this is a hard problem.This problem is a restricted problem of__CNF-SAT:__**SAT**, where the expression should be in a conjunctive normal form. An expression is said to be in a conjunction form if all the clauses are connected by the Boolean**AND**operator. Like in case of a**SAT**, this is about assigning truth values to n variables such that the output of the expression is true__.__This problem is another variant where the additional restriction is that the expression is in a conjunctive normal form and that every clause should contain exactly three literals. This problem is also about assigning__3-CNF-SAT(3-SAT):__**n**assignments of truth values to**n**variables of the Boolean expression such that the output of the expression is true. In simple words, given an expression in 3-CNF, a 3-SAT problem is to check whether the given expression is satisfiable.

*These problems can be used to prove the NP-completeness of some important problems.*