Буле кеңістігінің қанағаттандырылу мәселесі

Problem of determining if a Boolean formula could be made true

In logic and computer science, the Boolean satisfiability problem (sometimes called propositional satisfiability problem and abbreviated SATISFIABILITY, SAT or B SAT) is the problem of determining if there exists an interpretation that satisfies a given Boolean formula. In other words, it asks whether the variables of a given Boolean formula can be consistently replaced by the values TRUE or FALSE in such a way that the formula evaluates to TRUE. If this is the case, the formula is called satisfiable. On the other hand, if no such assignment exists, the function expressed by the formula is FALSE for all possible variable assignments and the formula is unsatisfiable. For example, the formula "a AND NOT b" is satisfiable because one can find the values a = TRUE and b = FALSE, which make (a AND NOT b) = TRUE. In contrast, "a AND NOT a" is unsatisfiable. SAT is the first problem that was proven to be NP complete; see 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; yet this belief has not been proven mathematically, and resolving 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, and automatic theorem proving.

A propositional logic formula, also called Boolean expression, 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 is of central importance in many areas of computer science, including theoretical computer science, complexity theory, algorithmics, cryptography and artificial intelligence.

SAT was the first known NP complete problem, 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 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, 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.

Conjunctive normal form (in particular with 3 literals per clause) is often considered the canonical representation for SAT formulas. As shown above, 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 a general SAT problem to disjunctive normal form; for an example exchange "∧" and "∨" in the above exponential blow up example for conjunctive normal forms.

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.

SAT is easier if the number of literals in a clause is limited to at most 2, in which case 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, 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 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 a set of other variables. Indeed, one such clause ¬x1 ∨ ∨ ¬xn ∨ y can be rewritten as x1 ∧ ∧ xn → y, that is, if x1, ,xn are all TRUE, then y needs to be TRUE as well. A generalization of the class of Horn formulae is that of renameable Horn formulae, which is the set of formulae that can be placed in Horn form by replacing some variables with their respective negation. For example, (x1 ∨ ¬x2) ∧ (¬x1 ∨ x2 ∨ x3) ∧ ¬x1 is not a Horn formula, but can be renamed to the Horn formula (x1 ∨ ¬x2) ∧ (¬x1 ∨ x2 ∨ ¬y3) ∧ ¬x1 by introducing y3 as negation of x3. In contrast, no renaming of (x1 ∨ ¬x2 ∨ ¬x3) ∧ (¬x1 ∨ x2 ∨ x3) ∧ ¬x1 leads to a Horn formula. Checking the existence of such a replacement can be done in linear time; therefore, 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.

Solving an XOR SAT exampleby Gaussian elimination Given formula ("⊕" means XOR, the is optional) (a⊕c⊕d) ∧ (b⊕¬c⊕d) ∧ (a⊕b⊕¬d) ∧ (a⊕¬b⊕¬c) Equation system ("1" means TRUE, "0" means FALSE) Each clause leads to one equation. a ⊕ c ⊕ d = 1 b ⊕ ¬ c ⊕ d = 1 a ⊕ b ⊕ ¬ d = 1 a ⊕ ¬ b ⊕ ¬ c = 1 Normalized equation system using properties of Boolean rings (¬x=1⊕x, x⊕x=0) a ⊕ c ⊕ d = 1 b ⊕ c ⊕ d = 0 a ⊕ b ⊕ d = 0 a ⊕ b ⊕ c = 1 (If the is present, contradicts the last black one, so the system is unsolvable. Therefore, Gauss' algorithm is used only for the black equations.) Associated coefficient matrix   a b c d line   1 0 1 1 1 A 0 1 1 1 0 B 1 1 0 1 0 C 1 1 1 0 1 DTransforming to echelon form   a b c d operation   1 0 1 1 1 A 1 1 0 1 0 C 1 1 1 0 1 D 0 1 1 1 0 B (swapped)   1 0 1 1 1 A 0 1 1 0 1 E = C⊕A 0 1 0 1 0 F = D⊕A 0 1 1 1 0 B   1 0 1 1 1 A 0 1 1 0 1 E 0 0 1 1 1 G = F⊕E 0 0 0 1 1 H = B⊕E Transforming to diagonal form   a b c d operation   1 0 1 0 0 I = A⊕H 0 1 1 0 1 E 0 0 1 0 0 J = G⊕H 0 0 0 1 1 H   1 0 0 0 0 K = I⊕J 0 1 0 0 1 L = E⊕J 0 0 1 0 0 J 0 0 0 1 1 H Solution: If the is present: Unsolvable Else: a = 0 = FALSE b = 1 = TRUE c = 0 = FALSE d = 1 = TRUE As a consequence: R(a,c,d) ∧ R(b,¬c,d) ∧ R(a,b,¬d) ∧ R(a,¬b,¬c) is not 1 in 3 satisfiable, while (a ∨ c ∨ d) ∧ (b ∨ ¬c ∨ d) ∧ (a ∨ b ∨ ¬d) ∧ (a ∨ ¬b ∨ ¬c) is 3 satisfiable with a=c=FALSE and b=d=TRUE. 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 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 is a solution of 3 SAT, cf. 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 the considered formulae to be conjunctions of subformulae; each restriction states a specific form for all subformulae: for example, only binary clauses can be subformulae in 2CNF. Schaefer's dichotomy theorem states that, for any restriction to Boolean functions that can be used to form these subformulae, 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. 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 the Boolean variables. An example of such an expression would be size=100%; 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 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 is at least one variable assignment that makes the formula true. A variety of variants deal with the number of such assignments:
MAJ SAT asks if the majority of all assignments make the formula TRUE. It is known to be complete for PP, a probabilistic class. #SAT, the problem of counting how many variable assignments satisfy a formula, is a counting problem, not a decision problem, and is #P complete. UNIQUE SAT is the problem of determining whether a formula has exactly one assignment. It is complete for US, the complexity class describing problems solvable by a non deterministic polynomial time Turing machine that accepts when there is exactly one nondeterministic accepting path and rejects otherwise. UNAMBIGUOUS SAT is the name given to the satisfiability problem when the input is restricted to formulas having at most one satisfying assignment. The problem is also called USAT. A solving algorithm for UNAMBIGUOUS SAT is allowed to exhibit any behavior, including endless looping, on a formula having several satisfying assignments. Although this problem seems easier, Valiant and Vazirani have shown that if there is a practical (i. e. randomized polynomial time) algorithm to solve it, then all problems in NP can be solved just as easily. MAX SAT, the maximum satisfiability problem, is an FNP generalization of SAT. It asks for the maximum number of clauses which can be satisfied by any assignment. It has efficient approximation algorithms, but is NP hard to solve exactly. Worse still, it is APX complete, meaning there is no polynomial time approximation scheme (PTAS) for this problem unless P=NP. WMSAT is the problem of finding an assignment of minimum weight that satisfy a monotone Boolean formula (i. e. a formula without any negation). Weights of propositional variables are given in the input of the problem. The weight of an assignment is the sum of weights of true variables. That problem is NP complete (see Th. 1 of ). Other generalizations include satisfiability for first and second order logic, constraint satisfaction problems, 0 1 integer programming.

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 our 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, planning, and scheduling problems, and so on. A SAT solving engine 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 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.