Misplaced Pages

#834165

76-853: CVC4 competed in SMT-COMP in the years 2014-2020, and cvc5 has competed in the years 2021-2022. CVC4 competed in SyGuS-COMP in the years 2015-2019, and in CASC in 2013-2015. CVC4 uses the DPLL(T) architecture, and supports the theories of linear arithmetic over rationals and integers , fixed-width bitvectors, floating-point arithmetic , strings , (co)-datatypes , sequences (used to model dynamic arrays ), finite sets and relations , separation logic , and uninterpreted functions among others. cvc5 additionally supports finite fields . In addition to standard SMT and SyGuS solving, cvc5 supports abductive reasoning , which

152-500: A DPLL -style search with theory-specific solvers ( T-solvers ) that handle conjunctions (ANDs) of predicates from a given theory. This approach is referred to as the lazy approach . Dubbed DPLL(T) , this architecture gives the responsibility of Boolean reasoning to the DPLL-based SAT solver which, in turn, interacts with a solver for theory T through a well-defined interface. The theory solver only needs to worry about checking

228-479: A constraint satisfaction problem and thus a certain formalized approach to constraint programming . Formally speaking, an SMT instance is a formula in first-order logic , where some function and predicate symbols have additional interpretations, and SMT is the problem of determining whether such a formula is satisfiable. In other words, imagine an instance of the Boolean satisfiability problem (SAT) in which some of

304-525: 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 ,

380-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

456-487: 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

532-586: A 32-bit integer variable would be encoded by 32 single-bit variables with appropriate weights and word-level operations such as 'plus' would be replaced by lower-level logic operations on the bits) and passing this formula to a Boolean SAT solver. This approach, which is referred to as the eager approach (or bitblasting ), has its merits: by pre-processing the SMT formula into an equivalent Boolean SAT formula existing Boolean SAT solvers can be used "as-is" and their performance and capacity improvements leveraged over time. On

608-636: 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 ,

684-913: A class of theory that support efficient theory propagation and conflict analysis, enabling practical use within DPLL(T) solvers. Monotonic theories support only boolean variables (boolean is the only sort ), and all their functions and predicates p obey the axiom p ( … , b i − 1 , 0 , b i + 1 , … ) ⟹ p ( … , b i − 1 , 1 , b i + 1 , … ) {\displaystyle p(\ldots ,b_{i-1},0,b_{i+1},\ldots )\implies p(\ldots ,b_{i-1},1,b_{i+1},\ldots )} Examples of monotonic theories include graph reachability , collision detection for convex hulls , minimum cuts , and computation tree logic . Every Datalog program can be interpreted as

760-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

836-400: A monotonic theory. Most of the common SMT approaches support decidable theories. However, many real-world systems, such as an aircraft and its behavior, can only be modelled by means of non-linear arithmetic over the real numbers involving transcendental functions . This fact motivates an extension of the SMT problem to non-linear theories, such as determining whether the following equation

SECTION 10

#1733106473835

912-531: A non-linear optimization packet as (necessarily incomplete) subordinate theory solver, iSAT , building on a unification of DPLL SAT-solving and interval constraint propagation called the iSAT algorithm, and cvc5 . The table below summarizes some of the features of the many available SMT solvers. The column "SMT-LIB" indicates compatibility with the SMT-LIB language; many systems marked 'yes' may support only older versions of SMT-LIB, or offer only partial support for

988-625: A number of standardized benchmarks and has enabled a yearly competition between SMT solvers called SMT-COMP. Initially, the competition took place during the Computer Aided Verification conference (CAV), but as of 2020 the competition is hosted as part of the SMT Workshop, which is affiliated with the International Joint Conference on Automated Reasoning (IJCAR). SMT solvers are useful both for verification, proving

1064-478: 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

1140-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,

1216-558: 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

1292-466: 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

1368-505: A standardized interface to SMT solvers (and automated theorem provers , a term often used synonymously). The most prominent is the SMT-LIB standard, which provides a language based on S-expressions . Other standardized formats commonly supported are the DIMACS format supported by many Boolean SAT solvers, and the CVC format used by the CVC automated theorem prover. The SMT-LIB format also comes with

1444-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

1520-495: 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

1596-437: 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

SECTION 20

#1733106473835

1672-440: Is a dependently typed language that uses Z3 to find proofs; the compiler carries these proofs through to produce proof-carrying bytecode. The Viper verification infrastructure encodes verification conditions to Z3. The sbv library provides SMT-based verification of Haskell programs, and lets the user choose among a number of solvers such as Z3, ABC, Boolector, cvc5, MathSAT and Yices. There are also many verifiers built on top of

1748-523: 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

1824-421: Is already NP-complete , the SMT problem is typically NP-hard , and for many theories it is undecidable . Researchers study which theories or subsets of theories lead to a decidable SMT problem and the computational complexity of decidable cases. The resulting decision procedures are often implemented directly in SMT solvers; see, for instance, the decidability of Presburger arithmetic . SMT can be thought of as

1900-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

1976-406: Is also decidable. Since multiplication by constants can be implemented as nested additions, the arithmetic in many computer programs can be expressed using Presburger arithmetic, resulting in decidable formulas. Examples of SMT solvers addressing Boolean combinations of theory atoms from undecidable arithmetic theories over the reals are ABsolver, which employs a classical DPLL(T) architecture with

2052-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

2128-470: Is blurry enough that some ATPs participate in SMT-COMP, while some SMT solvers participate in CASC . An SMT instance is a generalization of a Boolean SAT instance in which various sets of variables are replaced by predicates from a variety of underlying theories. SMT formulas provide a much richer modeling language than is possible with Boolean SAT formulas. For example, an SMT formula allows one to model

2204-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

2280-594: 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

2356-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

Cooperating Validity Checker - Misplaced Pages Continue

2432-541: Is derived from the fact that these expressions are interpreted within ("modulo") a certain formal theory in first-order logic with equality (often disallowing quantifiers ). SMT solvers are tools that aim to solve the SMT problem for a practical subset of inputs. SMT solvers such as Z3 and cvc5 have been used as a building block for a wide range of applications across computer science, including in automated theorem proving , program analysis , program verification , and software testing . Since Boolean satisfiability

2508-557: 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

2584-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,

2660-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

2736-484: 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

2812-410: 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

2888-399: Is satisfiable: where Such problems are, however, undecidable in general. (On the other hand, the theory of real closed fields , and thus the full first order theory of the real numbers , are decidable using quantifier elimination . This is due to Alfred Tarski .) The first order theory of the natural numbers with addition (but not multiplication), called Presburger arithmetic ,

2964-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

3040-437: Is some unspecified function of two arguments). These predicates are classified according to each respective theory assigned. For instance, linear inequalities over real variables are evaluated using the rules of the theory of linear real arithmetic , whereas predicates involving uninterpreted terms and function symbols are evaluated using the rules of the theory of uninterpreted functions with equality (sometimes referred to as

3116-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

Cooperating Validity Checker - Misplaced Pages Continue

3192-480: 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

3268-428: Is the problem of constructing a formula B that can be conjoined with a formula A to prove a goal formula C . cvc5 has been subject to several independent test campaigns. CVC4 has been applied to the synthesis of recursive programs. and to the verification of Amazon Web Services access policies. CVC4 and cvc5 have been integrated with Coq and Isabelle . CVC4 is one of the back-end reasoners supported by CBMC,

3344-424: 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

3420-537: Is to translate preconditions, postconditions, loop conditions, and assertions into SMT formulas in order to determine if all properties can hold. There are many verifiers built on top of the Z3 SMT solver . Boogie is an intermediate verification language that uses Z3 to automatically check simple imperative programs. The VCC verifier for concurrent C uses Boogie, as well as Dafny for imperative object-based programs, Chalice for concurrent programs, and Spec# for C#. F*

3496-798: The Alt-Ergo SMT solver. Here is a list of mature applications: Many SMT solvers implement a common interface format called SMTLIB2 (such files usually have the extension " .smt2 "). The LiquidHaskell tool implements a refinement type based verifier for Haskell that can use any SMTLIB2 compliant solver, e.g. cvc5, MathSat, or Z3. An important application of SMT solvers is symbolic execution for analysis and testing of programs (e.g., concolic testing ), aimed particularly at finding security vulnerabilities. Example tools in this category include SAGE from Microsoft Research , KLEE , S2E , and Triton . SMT solvers that have been used for symbolic-execution applications include Z3 , STP Archived 2015-04-06 at

3572-481: 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 the question of whether SAT has

3648-697: The Wayback Machine , the Z3str family of solvers , and Boolector . SMT solvers have been integrated with proof assistants, including Coq and Isabelle/HOL . This article was originally adapted from a column in the ACM SIGDA e-newsletter by Prof. Karem A. Sakallah . Original text is available here Boolean satisfiability problem In logic and computer science , the Boolean satisfiability problem (sometimes called propositional satisfiability problem and abbreviated SATISFIABILITY , SAT or B-SAT )

3724-598: The binary variables are replaced by predicates over a suitable set of non-binary variables. A predicate is a binary-valued function of non-binary variables. Example predicates include linear inequalities (e.g., 3 x + 2 y − z ≥ 4 {\displaystyle 3x+2y-z\geq 4} ) or equalities involving uninterpreted terms and function symbols (e.g., f ( f ( u , v ) , v ) = f ( u , v ) {\displaystyle f(f(u,v),v)=f(u,v)} where f {\displaystyle f}

3800-464: The correctness of programs, software testing based on symbolic execution , and for synthesis , generating program fragments by searching over the space of possible programs. Outside of software verification, SMT solvers have also been used for type inference and for modelling theoretic scenarios, including modelling actor beliefs in nuclear arms control . Computer-aided verification of computer programs often uses SMT solvers. A common technique

3876-445: The datapath operations of a microprocessor at the word rather than the bit level. By comparison, answer set programming is also based on predicates (more precisely, on atomic sentences created from atomic formulas ). Unlike SMT, answer-set programs do not have quantifiers, and cannot easily express constraints such as linear arithmetic or difference logic —answer set programming is best suited to Boolean problems that reduce to

SECTION 50

#1733106473835

3952-668: The empty theory ). Other theories include the theories of arrays and list structures (useful for modeling and verifying computer programs ), and the theory of bit vectors (useful in modeling and verifying hardware designs ). Subtheories are also possible: for example, difference logic is a sub-theory of linear arithmetic in which each inequality is restricted to have the form x − y > c {\displaystyle x-y>c} for variables x {\displaystyle x} and y {\displaystyle y} and constant c {\displaystyle c} . The examples above show

4028-583: The free theory of uninterpreted functions. Implementing 32-bit integers as bitvectors in answer set programming suffers from most of the same problems that early SMT solvers faced: "obvious" identities such as x + y = y + x are difficult to deduce. Constraint logic programming does provide support for linear arithmetic constraints, but within a completely different theoretical framework. SMT solvers have also been extended to solve formulas in higher-order logic . Early attempts for solving SMT instances involved translating them to Boolean SAT instances (e.g.,

4104-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

4180-515: The C Bounded Model Checker. Satisfiability modulo theories#Standardization and the SMT-COMP solver competition In computer science and mathematical logic , satisfiability modulo theories ( SMT ) is the problem of determining whether a mathematical formula is satisfiable . It generalizes the Boolean satisfiability problem (SAT) to more complex formulas involving real numbers , integers , and/or various data structures such as lists , arrays , bit vectors , and strings . The name

4256-447: 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

4332-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

4408-616: 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

4484-483: The development of specialized decidable theories , including linear arithmetic over rationals and integers , fixed-width bitvectors, floating-point arithmetic (often implemented in SMT solvers via bit-blasting , i.e., reduction to bitvectors), strings , (co)-datatypes , sequences (used to model dynamic arrays ), finite sets and relations , separation logic , finite fields , and uninterpreted functions among others. Boolean monotonic theories are

4560-450: The feasibility of conjunctions of theory predicates passed on to it from the SAT solver as it explores the Boolean search space of the formula. For this integration to work well, however, the theory solver must be able to participate in propagation and conflict analysis, i.e., it must be able to infer new facts from already established facts, as well as to supply succinct explanations of infeasibility when theory conflicts arise. In other words,

4636-495: 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 ,

SECTION 60

#1733106473835

4712-492: 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

4788-401: 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 —this is

4864-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

4940-496: The language. The column "CVC" indicates support for the CVC language. The column "DIMACS" indicates support for the DIMACS format . Projects differ not only in features and performance, but also in the viability of the surrounding community, its ongoing interest in a project, and its ability to contribute documentation, fixes, tests and enhancements. There are multiple attempts to describe

5016-489: 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

5092-464: The other hand, the loss of the high-level semantics of the underlying theories means that the Boolean SAT solver has to work a lot harder than necessary to discover "obvious" facts (such as x + y = y + x {\displaystyle x+y=y+x} for integer addition.) This observation led to the development of a number of SMT solvers that tightly integrate the Boolean reasoning of

5168-478: 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

5244-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

5320-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

5396-467: 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

5472-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

5548-442: The theory solver must be incremental and backtrackable . Researchers study which theories or subsets of theories lead to a decidable SMT problem and the computational complexity of decidable cases. Since full first-order logic is only semidecidable , one line of research attempts to find efficient decision procedures for fragments of first-order logic such as effectively propositional logic . Another line of research involves

5624-413: 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

5700-566: The use of Linear Integer Arithmetic over inequalities. Other examples include: Most SMT solvers support only quantifier -free fragments of their logics. There is substantial overlap between SMT solving and automated theorem proving (ATP). Generally, automated theorem provers focus on supporting full first-order logic with quantifiers, whereas SMT solvers focus more on supporting various theories (interpreted predicate symbols). ATPs excel at problems with lots of quantifiers, whereas SMT solvers do well on large problems without quantifiers. The line

5776-577: 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

#834165