Satisfiability is the problem of determining if the variables of a given Boolean formula can be assigned in such a way as to make the formula evaluate to TRUE. Equally important is to determine whether no such assignments exist, which would imply that the function expressed by the formula is identically FALSE for all possible variable assignments. In this latter case, we would say that the function is unsatisfiable; otherwise it is satisfiable. To emphasize the binary nature of this problem, it is frequently referred to as Boolean or propositional satisfiability. The shorthand "SAT" is also commonly used to denote it, with the implicit understanding that the function and its variables are all binary-valued. 3sats logo 3sat is the name of a public, advertising-free, television network in Central Europe. ... For use in mathematics, see Boolean algebra (structure). ...

Basic definitions, terminology and applications

In complexity theory, the Boolean satisfiability problem (SAT) is a decision problem, whose instance is a Boolean expression written using only AND, OR, NOT, variables, and parentheses. The question is: given the expression, is there some assignment of TRUE and FALSE values to the variables that will make the entire expression true? A formula of propositional logic is said to be satisfiable if logical values can be assigned to its variables in a way that makes the formula true. The boolean satisfiability problem is NP-complete. The propositional satisfiability problem (PSAT), which decides whether a given propositional formula is satisfiable, is of central importance in various areas of computer science, including theoretical computer science, algorithmics, artificial intelligence, hardware design, electronic design automation, and verification. As a branch of the theory of computation in computer science, computational complexity theory investigates the problems related to the amounts of resources required for the execution of algorithms (e. ... In computability theory and computational complexity theory, a decision problem is a question in some formal system with a yes-or-no answer. ... Propositional logic or sentential logic is the logic of propositions, sentences, or clauses. ... In logic and mathematics, a logical value, also called a truth value, is a value indicating to what extent a proposition is true. ... In computer science and mathematics, a variable (pronounced ) (sometimes called an object or identifier in computer science) is a symbolic representation used to denote a quantity or expression. ... In complexity theory, the NP-complete problems are the most difficult problems in NP, in the sense that they are the ones most likely not to be in P. The reason is that if you could find a way to solve an NP-complete problem quickly, then you could use... Computer science, or computing science, is the study of the theoretical foundations of information and computation and their implementation and application in computer systems. ... Computer science (informally, CS or compsci) is, in its most general sense, the study of computation and information processing, both in hardware and in software. ... Flowcharts are often used to represent algorithms. ... AI redirects here. ... Hardware Design, or computer hardware design, is integral to how a computer operates. ... PCB Layout Program Electronic design automation (EDA) is the category of tools for designing and producing electronic systems ranging from printed circuit boards (PCBs) to integrated circuits. ... In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of a system with respect to a certain formal specification or property, using formal methods. ...

The problem can be significantly restricted while still remaining NP-complete. By applying De Morgan's laws, we can assume that NOT operators are only applied directly to variables, not expressions; we refer to either a variable or its negation as a literal. For example, both x₁ and not(x₂) are literals, the first a positive literal and the second a negative literal. If we OR together a group of literals, we get a clause, such as (x₁ or not(x₂)). Finally, let us consider formulae that are a conjunction (AND) of clauses - this is the conjunctive normal form (CNF). Determining whether a formula in this form is satisfiable is still NP-complete, even if each clause is limited to at most three literals. This last problem is called 3SAT, 3CNFSAT, or 3-satisfiability. In complexity theory, the NP-complete problems are the most difficult problems in NP, in the sense that they are the ones most likely not to be in P. The reason is that if you could find a way to solve an NP-complete problem quickly, then you could use... note that demorgans laws are also a big part in circut design. ... In boolean logic, a formula is in conjunctive normal form (CNF) if it is a conjunction of clauses, where a clause is a disjunction of literals. ...

On the other hand, if we restrict each clause to at most two literals, the resulting problem, 2SAT, is NL-complete. Alternately, if every clause must be a Horn clause, containing at most one positive literal, the resulting problem, Horn-satisfiability, is P-complete. 2-satisfiability (abbreviated as 2-SAT) is a special case of satisfiability if expressions are written in conjunctive normal form with 2 variables per clause (2-CNF). ... In computational complexity theory, NL-Complete is a complexity class which is complete for NL. It contains the most difficult or expressive problems in NL. If a method exists for solving any one of the NL-complete problems in logarithmic memory space, then NL=L. One important NL-complete problems... In logic, and in particular in propositional calculus, a Horn clause is a proposition of the general type (p and q and . ... In formal logic, Horn-satisfiability is the problem of deciding whether a given set of Horn clauses is satisfiable or not. ... In complexity theory, the complexity class P-complete is a set of decision problems and is useful in the analysis of which problems can be efficiently solved on parallel computers. ...

Cook's theorem proves that the Boolean satisfiability problem is NP-complete, and in fact, this was the first decision problem proved to be NP-complete. However, beyond this theoretical significance, efficient and scalable algorithms for SAT that were developed over the last decade have contributed to dramatic advances in our ability to automatically solve problem instances involving tens of thousands of variables and millions of constraints. Examples of such problems in Electronic Design Automation include combinational equivalence checking, model checking, formal verification of pipelined microprocessors, automatic test pattern generation, routing of FPGAs, and so on. In fact, a SAT-solving engine is now considered to be an essential component in the EDA toolbox and all EDA vendors provide such a capability (usually behind the scenes.) It has been suggested that Proof that Boolean satisfiability problem is NP-complete be merged into this article or section. ... In complexity theory, the NP-complete problems are the most difficult problems in NP, in the sense that they are the ones most likely not to be in P. The reason is that if you could find a way to solve an NP-complete problem quickly, then you could use... PCB Layout Program Electronic design automation (EDA) is the category of tools for designing and producing electronic systems ranging from printed circuit boards (PCBs) to integrated circuits. ... Formal equivalence checking process is a part of Electronic Design Automation, commonly used during the development of digital integrated circuits, to formally prove that two representations of a circuit design exhibit exactly the same behavior. ... Model checking is the process of checking whether a given model satisfies a given logical formula. ... In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal methods of mathematics. ... A microprocessor is a programmable digital electronic component that incorporates the functions of a central processing unit (CPU) on a single semiconducting integrated circuit (IC). ... // Introduction ATPG, or Automatic test pattern generation is an electronic design automation tool that attempts to find an input (or test) sequence that, when applied to a digital circuit, enables testers to distinguish between the correct circuit behavior and the faulty circuit behavior caused by a particular fault. ... This article is about routing (or routeing) in computer networks. ... A field-programmable gate array or FPGA is a gate array that can be reprogrammed after it is manufactured, rather than having its programming fixed during the manufacturing — a programmable logic device. ...

Complexity and restricted versions

NP-completeness

SAT was the first known NP-complete problem, as proved by Stephen Cook in 1971 (see Cook's theorem for the proof). Until that time, the concept of an NP-complete problem did not even exist. The problem remains NP-complete even if all expressions are written in conjunctive normal form with 3 variables per clause (3-CNF), yielding the 3SAT problem. This means the expression has the form: In complexity theory, the NP-complete problems are the most difficult problems in NP, in the sense that they are the ones most likely not to be in P. The reason is that if you could find a way to solve an NP-complete problem quickly, then you could use... Stephen A. Cook is a noted computer scientist. ... It has been suggested that Proof that Boolean satisfiability problem is NP-complete be merged into this article or section. ... In boolean logic, a formula is in conjunctive normal form (CNF) if it is a conjunction of clauses, where a clause is a disjunction of literals. ...

(x₁₁ OR x₁₂ OR x₁₃) AND

(x₂₁ OR x₂₂ OR x₂₃) AND

(x₃₁ OR x₃₂ OR x₃₃) AND ...

where each x is a variable or a negation of a variable, and each variable can appear multiple times in the expression.

A useful property of Cook's reduction is that it preserves the number of accepting answers. For example, if a graph has 17 valid 3-colorings, the SAT formula produced by the 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 runtime behavior below.

2-satisfiability

Main article: 2-satisfiability

SAT is easier if the formulas are restricted to those in disjunctive normal form, that is, they are disjunction (OR) of terms, where each term is a conjunction (AND) of literals (possibly negated variables). Such a formula is indeed satisfiable if and only if at least one of its terms is satisfiable, and a term is satisfiable if and only if it does not contain both x and NOT x for some variable x. This can be checked in polynomial time. 2-satisfiability (abbreviated as 2-SAT) is a special case of satisfiability if expressions are written in conjunctive normal form with 2 variables per clause (2-CNF). ... In boolean logic, a disjunctive normal form (DNF) is a standardization (or normalization) of a logical formula which is a disjunction of conjunctive clauses. ...

SAT is also easier if the number of literals in a clause is limited to 2, in which case the problem is called 2SAT. This problem can also be solved in polynomial time, and in fact is complete for the class NL. Similarly, if we limit the number of literals per clause to 2 and change the AND operations to XOR operations, the result is exclusive-or 2-satisfiability, a problem complete for SL = L. In computational complexity theory, NL is the complexity class containing decision problems which can be solved by a nondeterministic Turing machine using a logarithmic amount of memory space. ... Exclusive disjunction (usual symbol xor) is a logical operator that results in true if one of the operands (not both) is true. ... In computational complexity theory, SL (Symmetric Logspace) is the complexity class of problems log-space reducible to USTCON, which is the problem of determining whether there exists a path between two vertices in an undirected graph, otherwise described as the problem of determining whether two vertices are in the same... In computational complexity theory, L is the complexity class containing decision problems which can be solved by a deterministic Turing machine using a logarithmic amount of memory space. ...

One of the most important restrictions of SAT is HORNSAT, where the formula is a conjunction of Horn clauses. This problem is solved by the polynomial-time Horn-satisfiability algorithm, and is in fact P-complete. It can be seen as P's version of the Boolean satisfiability problem. In logic, and in particular in propositional calculus, a Horn clause is a proposition of the general type (p and q and . ... In formal logic, Horn-satisfiability is the problem of deciding whether a given set of Horn clauses is satisfiable or not. ... In complexity theory, the complexity class P-complete is a set of decision problems and is useful in the analysis of which problems can be efficiently solved on parallel computers. ... In computational complexity theory, P is the complexity class containing decision problems which can be solved by a deterministic Turing machine using a polynomial amount of computation time, or polynomial time. ...

Provided that the complexity classes P and NP are not equal, none of these restrictions are NP-complete, unlike SAT. The assumption that P and NP are not equal is not currently proved. Diagram of complexity classes provided that P ≠ NP. The existence of problems outside both P and NP-complete in this case was established by Ladner. ...

3-satisfiability

3-satisfiability is a special case of k-satisfiability (k-SAT) or simply satisfiability (SAT), when each clause contains exactly k = 3 literals. It was one of Karp's 21 NP-complete problems. One of the most important results of computational complexity theory was Stephen Cooks 1971 paper that demonstrated the first NP-complete problem, the boolean satisfiability problem. ...

Here is an example, where ~ indicates NOT:

E = (x₁ or ~x₂ or ~x₃) and (x₁ or x₂ or x₄)

E has two clauses (denoted by parentheses), four literals (x₁, x₂, x₃, x₄), and k=3 (three literals per clause).

To solve this instance of the decision problem we must determine whether there is a truth value (TRUE or FALSE) we can assign to each of the literals (x₁ through x₄) such that the entire expression is TRUE. In this instance, there is such an assignment (x₁ = TRUE, x₂ = TRUE, x₃=TRUE, x₄=TRUE), so the answer to this instance is YES. This is one of many possible assignments, with for instance, any set of assignments including x₁ = TRUE being sufficient. If there were no such assignment(s), the answer would be NO.

Since k-SAT (the general case) reduces to 3-SAT, and 3-SAT can be proven to be NP-complete, it can be used to prove that other problems are also NP-complete. This is done by showing how a solution to another problem could be used to solve 3-SAT. An example of a problem where this method has been used is "Clique". It's often easier to use reductions from 3-SAT than SAT to problems which researchers are attempting to prove NP-complete. In complexity theory, the NP-complete problems are the most difficult problems in NP, in the sense that they are the ones most likely not to be in P. The reason is that if you could find a way to solve an NP-complete problem quickly, then you could use... In computational complexity theory, the clique problem is a graph-theoretical NP-complete problem. ...

3-SAT can be further restricted to One-in-three 3SAT, where we ask if exactly one of the variables in each clause is true, rather than at least one. One-in-three 3SAT remains NP-complete. This article or section is in need of attention from an expert on the subject. ...

Horn-satisfiability

Main article: Horn-satisfiability

A clause is Horn if it contains at most one positive literal. Such clauses are of interest because they are able to express entailment of one variable from a set of other variables. Indeed, one such clauses can be rewritten as , that is, if are all true, then y needs to be true as well. In formal logic, Horn-satisfiability is the problem of deciding whether a given set of Horn clauses is satisfiable or not. ...

The problem of deciding whether a set of Horn clauses is satisfiable is in P. This problem can indeed be solved by a single step of the Unit propagation, which produces the single minimal (w.r.t. the set of literal assigned to true) model of the set of Horn clauses. Unit propagation is a procedure of automated theorem proving that can simplify a set of (usually propositional) clauses. ...

A generalization of the class of Horn formulae is that of renamable-Horn formulae, which is the set of formulae that can be placed in Horn form by replacing some variables with their respective negation. 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.

Schaefer's dichotomy theorem

Main article: Schaefer's dichotomy theorem

The restrictions above (CNF, 2CNF, 3CNF, Horn) bound the considered formulae to be conjunction of subformulae; each restriction states a specific form for all subformulae: for example, only binary clauses can be subformulae in 2CNF. In computational complexity theory, a branch of computer science, Schaefers theorem states necessary and sufficient conditions under which a set O of Boolean operators generate polynomial-time or NP-complete problems when some of the operators of O are applied to some of the propositional variables. ...

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 either in P or NP-complete. The membership in P of the satisfiability of 2CNF and Horn formulae are special cases of this theorem.

Runtime behavior

As mentioned briefly above, though the problem is NP-complete, many practical instances can be solved much more quickly. Many practical problems are actually "easy", so the SAT solver can easily find a solution, or prove that none exists, relatively quickly, even though the instance has thousands of variables and tens of thousands of constraints. Other much smaller problems exhibit run-times that are exponential in the problem size, and rapidly become impractical. Unfortunately, there is no reliable way to tell the difficulty of the problem without trying it. Therefore, almost all SAT solvers include time-outs, so they will terminate even if they cannot find a solution. Finally, 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.^[1]

Extensions of SAT

An extension that has gained significant popularity since 2003 is Satisfiability modulo theories 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. Satisfiability Modulo Theories (SMT) problem is a decision problem for logical formulas with respect to combinations of background theories expressed in classical first-order logic with equality. ...

The satisfiability problem seems to become more difficult (PSPACE-complete) if we allow quantifiers such as "for all" and "there exists" that bind the Boolean variables. An example of such an expression would be: In language and logic, quantification is a construct that specifies the extent of validity of a predicate, that is the extent to which a predicate holds over a range of things. ...

If we use only quantifiers, this is still the SAT problem. If we allow only quantifiers, it becomes the Co-NP-complete tautology problem. If we allow both, 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. In complexity theory, the complexity class Co-NP-complete is the set of problems that are the hardest problems in Co-NP, in the sense that they are the ones most likely not to be in P. If you can find a way to solve a Co-NP-complete problem... In propositional logic, a tautology (from the Greek word ταυτολογία) is a sentence that is true in every valuation (also called interpretation) of its propositional variables, independent of the truth values assigned to these variables. ... In computational complexity theory, the quantified boolean formula problem (QBF) is a generalization of the boolean satisfiability problem in which both existential quantifiers and universal quantifiers can be applied to each variable. ... In complexity theory, PSPACE-complete is a complexity class. ...

A number of variants deal with the number of variable assignments making the formula true. Ordinary SAT asks if there is at least one such assignment. MAJSAT, which asks if the majority of all assignments make the formula true, is complete for PP, a probabilistic class. The problem of how many variable assignments satisfy a formula, not a decision problem, is in #P. UNIQUE-SAT or USAT is the problem of determining whether a formula known to have either zero or one satisfying assignments has zero or has one. Although this problem seems easier, it has been shown that if there is a practical (randomized polynomial-time) algorithm to solve this problem, then all problems in NP can be solved just as easily. In complexity theory, PP is the class of decision problems solvable by a probabilistic Turing machine in polynomial time, with an error probability of less than 1/2 for all instances. ... The title given to this article is incorrect due to technical limitations. ... Valiant-Vazirani Theorem Introduction The Valiant-Vazirani Theorem was proven by Leslie Valiant and Vijay Vazirani in their paper titled NP is as easy as detecting unique solutions published in 1986. ... This article is about the complexity class. ... In computational complexity theory, NP (Non-deterministic Polynomial time) is the set of decision problems solvable in polynomial time on a non-deterministic Turing machine. ...

The maximum satisfiability problem, an FNP generalization of SAT, 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. The introduction to this article provides insufficient context for those unfamiliar with the subject matter. ... In computational complexity theory, the complexity class FNP is the function problem extension of the decision problem class NP. The name is a bit of a misnomer, since technically it is a class of binary relations, not functions, as the following formal definition explains: A binary relation P(x,y... In computer science, approximation algorithms are an approach to attacking NP-hard optimization problems. ... In complexity theory the class APX (an abbreviation of approximable) is the set of NP optimization problems that allow polynomial-time approximation algorithms with approximation ratio bounded by a constant (or constant-factor approximation algorithms for short). ... In computer science, a polynomial-time approximation scheme (abbreviated PTAS) is a type of approximation algorithm for optimization problems (most often, NP-hard optimization problems). ...

Algorithms for solving SAT

There are two classes of high-performance algorithms for solving instances of SAT in practice: modern variants of the DPLL algorithm, such as Chaff, GRASP or march, and stochastic local search algorithms, such as WalkSAT. Flowcharts are often used to represent algorithms. ... The DPLL/Davis-Putnam-Logemann-Loveland algorithm is a complete, backtracking-based algorithm for deciding the satisfiability of propositional logic formulae in conjunctive normal form, i. ... Chaff is an algorithm for solving instances of the boolean satisfiability problem in programming. ... GRASP is a well known SAT instance solver. ... GSAT and WalkSat are local search algorithms to solve boolean satisfiability problems. ...

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 60s (see references below) and is now commonly referred to as the Davis-Putnam-Logemann-Loveland (DPLL) algorithm (also "DLL").

Modern SAT solvers (developed in the last ten years) come in two flavours: "conflict-driven" and "look-ahead". Conflict-driven solvers augment the basic DPLL search algorithm with efficient conflict analysis, clause learning, non-chronological backtracking (aka 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). 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 have inside actually an easy instance). PCB Layout Program Electronic design automation (EDA) is the category of tools for designing and producing electronic systems ranging from printed circuit boards (PCBs) to integrated circuits. ...

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 in the public domain, and are remarkably easy to use. In particular, MiniSAT, which was relatively successful at the 2005 SAT competition, only has about 600 lines of code. Minisat is an example of a conflict driven solver, and an example for look-ahead solvers is march_dl, which won a prize at the 2007 SAT competition.

Genetic algorithms and other general-purpose stochastic local search methods are also being used to solve SAT problems, especially when there is no or limited knowledge of the specific structure of the problem instances to be solved. 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). A genetic algorithm (GA) is a search technique used in computing to find exact or approximate solutions to optimization and search problems. ... Hardware Design, or computer hardware design, is integral to how a computer operates. ... In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of a system with respect to a certain formal specification or property, using formal methods. ... A binary decision diagram (BDD), like a negation normal form (NNF) or a propositional directed acyclic graph (PDAG), is a data structure that is used to represent a Boolean function. ...

Propositional satisfiability has various generalisations, including satisfiability for quantified Boolean formula problem, for first- and second-order logic, constraint satisfaction problems, 0-1 integer programming, and maximum satisfiability problem. In computational complexity theory, the quantified boolean formula problem (QBF) is a generalization of the boolean satisfiability problem in which both existential quantifiers and universal quantifiers can be applied to each variable. ... First-order predicate calculus or first-order logic (FOL) permits the formulation of quantified statements such as there exists an x such that. ... In mathematical logic, second-order logic is an extension of first-order logic, which itself is an extension of propositional logic. ... Constraint-satisfaction problems or CSPs are mathematical problems where one must find states or objects in a system that satisfy a number of constraints or criteria. ... -1... The introduction to this article provides insufficient context for those unfamiliar with the subject matter. ...

Many other decision problems, such as graph colouring problems, planning problems, and scheduling problems, can be easily encoded into SAT. A 3-coloring suits this graph, but fewer colors would result in adjacent vertices of the same color. ...

See also

• Unsatisfiable core

Given an unsatisfiable boolean propositional formula in conjunctive normal form, a subset of clauses whose conjunction is still unsatisfiable is called an unsatisfiable core of the original formula. ...

References

• M. Davis and H. Putnam, A Computing Procedure for Quantification Theory , Journal of the Association for Computing Machinery, vol. 7, no., pp. 201-215, 1960.
• M. Davis, G. Logemann, and D. Loveland, A Machine Program for Theorem-Proving , Communications of the ACM, vol. 5, no. 7, pp. 394-397, 1962.
• S. A. Cook, The Complexity of Theorem Proving Procedures , in Proc. 3rd Ann. ACM Symp. on Theory of Computing, pp. 151-158, Association for Computing Machinery, 1971.
• Michael R. Garey and David S. Johnson (1979). Computers and Intractability: A Guide to the Theory of NP-Completeness. W.H. Freeman. ISBN 0-7167-1045-5.  A9.1: LO1 – LO7, pp.259 – 260.
• J. P. Marques-Silva and K. A. Sakallah, GRASP: A Search Algorithm for Propositional Satisfiability , IEEE Transactions on Computers, vol. 48, no. 5, pp. 506-521, 1999.
• J.-P. Marques-Silva and T. Glass, Combinational Equivalence Checking Using Satisfiability and Recursive Learning , in Proc. Design, Automation and Test in Europe Conference, pp. 145-149, 1999.
• 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.
• M. W. Moskewicz, C. F. Madigan, Y. Zhao, L. Zhang, and S. Malik, Chaff: engineering an efficient SAT solver , in Proc. 38th ACM/IEEE Design Automation Conference, pp. 530-535, Las Vegas, Nevada, 2001.
• E. Clarke, A. Biere, R. Raimi, and Y. Zhu, Bounded Model Checking Using Satisfiability Solving , Formal Methods in System Design, vol. 19, no. 1, 2001.
• M. Perkowski and A. Mishchenko, "Logic Synthesis for Regular Layout using Satisfiability," in Proc. Intl Workshop on Boolean Problems, 2002.
• G.-J. Nam, K. A. Sakallah, and R. Rutenbar, A New FPGA Detailed Routing Approach via Search-Based Boolean Satisfiability , IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, vol. 21, no. 6, pp. 674-684, 2002.
• N. Een and N. Sorensson, An Extensible SAT-solver , in Satisfiability Workshop, 2003.
• D. Babić, J. Bingham, and A. J. Hu, B-Cubing: New Possibilities for Efficient SAT-Solving , IEEE Transactions on Computers 55(11):1315–1324, 2006.

1. ^ The international SAT Competitions web page. Retrieved on 2007-11-15.

Michael R. Garey is a computer science researcher, and co-author (with David S. Johnson) of Computers and Intractibility: A Guide to the Theory of NP-completeness. ... David S. Johnson (born December 9, 1945) is a computer scientist specializing in algorithms and optimization. ... This is a list of important publications in computer science, organized by field. ... IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, often abbreviated IEEE TCAD or IEEE Transactions on CAD, is a technical journal devoted to the design, analysis, and use of computer programs that aid in the design of integrated circuits and systems. ... Year 2007 (MMVII) is the current year, a common year starting on Monday of the Gregorian calendar and the AD/CE era in the 21st century. ... is the 319th day of the year (320th in leap years) in the Gregorian calendar. ...

External links

SAT Solvers:

• Chaff
• HyperSAT
• Spear
• The MiniSAT Solver
• UBCSAT
• Sat4j

Conferences/Publications:

• SAT 2007: Tenth International Conference on Theory and Applications of Satisfiability Testing
• Journal on Satisfiability, Boolean Modeling and Computation
• Survey Propagation

Benchmarks:

• Forced Satisfiable SAT Benchmarks
• IBM Formal Verification SAT Benchmarks
• SATLIB
• Software Verification Benchmarks

SAT solving in general:

• http://www.satlive.org
• http://www.satisfiability.org

This article includes material from a column in the ACM SIGDA e-newsletter by Prof. Karem Sakallah
Original text is available here.