请输入您要查询的百科知识：

　

词条 Boolean satisfiability problem
释义

  1. Basic definitions and terminology

  2. Complexity and restricted versions

     Unrestricted satisfiability (SAT)  3-satisfiability  Exactly-1 3-satisfiability  Not-all-equal 3-satisfiability  2-satisfiability  Horn-satisfiability  XOR-satisfiability  Schaefer's dichotomy theorem 

  3. Extensions of SAT

  4. Self-reducibility

  5. Algorithms for solving SAT

  6. See also

  7. Notes

  8. References

  9. External links

     SAT problem format  Online SAT solvers  Offline SAT solvers  SAT applications  Conferences  Publications  Benchmarks  Evaluation of SAT solvers 
{{Redirect|3SAT|the Central European television network|3sat}}

In computer science, the Boolean satisfiability problem (sometimes called propositional satisfiability problem and abbreviated SATISFIABILITY or 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,[1] which is sufficient for many practical SAT problems from, e.g., artificial intelligence, circuit design, and automatic theorem proving.

Basic definitions and terminology

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.

There are several special cases of the Boolean satisfiability problem in which the formulas are required to have a particular structure. A literal is either a variable, called positive literal, or the negation of a variable, called negative literal.

A clause is a disjunction of literals (or a single literal). A clause 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, {{math|size=100%|x1}} is a positive literal, {{math|size=100%|¬x2}} is a negative literal, {{math|size=100%|x1 ∨ ¬x2}} is a clause, and {{math|size=100%|(x1 ∨ ¬x2) ∧ (¬x1 ∨ x2 ∨ x3) ∧ ¬x1}} is a formula in conjunctive normal form; its first and third clauses are Horn clauses, but its second clause is not. The formula is satisfiable, by choosing x1 = FALSE, x2 = FALSE, and x3 arbitrarily, since (FALSE ∨ ¬FALSE) ∧ (¬FALSE ∨ FALSE ∨ x3) ∧ ¬FALSE evaluates to (FALSE ∨ TRUE) ∧ (TRUE ∨ FALSE ∨ x3) ∧ 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 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 {{math|R(l1,...,ln)}} for some boolean operator R and (ordinary) literals {{mvar|li}}. Different sets of allowed boolean operators lead to different problem versions. As an example, R(¬x,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 the formula

(x1∧y1) ∨ (x2∧y2) ∨ ... ∨ (xn∧yn)

into conjunctive normal form yields

{{math|(x1 ∨ x2 ∨ … ∨ xn) ∧}}

{{math|(y1 ∨ x2 ∨ … ∨ xn) ∧}}

{{math|(x1 ∨ y2 ∨ … ∨ xn) ∧}}

{{math|(y1 ∨ y2 ∨ … ∨ xn) ∧ ... ∧}}

{{math|(x1 ∨ x2 ∨ … ∨ yn) ∧}}

{{math|(y1 ∨ x2 ∨ … ∨ yn) ∧}}

{{math|(x1 ∨ y2 ∨ … ∨ yn) ∧}}

{{math|(y1 ∨ y2 ∨ … ∨ yn)}};

while the former is a disjunction of n conjunctions of 2 variables, the latter consists of 2n clauses of n variables.

Complexity and restricted versions

Unrestricted satisfiability (SAT)

{{Main article|Cook–Levin theorem}}

SAT was the first known NP-complete problem, as proved by Stephen Cook at the University of Toronto in 1971[1] and independently by Leonid Levin at the National Academy of Sciences in 1973.[2] 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[3] 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.

SAT is trivial if the formulas are restricted to those in disjunctive normal form, that is, they are 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.

3-satisfiability

Like 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 {{math|l1 ∨ ⋯ ∨ ln}} to a conjunction of n − 2 clauses

{{math|(l1 ∨ l2 ∨ x2) ∧ }}

{{math|(¬x2 ∨ l3 ∨ x3) ∧ }}

{{math|(¬x3 ∨ l4 ∨ x4) ∧ ⋯ ∧ }}

{{math|(¬xn − 3 ∨ ln − 2 ∨ xn − 2) ∧ }}

{{math|(¬xn − 2 ∨ ln − 1 ∨ ln)}}

where {{math|x2, ⋯ , xn − 2}} are fresh variables not occurring elsewhere.

Although 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, i.e. the length growth is polynomial.[4]

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.[5] This is done by polynomial-time reduction from 3-SAT to 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[6] literals from different clauses, cf. picture. The graph has a c-clique if and only if the formula is satisfiable.{{refn|Aho, Hopcroft, Ullman[4] (1974); Thm.10.5}}

There is a simple randomized algorithm due to Schöning (1999) that runs in time (4/3)n where n is the number of variables in the 3-SAT proposition, and succeeds with high probability to correctly decide 3-SAT.[7]

The exponential time hypothesis asserts that no algorithm can solve 3-SAT (or indeed k-SAT for any k > 2) in {{math|exp(o(n))}} time (i.e., 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 is measured in number recursive calls made by a DPLL algorithm.[8]

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 the latter two are NP-complete, so must be k-SAT.

Some authors restrict k-SAT to CNF formulas with exactly k literals. This doesn't lead to a different complexity class either, as each clause {{math|l1 ∨ ⋯ ∨ lj}} with j<k literals can be padded with fixed dummy variables to

{{math|l1 ∨ ⋯ ∨ lj ∨ dj+1 ∨ ⋯ ∨ dk}}.

After padding all clauses, 2k-1 extra clauses[9] have to be appended to ensure that only {{math|1=d1=⋯=dk=FALSE}} can lead to a satisfying assignment. Since k doesn't 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 (like e.g. {{math|¬x ∨ ¬y ∨ ¬y}}), or not.

Exactly-1 3-satisfiability

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 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 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 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.[10]

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 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 5m clauses and n+6m variables.[11]

Another reduction involves only four fresh variables and three clauses: R(¬x,a,b) ∧ R(b,y,c) ∧ R(c,d,¬z), see picture (right).

Not-all-equal 3-satisfiability

{{main|Not-all-equal 3-satisfiability}}

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.[10]

2-satisfiability

{{Main article|2-satisfiability}}

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.

Horn-satisfiability

{{Main article|Horn-satisfiability}}

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.

[12]

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.

XOR-satisfiability

Another special case is the class of problems where each clause contains XOR (i.e. exclusive or) rather than (plain) OR operators.[13]

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;[14] 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.

Schaefer's dichotomy theorem

{{Main article|Schaefer's dichotomy theorem}}

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 operators 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.[10]

Extensions of SAT

An extension that has gained significant popularity since 2003 is satisfiability modulo theories (SMT) that can enrich CNF formulas with linear constraints, arrays, all-different constraints, uninterpreted functions,[15] 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 {{math|size=100%|∀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 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.[16]

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:

Other generalizations include satisfiability for first- and second-order logic, constraint satisfaction problems, 0-1 integer programming.

Self-reducibility

The SAT problem is self-reducible, that is, each algorithm which correctly answers if an instance of SAT 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 Φ{x1=TRUE}, i.e. Φ with the first variable x1 replaced by TRUE, and simplified accordingly. If the answer is "yes", then x1=TRUE, otherwise x1=FALSE. Values of other variables can be found subsequently in the same way. In total, n+1 runs of the algorithm are required, where n is the number of distinct variables in Φ.

This property of self-reducibility is used in several theorems in complexity theory:

NP ⊆ P/poly ⇒ PH = Σ2   (Karp–Lipton theorem)

NP ⊆ BPP ⇒ NP = RP

P = NP ⇒ FP = FNP

Algorithms for solving SAT

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 over the last decade{{When|date=July 2016}} 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).[18] Examples of such problems in electronic design automation (EDA) include formal equivalence checking, model checking, formal verification of pipelined microprocessors,[15] automatic test pattern generation, routing of FPGAs,[19] planning, and scheduling problems, and so on. A SAT-solving engine is now considered to be an essential component in the EDA toolbox.

There are two classes of high-performance algorithms for solving instances of SAT in practice: the conflict-driven clause learning algorithm, which can be viewed as a modern variant of the DPLL algorithm (well known implementations include Chaff[20] and GRASP[21]) and stochastic local search algorithms, such as WalkSAT.

A DPLL SAT solver employs a systematic backtracking search procedure to explore the (exponentially sized) space of variable assignments looking for satisfying assignments. The basic search procedure was proposed in two seminal papers in the early 1960s (see references below) and is now commonly referred to as the Davis–Putnam–Logemann–Loveland algorithm ("DPLL" or "DLL").[22][23] Theoretically, exponential lower bounds have been proved for the DPLL family of algorithms.

In contrast, randomized algorithms like the PPSZ algorithm by Paturi, Pudlak, Saks, and Zane set variables in a random order according to some heuristics, for example bounded-width resolution. If the heuristic can't find the correct setting, the variable is assigned randomly. The PPSZ algorithm has a runtime of for 3-SAT with a single satisfying assignment. Currently this is the best-known runtime for this problem. In the setting with many satisfying assignments the randomized algorithm by Schöning has a better bound.[7][24]

Modern SAT solvers (developed in the last ten years{{When|date=July 2016}}) come in two flavors: "conflict-driven" and "look-ahead".{{clarify|reason=3 paragraphs before here, 'two classes', viz. 'conflict-driven clause learning DPLL' and 'stochastic local search' were named. Please indicate if the latter essentially means the same as 'look-ahead' here.|date=September 2013}} Conflict-driven solvers augment the basic DPLL search algorithm with efficient conflict analysis, clause learning, non-chronological backtracking (a.k.a. backjumping), as well as "two-watched-literals" unit propagation, adaptive branching, and random restarts. These "extras" to the basic systematic search have been empirically shown to be essential for handling the large SAT instances that arise in electronic design automation (EDA).[25] Look-ahead solvers have especially strengthened reductions (going beyond unit-clause propagation) and the heuristics, and they are generally stronger than conflict-driven solvers on hard instances (while conflict-driven solvers can be much better on large instances which actually have an easy instance inside).

Modern SAT solvers are also having significant impact on the fields of software verification, constraint solving in artificial intelligence, and operations research, among others. Powerful solvers are readily available as free and open source software. In particular, the conflict-driven MiniSAT, which was relatively successful at the 2005 SAT competition, only has about 600 lines of code. A modern Parallel SAT solver is ManySAT. It can achieve super linear speed-ups on important classes of problems. An example for look-ahead solvers is march_dl, which won a prize at the 2007 SAT competition.

Certain types of large random satisfiable instances of SAT can be solved by survey propagation (SP). Particularly in hardware design and verification applications, satisfiability and other logical properties of a given propositional formula are sometimes decided based on a representation of the formula as a binary decision diagram (BDD).

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.

All of these behaviors can be seen in the SAT solving contests.[26]

See also

Notes

1. ^{{Cite journal | last1 = Cook | first1 = Stephen A. | authorlink1=Stephen Cook| title = The Complexity of Theorem-Proving Procedures | pages = 151–158 | year = 1971 | url=http://www.cs.toronto.edu/~sacook/homepage/1971.pdf| doi = 10.1145/800157.805047| journal = Proceedings of the 3rd Annual ACM Symposium on Theory of Computing}}
2. ^{{cite journal|last=Levin|first=Leonid|authorlink=Leonid Levin|title = Universal search problems (Russian: Универсальные задачи перебора, Universal'nye perebornye zadachi)|journal = Problems of Information Transmission (Russian: Проблемы передачи информа́ции, Problemy Peredachi Informatsii)|volume = 9|issue = 3|pages = 115–116|year = 1973}} (pdf) {{ru icon}}, translated into English by {{cite journal|last=Trakhtenbrot|first=B. A.|title = A survey of Russian approaches to perebor (brute-force searches) algorithms|journal = Annals of the History of Computing |volume = 6|issue = 4|pages = 384–400|year = 1984|doi=10.1109/MAHC.1984.10036}}
3. ^The SAT problem for arbitrary formulas is NP-complete, too, since it is easily shown to be in NP, and it cannot be easier than SAT for CNF formulas.
4. ^1 {{cite book|author1=Alfred V. Aho |author2=John E. Hopcroft |author3=Jeffrey D. Ullman | title=The Design and Analysis of Computer Algorithms| year=1974| publisher=Addison-Wesley}}; here: Thm.10.4
5. ^i.e. at least as hard as every other problem in NP. A decision problem is NP-complete if and only if it is in NP and is NP-hard.
6. ^i.e. such that one literal is not the negation of the other
7. ^1 {{cite book | last1 = Schöning | first1 = Uwe| chapter = A Probabilistic Algorithm for k-SAT and Constraint Satisfaction Problems | title = Proc. 40th Ann. Symp. Foundations of Computer Science| pages = 410–414 | date=Oct 1999 | url=http://homepages.cwi.nl/~rdewolf/schoning99.pdf| doi = 10.1109/SFFCS.1999.814612}}
8. ^{{cite journal|author1=Bart Selman |author2=David Mitchell |author3=Hector Levesque | title=Generating Hard Satisfiability Problems| journal=Artificial Intelligence| year=1996| volume=81| pages=17–29| url=http://citeseerx.ist.psu.edu/viewdoc/download;jsessionid=3CBEAB7E11BF4B2283E9F383810060C1?doi=10.1.1.37.7362&rep=rep1&type=pdf| doi=10.1016/0004-3702(95)00045-3}}
9. ^viz. all maxterms that can be built with {{math|d1,⋯,dk}}, except {{math|d1∨⋯∨dk}}
10. ^1 2 {{Cite conference | last1 = Schaefer | first1 = Thomas J. | last2 = | first2 = | year = 1978 | title = The complexity of satisfiability problems | booktitle = Proceedings of the 10th Annual ACM Symposium on Theory of Computing | place = San Diego, California | journal = | volume = | issue = | pages = 216–226 | publisher = | jstor = | url = http://www.ccs.neu.edu/home/lieber/courses/csg260/f06/materials/papers/max-sat/p216-schaefer.pdf | accessdate = }}
11. ^(Schaefer, 1978), p.222, Lemma 3.5
12. ^{{Cite journal | last1 = Buning | first1 = H.K. | last2 = Karpinski| first2 = Marek| last3=Flogel|first3=A.|year = 1995 | title = Resolution for Quantified Boolean Formulas | place = | journal = Information and Computation | volume = 117 | issue = 1 | pages = 12–18 | publisher = Elsevier | jstor = | doi= 10.1006/inco.1995.1025| accessdate = }}
13. ^Formally, generalized conjunctive normal forms with a ternary boolean operator R are employed, which is TRUE just if 1 or 3 of its arguments is. An input clause with more than 3 literals can be transformed into an equisatisfiable conjunction of clauses á 3 literals similar to above; i.e. XOR-SAT can be reduced to XOR-3-SAT.
14. ^{{citation|title=The Nature of Computation|first1=Cristopher|last1=Moore|author1-link=Cristopher Moore|first2=Stephan|last2=Mertens|publisher=Oxford University Press|year=2011|isbn=9780199233212|page=366|url=https://books.google.com/books?id=z4zMiZyAE1kC&pg=PA366}}.
15. ^1 R. E. Bryant, S. M. German, and M. N. Velev, Microprocessor Verification Using Efficient Decision Procedures for a Logic of Equality with Uninterpreted Functions, in Analytic Tableaux and Related Methods, pp. 1–13, 1999.
16. ^{{Cite journal | last1 = Alhazov | first1 = Artiom | last2 = Martín-Vide | first2 = Carlos | last3 = Pan | first3 = Linqiang | title = Solving a PSPACE-Complete Problem by Recognizing P Systems with Restricted Active Membranes | url = http://dl.acm.org/citation.cfm?id=2371013 | journal = Fundamenta Informaticae | volume = 58 | pages = 67–77 | year = 2003 }}
17. ^{{Cite journal | last1 = Valiant | first1 = L. | last2 = Vazirani | first2 = V.| doi = 10.1016/0304-3975(86)90135-0 | title = NP is as easy as detecting unique solutions | url = http://www.cs.princeton.edu/courses/archive/fall05/cos528/handouts/NP_is_as.pdf| journal = Theoretical Computer Science | volume = 47 | pages = 85–93 | year = 1986 | pmid = | pmc = }}
18. ^1 {{citation|title=Principles and Practice of Constraint Programming – CP 2007|series=Lecture Notes in Computer Science|volume=4741|year=2007|pages=544–558|contribution=Propagation = Lazy Clause Generation|first1=Olga|last1=Ohrimenko|first2=Peter J.|last2=Stuckey|first3=Michael|last3=Codish|doi=10.1007/978-3-540-74970-7_39|quote=modern SAT solvers can often handle problems with millions of constraints and hundreds of thousands of variables|citeseerx=10.1.1.70.5471}}.
19. ^{{Cite journal | last1 = Gi-Joon Nam | last2 = Sakallah | first2 = K. A. | last3 = Rutenbar | first3 = R. A. | title = A new FPGA detailed routing approach via search-based Boolean satisfiability | journal = IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems | volume = 21 | issue = 6 | pages = 674 | year = 2002 | url = http://cs-rutenbar.web.engr.illinois.edu/wp-content/uploads/2012/10/rutenbar-sattranscad02.pdf| doi = 10.1109/TCAD.2002.1004311}}
20. ^{{Cite book | last1 = Moskewicz | first1 = M. W. | last2 = Madigan | first2 = C. F. | last3 = Zhao | first3 = Y. | last4 = Zhang | first4 = L. | last5 = Malik | first5 = S. | chapter = Chaff: Engineering an Efficient SAT Solver| title = Proceedings of the 38th conference on Design automation (DAC)| pages = 530 | year = 2001 | isbn = 1581132972 | chapter-url = http://www.princeton.edu/~chaff/publication/DAC2001v56.pdf| doi = 10.1145/378239.379017}}
21. ^{{Cite journal | last1 = Marques-Silva | first1 = J. P. | last2 = Sakallah | first2 = K. A. | title = GRASP: a search algorithm for propositional satisfiability | journal = IEEE Transactions on Computers | volume = 48 | issue = 5 | pages = 506 | year = 1999 | url = http://embedded.eecs.berkeley.edu/Alumni/wjiang/ee219b/grasp.pdf| doi = 10.1109/12.769433}}
22. ^{{Cite journal | last1 = Davis | first1 = M. | last2 = Putnam | first2 = H. | title = A Computing Procedure for Quantification Theory | journal = Journal of the ACM | volume = 7 | issue = 3 | pages = 201 | year = 1960 | doi = 10.1145/321033.321034}}
23. ^{{Cite journal | last1 = Davis | first1 = M. |authorlink1=Martin Davis| last2 = Logemann | first2 = G. | last3 = Loveland | first3 = D. | title = A machine program for theorem-proving | journal = Communications of the ACM| volume = 5 | issue = 7 | pages = 394–397 | year = 1962 | url = http://www.ensiie.fr/~blazy/ipr/article2.pdf| doi = 10.1145/368273.368557}}
24. ^"An improved exponential-time algorithm for k-SAT", Paturi, Pudlak, Saks, Zani
25. ^{{Cite journal | last1 = Vizel | first1 = Y. | last2 = Weissenbacher | first2 = G. | last3 = Malik | first3 = S. | journal = Proceedings of the IEEE | volume = 103 | issue = 11 | year = 2015 | doi = 10.1109/JPROC.2015.2455034|title=Boolean Satisfiability Solvers and Their Applications in Model Checking}}
26. ^{{cite web|url=http://www.satcompetition.org/ |title=The international SAT Competitions web page|accessdate=2007-11-15}}

References

{{Reflist|30em}}

References are ordered by date of publication:

{{refbegin|colwidth=30em}}{{refend}}

External links

{{commons category}}

SAT Game - try solving a Boolean satisfiability problem yourself

SAT problem format

A SAT problem is often described in the DIMACS-CNF format: an input file in which each line represents a single disjunction. For example, a file with the two lines

 1 -5 4 0 -1 5 3 4 0

represents the formula "(x1 ∨ ¬x5 ∨ x4) ∧ (¬x1 ∨ x5 ∨ x3 ∨ x4)".

Another common format for this formula is the 7-bit ASCII representation "(x1 | ~x5 | x4) & (~x1 | x5 | x3 | x4)".

Online SAT solvers

Offline SAT solvers

SAT applications

Conferences

Publications

Benchmarks

SAT solving in general:

Evaluation of SAT solvers

More information on SAT:


This article includes material from a column in the ACM SIGDA [https://web.archive.org/web/20070208034716/http://www.sigda.org/newsletter/index.html e-newsletter] by Prof. Karem Sakallah

Original text is available [https://web.archive.org/web/20070708233347/http://www.sigda.org/newsletter/2006/eNews_061201.html here]

{{Logic}}{{DEFAULTSORT:Boolean Satisfiability Problem}}

6 : Boolean algebra|Electronic design automation|Formal methods|Logic in computer science|NP-complete problems|Satisfiability problems

随便看

　

开放百科全书收录14589846条英语、德语、日语等多语种百科知识，基本涵盖了大多数领域的百科知识，是一部内容自由、开放的电子版国际百科全书。

　

Copyright © 2023 OENC.NET All Rights Reserved
京ICP备2021023879号 更新时间：2024/11/12 1:25:13