Misplaced Pages

#337662

96-518: SAT is the first problem that was proven to be NP-complete —this is the Cook–Levin theorem . This means that all problems in the complexity class NP , which includes a wide range of natural decision and optimization problems, are at most as difficult to solve as SAT. There is no known algorithm that efficiently solves each SAT problem, and it is generally believed that no such algorithm exists, but this belief has not been proven mathematically, and resolving

192-425: A in A ; rings with this property are called Boolean rings . Conversely, if a Boolean ring A is given, we can turn it into a Boolean algebra by defining x ∨ y  := x + y + ( x · y ) and x ∧ y  := x · y . Since these two constructions are inverses of each other, we can say that every Boolean ring arises from a Boolean algebra, and vice versa. Furthermore, a map f  : A → B

288-577: A decision problem as a formal language in some fixed encoding, the set NPC of all NP-complete problems is not closed under: It is not known whether NPC is closed under complementation , since NPC= co-NPC if and only if NP= co-NP , and since NP=co-NP is an open question . Boolean algebra (structure) In abstract algebra , a Boolean algebra or Boolean lattice is a complemented distributive lattice . This type of algebraic structure captures essential properties of both set operations and logic operations. A Boolean algebra can be seen as

384-489: A graph isomorphism exists between two graphs. Two graphs are isomorphic if one can be transformed into the other simply by renaming vertices . Consider these two problems: The Subgraph Isomorphism problem is NP-complete. The graph isomorphism problem is suspected to be neither in P nor NP-complete, though it is in NP. This is an example of a problem that is thought to be hard , but is not thought to be NP-complete. This class

480-459: A ∉ I and − a ∉ I , then I ∪ { a } or I ∪ {− a } is contained in another proper ideal J . Hence, such an I is not maximal, and therefore the notions of prime ideal and maximal ideal are equivalent in Boolean algebras. Moreover, these notions coincide with ring theoretic ones of prime ideal and maximal ideal in the Boolean ring A . The dual of an ideal

576-407: A ∧ ¬ b ) ∨ ( b ∧ ¬ a ) = ( a ∨ b ) ∧ ¬( a ∧ b ) (this operation is called symmetric difference in the case of sets and XOR in the case of logic) and a · b  := a ∧ b . The zero element of this ring coincides with the 0 of the Boolean algebra; the multiplicative identity element of the ring is the 1 of the Boolean algebra. This ring has the property that a · a = a for all

672-464: A , b ) is a generalized clause, and R (¬ x , a , b ) ∧ R ( b , y , c ) ∧ R ( c , d ,¬ z ) is a generalized conjunctive normal form. This formula is used below , with R being the ternary operator that is TRUE just when exactly one of its arguments is. Using the laws of Boolean algebra , every propositional logic formula can be transformed into an equivalent conjunctive normal form, which may, however, be exponentially longer. For example, transforming

768-486: A , b ) ∧ R ( b , y , c ) ∧ R( c , d ,¬ z ), see picture (right). Another variant is the not-all-equal 3-satisfiability problem (also called NAE3SAT ). Given a conjunctive normal form with three literals per clause, the problem is to determine if an assignment to the variables exists such that in no clause all three literals have the same truth value. This problem is NP-complete, too, even if no negation symbols are admitted, by Schaefer's dichotomy theorem. A 3-SAT formula

864-643: A =TRUE or a =FALSE it evaluates to TRUE ∧ ¬TRUE (i.e., FALSE) or FALSE ∧ ¬FALSE (i.e., again FALSE), respectively. For some versions of the SAT problem, it is useful to define the notion of a generalized conjunctive normal form formula, viz. as a conjunction of arbitrarily many generalized clauses , the latter being of the form R ( l 1 ,..., l n ) for some Boolean function R and (ordinary) literals l i . Different sets of allowed Boolean functions lead to different problem versions. As an example, R (¬ x ,

960-512: A Boolean algebra can be extended to an ultrafilter is called the ultrafilter lemma and cannot be proven in Zermelo–Fraenkel set theory (ZF), if ZF is consistent . Within ZF, the ultrafilter lemma is strictly weaker than the axiom of choice . The ultrafilter lemma has many equivalent formulations: every Boolean algebra has an ultrafilter , every ideal in a Boolean algebra can be extended to

1056-403: A definition of a bounded lattice . It follows from the first five pairs of axioms that any complement is unique. The set of axioms is self-dual in the sense that if one exchanges ∨ with ∧ and 0 with 1 in an axiom, the result is again an axiom. Therefore, by applying this operation to a Boolean algebra (or Boolean lattice), one obtains another Boolean algebra with the same elements; it

SECTION 10

#1732780085338

1152-412: A general SAT problem to disjunctive normal form; to obtain an example, exchange "∧" and "∨" in the above exponential blow-up example for conjunctive normal forms. A variant of the 3-satisfiability problem is the one-in-three 3-SAT (also known variously as 1-in-3-SAT and exactly-1 3-SAT ). Given a conjunctive normal form with three literals per clause, the problem is to determine whether there exists

1248-465: A generalization of a power set algebra or a field of sets , or its elements can be viewed as generalized truth values . It is also a special case of a De Morgan algebra and a Kleene algebra (with involution) . Every Boolean algebra gives rise to a Boolean ring , and vice versa, with ring multiplication corresponding to conjunction or meet ∧, and ring addition to exclusive disjunction or symmetric difference (not disjunction ∨). However,

1344-411: A homomorphism g  : B → A such that the composition g ∘ f  : A → A is the identity function on A , and the composition f ∘ g  : B → B is the identity function on B . A homomorphism of Boolean algebras is an isomorphism if and only if it is bijective . Every Boolean algebra ( A , ∧, ∨) gives rise to a ring ( A , +, ·) by defining a + b  := (

1440-474: A more substantial book, The Laws of Thought , published in 1854. Boole's formulation differs from that described above in some important respects. For example, conjunction and disjunction in Boole were not a dual pair of operations. Boolean algebra emerged in the 1860s, in papers written by William Jevons and Charles Sanders Peirce . The first systematic presentation of Boolean algebra and distributive lattices

1536-402: A nondeterministic Turing machine to perform the whole search. " Complete " refers to the property of being able to simulate everything in the same complexity class . More precisely, each input to the problem should be associated with a set of solutions of polynomial length, the validity of each of which can be tested quickly (in polynomial time ), such that the output for any input is "yes" if

1632-482: A one-in-three 3-SAT formula are positive, the satisfiability problem is called one-in-three positive 3-SAT . One-in-three 3-SAT, together with its positive case, is listed as NP-complete problem "LO4" in the standard reference Computers and Intractability: A Guide to the Theory of NP-Completeness by Michael R. Garey and David S. Johnson . One-in-three 3-SAT was proved to be NP-complete by Thomas Jerome Schaefer as

1728-428: A polynomial time algorithm, all problems in NP do. The set of NP-complete problems is often denoted by NP-C or NPC . Although a solution to an NP-complete problem can be verified "quickly", there is no known way to find a solution quickly. That is, the time required to solve the problem using any currently known algorithm increases rapidly as the size of the problem grows. As a consequence, determining whether it

1824-543: A prime ideal , etc. It can be shown that every finite Boolean algebra is isomorphic to the Boolean algebra of all subsets of a finite set. Therefore, the number of elements of every finite Boolean algebra is a power of two . Stone's celebrated representation theorem for Boolean algebras states that every Boolean algebra A is isomorphic to the Boolean algebra of all clopen sets in some ( compact totally disconnected Hausdorff ) topological space. The first axiomatization of Boolean lattices/algebras in general

1920-414: A problem is NP-complete when: The name "NP-complete" is short for "nondeterministic polynomial-time complete". In this name, "nondeterministic" refers to nondeterministic Turing machines , a way of mathematically formalizing the idea of a brute-force search algorithm. Polynomial time refers to an amount of time that is considered "quick" for a deterministic algorithm to check a single solution, or for

2016-403: A satisfying assignment. Since k does not depend on the formula length, the extra clauses lead to a constant increase in length. For the same reason, it does not matter whether duplicate literals are allowed in clauses, as in ¬ x ∨ ¬ y ∨ ¬ y . Conjunctive normal form (in particular with 3 literals per clause) is often considered the canonical representation for SAT formulas. As shown above,

SECTION 20

#1732780085338

2112-562: A set of other variables. Indeed, one such clause ¬ x 1 ∨ ... ∨ ¬ x n ∨ y can be rewritten as x 1 ∧ ... ∧ x n → y ; that is, if x 1 ,..., x n are all TRUE, then y must be TRUE as well. A generalization of the class of Horn formulas is that of renameable-Horn formulae, which is the set of formulas that can be placed in Horn form by replacing some variables with their respective negation. For example, ( x 1 ∨ ¬ x 2 ) ∧ (¬ x 1 ∨ x 2 ∨ x 3 ) ∧ ¬ x 1

2208-650: A solution. Different SAT solvers will find different instances easy or hard, and some excel at proving unsatisfiability, and others at finding solutions. Recent attempts have been made to learn an instance's satisfiability using deep learning techniques. SAT solvers are developed and compared in SAT-solving contests. Modern SAT solvers are also having significant impact on the fields of software verification, constraint solving in artificial intelligence, and operations research, among others. (by date of publication) NP-complete In computational complexity theory ,

2304-465: A special case of Schaefer's dichotomy theorem , which asserts that any problem generalizing Boolean satisfiability in a certain way is either in the class P or is NP-complete. Schaefer gives a construction allowing an easy polynomial-time reduction from 3-SAT to one-in-three 3-SAT. Let "( x or y or z )" be a clause in a 3CNF formula. Add six fresh Boolean variables a , b , c , d , e , and f , to be used to simulate this clause and no other. Then

2400-400: A subroutine that solves Y {\displaystyle \scriptstyle Y} in polynomial time, one could write a program that calls this subroutine and solves X {\displaystyle \scriptstyle X} in polynomial time. This contrasts with many-one reducibility, which has the restriction that the program can only call the subroutine once, and the return value of

2496-435: A truth assignment to the variables so that each clause has exactly one TRUE literal (and thus exactly two FALSE literals). In contrast, ordinary 3-SAT requires that every clause has at least one TRUE literal. Formally, a one-in-three 3-SAT problem is given as a generalized conjunctive normal form with all generalized clauses using a ternary operator R that is TRUE just if exactly one of its arguments is. When all literals of

2592-500: Is satisfiability modulo theories ( SMT ) that can enrich CNF formulas with linear constraints, arrays, all-different constraints, uninterpreted functions , etc. Such extensions typically remain NP-complete, but very efficient solvers are now available that can handle many such kinds of constraints. The satisfiability problem becomes more difficult if both "for all" ( ∀ ) and "there exists" ( ∃ ) quantifiers are allowed to bind

2688-436: Is Linear SAT ( LSAT ) if each clause (viewed as a set of literals) intersects at most one other clause, and, moreover, if two clauses intersect, then they have exactly one literal in common. An LSAT formula can be depicted as a set of disjoint semi-closed intervals on a line. Deciding whether an LSAT formula is satisfiable is NP-complete. SAT is easier if the number of literals in a clause is limited to at most 2, in which case

2784-401: Is NP-complete if: C {\displaystyle \scriptstyle C} can be shown to be in NP by demonstrating that a candidate solution to C {\displaystyle \scriptstyle C} can be verified in polynomial time. Note that a problem satisfying condition 2 is said to be NP-hard , whether or not it satisfies condition 1. A consequence of this definition

2880-482: Is NP-complete is first to prove that it is in NP, and then to reduce some known NP-complete problem to it. Therefore, it is useful to know a variety of NP-complete problems. The list below contains some well-known problems that are NP-complete when expressed as decision problems. To the right is a diagram of some of the problems and the reductions typically used to prove their NP-completeness. In this diagram, problems are reduced from bottom to top. Note that this diagram

2976-414: Is a cycle or is bipartite is very easy (in L ), but finding a maximum bipartite or a maximum cycle subgraph is NP-complete. A solution of the knapsack problem within any fixed percentage of the optimal solution can be computed in polynomial time, but finding the optimal solution is NP-complete. An interesting example is the graph isomorphism problem , the graph theory problem of determining whether

Boolean satisfiability problem - Misplaced Pages Continue

3072-425: Is a filter . A filter of the Boolean algebra A is a nonempty subset p such that for all x , y in p we have x ∧ y in p and for all a in A we have a ∨ x in p . The dual of a maximal (or prime ) ideal in a Boolean algebra is ultrafilter . Ultrafilters can alternatively be described as 2-valued morphisms from A to the two-element Boolean algebra. The statement every filter in

3168-428: Is a function f  : A → B such that for all a , b in A : It then follows that f (¬ a ) = ¬ f ( a ) for all a in A . The class of all Boolean algebras, together with this notion of morphism, forms a full subcategory of the category of lattices. An isomorphism between two Boolean algebras A and B is a homomorphism f  : A → B with an inverse homomorphism, that is,

3264-417: Is a Boolean algebra. Crucial to McCune's proof was the computer program EQP he designed. For a simplification of McCune's proof, see Dahn (1998). Further work has been done for reducing the number of axioms; see Minimal axioms for Boolean algebra . Removing the requirement of existence of a unit from the axioms of Boolean algebra yields "generalized Boolean algebras". Formally, a distributive lattice B

3360-421: Is a generalized Boolean lattice, if it has a smallest element 0 and for any elements a and b in B such that a ≤ b , there exists an element x such that a ∧ x = 0 and a ∨ x = b . Defining a \ b as the unique x such that ( a ∧ b ) ∨ x = a and ( a ∧ b ) ∧ x = 0 , we say that the structure ( B , ∧, ∨, \, 0) is a generalized Boolean algebra , while ( B , ∨, 0)

3456-498: Is a homomorphism of Boolean algebras if and only if it is a homomorphism of Boolean rings. The categories of Boolean rings and Boolean algebras are equivalent ; in fact the categories are isomorphic . Hsiang (1985) gave a rule-based algorithm to check whether two arbitrary expressions denote the same value in every Boolean ring. More generally, Boudet, Jouannaud , and Schmidt-Schauß (1989) gave an algorithm to solve equations between arbitrary Boolean-ring expressions. Employing

3552-511: Is a many-one reduction that can be computed with only a logarithmic amount of space. Since every computation that can be done in logarithmic space can also be done in polynomial time it follows that if there is a logarithmic-space many-one reduction then there is also a polynomial-time many-one reduction. This type of reduction is more refined than the more usual polynomial-time many-one reductions and it allows us to distinguish more classes such as P-complete . Whether under these types of reductions

3648-528: Is a solution of 3-SAT; see the picture. As a consequence, for each CNF formula, it is possible to solve the XOR-3-SAT problem defined by the formula, and based on the result infer either that the 3-SAT problem is solvable or that the 1-in-3-SAT problem is unsolvable. Provided that the complexity classes P and NP are not equal , neither 2-, nor Horn-, nor XOR-satisfiability is NP-complete, unlike SAT. The restrictions above (CNF, 2CNF, 3CNF, Horn, XOR-SAT) bound

3744-491: Is also considered to be an essential component in the electronic design automation toolbox. Major techniques used by modern SAT solvers include the Davis–Putnam–Logemann–Loveland algorithm (or DPLL), conflict-driven clause learning (CDCL), and stochastic local search algorithms such as WalkSAT . Almost all SAT solvers include time-outs, so they will terminate in reasonable time even if they cannot find

3840-461: Is at least one variable assignment that makes the formula true. A variety of variants deal with the number of such assignments: Other generalizations include satisfiability for first - and second-order logic , constraint satisfaction problems , 0-1 integer programming . While SAT is a decision problem , the search problem of finding a satisfying assignment reduces to SAT. That is, each algorithm which correctly answers whether an instance of SAT

3936-400: Is built from variables , operators AND ( conjunction , also denoted by ∧), OR ( disjunction , ∨), NOT ( negation , ¬), and parentheses. A formula is said to be satisfiable if it can be made TRUE by assigning appropriate logical values (i.e. TRUE, FALSE) to its variables. The Boolean satisfiability problem (SAT) is, given a formula, to check whether it is satisfiable. This decision problem

Boolean satisfiability problem - Misplaced Pages Continue

4032-543: Is called Horn-satisfiability , or HORN-SAT . It can be solved in polynomial time by a single step of the unit propagation algorithm, which produces the single minimal model of the set of Horn clauses (w.r.t. the set of literals assigned to TRUE). Horn-satisfiability is P-complete . It can be seen as P's version of the Boolean satisfiability problem. Also, deciding the truth of quantified Horn formulas can be done in polynomial time. Horn clauses are of interest because they are able to express implication of one variable from

4128-407: Is called NP-Intermediate problems and exists if and only if P≠NP. At present, all known algorithms for NP-complete problems require time that is superpolynomial in the input size. The vertex cover problem has O ( 1.2738 k + n k ) {\displaystyle O(1.2738^{k}+nk)} for some k > 0 {\displaystyle k>0} and it

4224-431: Is called prime if I ≠ A and if a ∧ b in I always implies a in I or b in I . Furthermore, for every a ∈ A we have that a ∧ − a = 0 ∈ I , and then if I is prime we have a ∈ I or − a ∈ I for every a ∈ A . An ideal I of A is called maximal if I ≠ A and if the only ideal properly containing I is A itself. For an ideal I , if

4320-487: Is called a Horn clause if it contains at most one positive literal. A formula is in conjunctive normal form (CNF) if it is a conjunction of clauses (or a single clause). For example, x 1 is a positive literal, ¬ x 2 is a negative literal, and x 1 ∨ ¬ x 2 is a clause. The formula ( x 1 ∨ ¬ x 2 ) ∧ (¬ x 1 ∨ x 2 ∨ x 3 ) ∧ ¬ x 1 is in conjunctive normal form; its first and third clauses are Horn clauses, but its second clause

4416-646: Is called its dual . A = { e ∈ R : e 2 = e  and  e x = x e  for all  x ∈ R } , {\displaystyle A=\left\{e\in R:e^{2}=e{\text{ and }}ex=xe\;{\text{ for all }}\;x\in R\right\},} becomes a Boolean algebra when its operations are defined by e ∨ f  := e + f − ef and e ∧ f  := ef . A homomorphism between two Boolean algebras A and B

4512-508: Is called the P versus NP problem . But if any NP-complete problem can be solved quickly, then every problem in NP can, because the definition of an NP-complete problem states that every problem in NP must be quickly reducible to every NP-complete problem (that is, it can be reduced in polynomial time). Because of this, it is often said that NP-complete problems are harder or more difficult than NP problems in general. A decision problem C {\displaystyle \scriptstyle C}

4608-440: Is known, however, that AC reductions define a strictly smaller class than polynomial-time reductions. According to Donald Knuth , the name "NP-complete" was popularized by Alfred Aho , John Hopcroft and Jeffrey Ullman in their celebrated textbook "The Design and Analysis of Computer Algorithms". He reports that they introduced the change in the galley proofs for the book (from "polynomially-complete"), in accordance with

4704-558: Is measured in number recursive calls made by a DPLL algorithm . They identified a phase transition region from almost-certainly-satisfiable to almost-certainly-unsatisfiable formulas at the clauses-to-variables ratio at about 4.26. 3-satisfiability can be generalized to k-satisfiability ( k-SAT , also k-CNF-SAT ), when formulas in CNF are considered with each clause containing up to k literals. However, since for any k ≥ 3, this problem can neither be easier than 3-SAT nor harder than SAT, and

4800-411: Is misleading as a description of the mathematical relationship between these problems, as there exists a polynomial-time reduction between any two NP-complete problems; but it indicates where demonstrating this polynomial-time reduction has been easiest. There is often only a small difference between a problem in P and an NP-complete problem. For example, the 3-satisfiability problem, a restriction of

4896-402: Is not a Horn formula, but can be renamed to the Horn formula ( x 1 ∨ ¬ x 2 ) ∧ (¬ x 1 ∨ x 2 ∨ ¬ y 3 ) ∧ ¬ x 1 by introducing y 3 as negation of x 3 . In contrast, no renaming of ( x 1 ∨ ¬ x 2 ∨ ¬ x 3 ) ∧ (¬ x 1 ∨ x 2 ∨ x 3 ) ∧ ¬ x 1 leads to a Horn formula. Checking the existence of such a replacement can be done in linear time; therefore,

SECTION 50

#1732780085338

4992-750: Is not obvious. The Cook–Levin theorem states that the Boolean satisfiability problem is NP-complete, thus establishing that such problems do exist. In 1972, Richard Karp proved that several other problems were also NP-complete (see Karp's 21 NP-complete problems ); thus, there is a class of NP-complete problems (besides the Boolean satisfiability problem). Since the original results, thousands of other problems have been shown to be NP-complete by reductions from other problems previously shown to be NP-complete; many of these problems are collected in Garey & Johnson (1979) . The easiest way to prove that some new problem

5088-416: Is not. The formula is satisfiable, by choosing x 1  = FALSE, x 2  = FALSE, and x 3 arbitrarily, since (FALSE ∨ ¬FALSE) ∧ (¬FALSE ∨ FALSE ∨ x 3 ) ∧ ¬FALSE evaluates to (FALSE ∨ TRUE) ∧ (TRUE ∨ FALSE ∨ x 3 ) ∧ TRUE, and in turn to TRUE ∧ TRUE ∧ TRUE (i.e. to TRUE). In contrast, the CNF formula a ∧ ¬ a , consisting of two clauses of one literal, is unsatisfiable, since for

5184-438: Is obtained, which is co-NP-complete . If both quantifiers are allowed, the problem is called the quantified Boolean formula problem ( QBF ), which can be shown to be PSPACE-complete . It is widely believed that PSPACE-complete problems are strictly harder than any problem in NP, although this has not yet been proved. Using highly parallel P systems , QBF-SAT problems can be solved in linear time. Ordinary SAT asks if there

5280-404: Is of central importance in many areas of computer science , including theoretical computer science , complexity theory , algorithmics , cryptography and artificial intelligence . A literal is either a variable (in which case it is called a positive literal ) or the negation of a variable (called a negative literal ). A clause is a disjunction of literals (or a single literal). A clause

5376-507: Is owed to the 1890 Vorlesungen of Ernst Schröder . The first extensive treatment of Boolean algebra in English is A. N. Whitehead 's 1898 Universal Algebra . Boolean algebra as an axiomatic algebraic structure in the modern axiomatic sense begins with a 1904 paper by Edward V. Huntington . Boolean algebra came of age as serious mathematics with the work of Marshall Stone in the 1930s, and with Garrett Birkhoff 's 1940 Lattice Theory . In

5472-524: Is possible to solve these problems quickly, called the P versus NP problem , is one of the fundamental unsolved problems in computer science today. While a method for computing the solutions to NP-complete problems quickly remains undiscovered, computer scientists and programmers still frequently encounter NP-complete problems. NP-complete problems are often addressed by using heuristic methods and approximation algorithms . NP-complete problems are in NP ,

5568-465: Is solvable can be used to find a satisfying assignment. First, the question is asked on the given formula Φ. If the answer is "no", the formula is unsatisfiable. Otherwise, the question is asked on the partly instantiated formula Φ { x 1 =TRUE} , that is, Φ with the first variable x 1 replaced by TRUE, and simplified accordingly. If the answer is "yes", then x 1 =TRUE, otherwise x 1 =FALSE. Values of other variables can be found subsequently in

5664-406: Is that if we had a polynomial time algorithm (on a UTM , or any other Turing-equivalent abstract machine ) for C {\displaystyle \scriptstyle C} , we could solve all problems in NP in polynomial time. The concept of NP-completeness was introduced in 1971 (see Cook–Levin theorem ), though the term NP-complete was introduced later. At the 1971 STOC conference, there

5760-546: Is that it preserves the number of accepting answers. For example, deciding whether a given graph has a 3-coloring is another problem in NP; if a graph has 17 valid 3-colorings, then the SAT formula produced by the Cook–Levin reduction will have 17 satisfying assignments. NP-completeness only refers to the run-time of the worst case instances. Many of the instances that occur in practical applications can be solved much more quickly. See §Algorithms for solving SAT below. Like

5856-479: Is the number of variables in the 3-SAT proposition, and succeeds with high probability to correctly decide 3-SAT. The exponential time hypothesis asserts that no algorithm can solve 3-SAT (or indeed k -SAT for any k > 2 ) in exp( o ( n )) time (that is, fundamentally faster than exponential in n ). Selman, Mitchell, and Levesque (1996) give empirical data on the difficulty of randomly generated 3-SAT formulas, depending on their size parameters. Difficulty

SECTION 60

#1732780085338

5952-409: Is unknown whether there are any faster algorithms. The following techniques can be applied to solve computational problems in general, and they often give rise to substantially faster algorithms: One example of a heuristic algorithm is a suboptimal O ( n log ⁡ n ) {\displaystyle O(n\log n)} greedy coloring algorithm used for graph coloring during

6048-426: The register allocation phase of some compilers, a technique called graph-coloring global register allocation . Each vertex is a variable, edges are drawn between variables which are being used at the same time, and colors indicate the register assigned to each variable. Because most RISC machines have a fairly large number of general-purpose registers, even a heuristic approach is effective for this application. In

6144-514: The 1960s, Paul Cohen , Dana Scott , and others found deep new results in mathematical logic and axiomatic set theory using offshoots of Boolean algebra, namely forcing and Boolean-valued models . A Boolean algebra is a set A , equipped with two binary operations ∧ (called "meet" or "and"), ∨ (called "join" or "or"), a unary operation ¬ (called "complement" or "not") and two elements 0 and 1 in A (called "bottom" and "top", or "least" and "greatest" element, also denoted by

6240-401: The Boolean satisfiability problem, remains NP-complete, whereas the slightly more restricted 2-satisfiability problem is in P (specifically, it is NL-complete ), but the slightly more general max. 2-sat. problem is again NP-complete. Determining whether a graph can be colored with 2 colors is in P, but with 3 colors is NP-complete, even when restricted to planar graphs . Determining if a graph

6336-404: The Boolean variables. An example of such an expression would be ∀ x ∀ y ∃ z ( x ∨ y ∨ z ) ∧ (¬ x ∨ ¬ y ∨ ¬ z ) ; it is valid, since for all values of x and y , an appropriate value of z can be found, viz. z =TRUE if both x and y are FALSE, and z =FALSE else. SAT itself (tacitly) uses only ∃ quantifiers. If only ∀ quantifiers are allowed instead, the so-called tautology problem

6432-444: The ability to automatically solve problem instances involving tens of thousands of variables and millions of constraints (i.e. clauses). Examples of such problems in electronic design automation (EDA) include formal equivalence checking , model checking , formal verification of pipelined microprocessors , automatic test pattern generation , routing of FPGAs , planning , and scheduling problems , and so on. A SAT-solving engine

6528-426: The box for an example. This recast is based on the kinship between Boolean algebras and Boolean rings , and the fact that arithmetic modulo two forms a finite field . Since a XOR b XOR c evaluates to TRUE if and only if exactly 1 or 3 members of { a , b , c } are TRUE, each solution of the 1-in-3-SAT problem for a given CNF formula is also a solution of the XOR-3-SAT problem, and in turn each solution of XOR-3-SAT

6624-615: The considered formulae to be conjunctions of subformulas; each restriction states a specific form for all subformulas: for example, only binary clauses can be subformulas in 2CNF. Schaefer's dichotomy theorem states that, for any restriction to Boolean functions that can be used to form these subformulas, the corresponding satisfiability problem is in P or NP-complete. The membership in P of the satisfiability of 2CNF, Horn, and XOR-SAT formulae are special cases of this theorem. The following table summarizes some common variants of SAT. An extension that has gained significant popularity since 2003

6720-527: The definition of NP-complete changes is still an open problem. All currently known NP-complete problems are NP-complete under log space reductions. All currently known NP-complete problems remain NP-complete even under much weaker reductions such as A C 0 {\displaystyle AC_{0}} reductions and N C 0 {\displaystyle NC_{0}} reductions. Some NP-Complete problems such as SAT are known to be complete even under polylogarithmic time projections. It

6816-403: The definition of NP-complete given above, the term reduction was used in the technical meaning of a polynomial-time many-one reduction . Another type of reduction is polynomial-time Turing reduction . A problem X {\displaystyle \scriptstyle X} is polynomial-time Turing-reducible to a problem Y {\displaystyle \scriptstyle Y} if, given

6912-466: The following elegant axiomatization for Boolean algebra. It requires just one binary operation + and a unary functional symbol n , to be read as 'complement', which satisfy the following laws: Herbert Robbins immediately asked: If the Huntington equation is replaced with its dual, to wit: do (1), (2), and (4) form a basis for Boolean algebra? Calling (1), (2), and (4) a Robbins algebra ,

7008-494: The formula R ( x , a , d ) ∧ R ( y , b , d ) ∧ R ( a , b , e ) ∧ R ( c , d , f ) ∧ R ( z , c ,FALSE) is satisfiable by some setting of the fresh variables if and only if at least one of x , y , or z is TRUE, see picture (left). Thus any 3-SAT instance with m clauses and n variables may be converted into an equisatisfiable one-in-three 3-SAT instance with 5 m clauses and n + 6 m variables. Another reduction involves only four fresh variables and three clauses: R (¬ x ,

7104-496: The formula ( x 1 ∧ y 1 ) ∨ ( x 2 ∧ y 2 ) ∨ ... ∨ ( x n ∧ y n ) into conjunctive normal form yields while the former is a disjunction of n conjunctions of 2 variables, the latter consists of 2 clauses of n variables. However, with use of the Tseytin transformation , we may find an equisatisfiable conjunctive normal form formula with length linear in the size of the original propositional logic formula. SAT

7200-805: The general SAT problem reduces to 3-SAT, the problem of determining satisfiability for formulas in this form. SAT is trivial if the formulas are restricted to those in disjunctive normal form , that is, they are a disjunction of conjunctions of literals. Such a formula is indeed satisfiable if and only if at least one of its conjunctions is satisfiable, and a conjunction is satisfiable if and only if it does not contain both x and NOT x for some variable x . This can be checked in linear time. Furthermore, if they are restricted to being in full disjunctive normal form , in which every variable appears exactly once in every conjunction, they can be checked in constant time (each conjunction represents one satisfying assignment). But it can take exponential time and space to convert

7296-445: The last three pairs of axioms above (identity, distributivity and complements), or from the absorption axiom, that The relation ≤ defined by a ≤ b if these equivalent conditions hold, is a partial order with least element 0 and greatest element 1. The meet a ∧ b and the join a ∨ b of two elements coincide with their infimum and supremum , respectively, with respect to ≤. The first four pairs of axioms constitute

7392-486: The latter two are NP-complete, so must be k-SAT. Some authors restrict k-SAT to CNF formulas with exactly k literals . This does not lead to a different complexity class either, as each clause l 1 ∨ ⋯ ∨ l j with j < k literals can be padded with fixed dummy variables to l 1 ∨ ⋯ ∨ l j ∨ d j +1 ∨ ⋯ ∨ d k . After padding all clauses, 2–1 extra clauses must be appended to ensure that only d 1 = ⋯ = d k = FALSE can lead to

7488-475: The other problem. An example of a problem where this method has been used is the clique problem : given a CNF formula consisting of c clauses, the corresponding graph consists of a vertex for each literal, and an edge between each two non-contradicting literals from different clauses; see the picture. The graph has a c -clique if and only if the formula is satisfiable. There is a simple randomized algorithm due to Schöning (1999) that runs in time (4/3) where n

7584-436: The other. This is known as "the question of whether P=NP". Nobody has yet been able to determine conclusively whether NP-complete problems are in fact solvable in polynomial time, making this one of the great unsolved problems of mathematics . The Clay Mathematics Institute is offering a US$ 1 million reward ( Millennium Prize ) to anyone who has a formal proof that P=NP or that P≠NP. The existence of NP-complete problems

7680-424: The problem is called 2-SAT . This problem can be solved in polynomial time, and in fact is complete for the complexity class NL . If additionally all OR operations in literals are changed to XOR operations, then the result is called exclusive-or 2-satisfiability , which is a problem complete for the complexity class SL = L . The problem of deciding the satisfiability of a given conjunction of Horn clauses

7776-555: The question of whether SAT has a polynomial-time algorithm is equivalent to the P versus NP problem , which is a famous open problem in the theory of computing. Nevertheless, as of 2007, heuristic SAT-algorithms are able to solve problem instances involving tens of thousands of variables and formulas consisting of millions of symbols, which is sufficient for many practical SAT problems from, e.g., artificial intelligence , circuit design , and automatic theorem proving . A propositional logic formula , also called Boolean expression ,

7872-485: The question then becomes: Is every Robbins algebra a Boolean algebra? This question (which came to be known as the Robbins conjecture ) remained open for decades, and became a favorite question of Alfred Tarski and his students. In 1996, William McCune at Argonne National Laboratory , building on earlier work by Larry Wos, Steve Winker, and Bob Veroff, answered Robbins's question in the affirmative: Every Robbins algebra

7968-479: The results of a poll he had conducted of the theoretical computer science community. Other suggestions made in the poll included " Herculean ", "formidable", Steiglitz 's "hard-boiled" in honor of Cook, and Shen Lin's acronym "PET", which stood for "probably exponential time", but depending on which way the P versus NP problem went, could stand for "provably exponential time" or "previously exponential time". The following misconceptions are frequent. Viewing

8064-433: The same way. In total, n +1 runs of the algorithm are required, where n is the number of distinct variables in Φ. This property is used in several theorems in complexity theory: Since the SAT problem is NP-complete, only algorithms with exponential worst-case complexity are known for it. In spite of this, efficient and scalable algorithms for SAT were developed during the 2000s and have contributed to dramatic advances in

8160-465: The satisfiability of such formulae is in P as it can be solved by first performing this replacement and then checking the satisfiability of the resulting Horn formula. Another special case is the class of problems where each clause contains XOR (i.e. exclusive or ) rather than (plain) OR operators. This is in P , since an XOR-SAT formula can also be viewed as a system of linear equations mod 2, and can be solved in cubic time by Gaussian elimination ; see

8256-511: The satisfiability problem for arbitrary formulas, determining the satisfiability of a formula in conjunctive normal form where each clause is limited to at most three literals is NP-complete also; this problem is called 3-SAT , 3CNFSAT , or 3-satisfiability . To reduce the unrestricted SAT problem to 3-SAT, transform each clause l 1 ∨ ⋯ ∨ l n to a conjunction of n - 2 clauses where x 2 , ⋯ ,  x n −2 are fresh variables not occurring elsewhere. Although

8352-429: The set of all decision problems whose solutions can be verified in polynomial time; NP may be equivalently defined as the set of decision problems that can be solved in polynomial time on a non-deterministic Turing machine . A problem p in NP is NP-complete if every other problem in NP can be transformed (or reduced) into p in polynomial time. It is not known whether every problem in NP can be quickly solved—this

8448-409: The similarity of Boolean rings and Boolean algebras, both algorithms have applications in automated theorem proving . An ideal of the Boolean algebra A is a nonempty subset I such that for all x , y in I we have x ∨ y in I and for all a in A we have a ∧ x in I . This notion of ideal coincides with the notion of ring ideal in the Boolean ring A . An ideal I of A

8544-458: The solution set is non-empty and "no" if it is empty. The complexity class of problems of this form is called NP , an abbreviation for "nondeterministic polynomial time". A problem is said to be NP-hard if everything in NP can be transformed in polynomial time into it even though it may not be in NP. A problem is NP-complete if it is both in NP and NP-hard. The NP-complete problems represent the hardest problems in NP. If some NP-complete problem has

8640-405: The subroutine must be the return value of the program. If one defines the analogue to NP-complete with Turing reductions instead of many-one reductions, the resulting set of problems won't be smaller than NP-complete; it is an open question whether it will be any larger. Another type of reduction that is also often used to define NP-completeness is the logarithmic-space many-one reduction which

8736-555: The symbols ⊥ and ⊤ , respectively), such that for all elements a , b and c of A , the following axioms hold: Note, however, that the absorption law and even the associativity law can be excluded from the set of axioms as they can be derived from the other axioms (see Proven properties ). A Boolean algebra with only one element is called a trivial Boolean algebra or a degenerate Boolean algebra . (In older works, some authors required 0 and 1 to be distinct elements in order to exclude this case.) It follows from

8832-543: The theory of Boolean rings has an inherent asymmetry between the two operators, while the axioms and theorems of Boolean algebra express the symmetry of the theory described by the duality principle . The term "Boolean algebra" honors George Boole (1815–1864), a self-educated English mathematician. He introduced the algebraic system initially in a small pamphlet, The Mathematical Analysis of Logic , published in 1847 in response to an ongoing public controversy between Augustus De Morgan and William Hamilton , and later as

8928-411: The two formulas are not logically equivalent , they are equisatisfiable . The formula resulting from transforming all clauses is at most 3 times as long as its original; that is, the length growth is polynomial. 3-SAT is one of Karp's 21 NP-complete problems , and it is used as a starting point for proving that other problems are also NP-hard . This is done by polynomial-time reduction from 3-SAT to

9024-422: Was a fierce debate between the computer scientists about whether NP-complete problems could be solved in polynomial time on a deterministic Turing machine . John Hopcroft brought everyone at the conference to a consensus that the question of whether NP-complete problems are solvable in polynomial time should be put off to be solved at some later date, since nobody had any formal proofs for their claims one way or

9120-516: Was given by the English philosopher and mathematician Alfred North Whitehead in 1898. It included the above axioms and additionally x ∨ 1 = 1 and x ∧ 0 = 0 . In 1904, the American mathematician Edward V. Huntington (1874–1952) gave probably the most parsimonious axiomatization based on ∧ , ∨ , ¬ , even proving the associativity laws (see box). He also proved that these axioms are independent of each other. In 1933, Huntington set out

9216-587: Was the first problem known to be NP-complete , as proved by Stephen Cook at the University of Toronto in 1971 and independently by Leonid Levin at the Russian Academy of Sciences in 1973. Until that time, the concept of an NP-complete problem did not even exist. The proof shows how every decision problem in the complexity class NP can be reduced to the SAT problem for CNF formulas, sometimes called CNFSAT . A useful property of Cook's reduction

#337662