Misplaced Pages

#859140

85-496: Since Boolean satisfiability 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

170-498: 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

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

340-460: A decision problem as a formal language in some fixed encoding, the set NPC of all NP-complete problems is not closed under: It is not known whether NPC is closed under complementation , since NPC= co-NPC if and only if NP= co-NP , and since NP=co-NP is an open question . Quantifier (logic) In logic , a quantifier is an operator that specifies how many individuals in the domain of discourse satisfy an open formula . For instance,

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

510-441: A "for all x " proposition, one needs no more than to find an x for which the predicate is false. Similarly, to disprove a "there exists an x " proposition, one needs to show that the predicate is false for all x . In classical logic , every formula is logically equivalent to a formula in prenex normal form , that is, a string of quantifiers and bound variables followed by a quantifier-free formula. Quantifier elimination

595-540: 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

680-911: 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

765-447: A first-order logic statement, quantifications in the same type (either universal quantifications or existential quantifications) can be exchanged without changing the meaning of the statement, while the exchange of quantifications in different types changes the meaning. As an example, the only difference in the definition of uniform continuity and (ordinary) continuity is the order of quantifications. First order quantifiers approximate

850-420: A function of subsequently introduced variables. A less trivial example from mathematical analysis regards the concepts of uniform and pointwise continuity, whose definitions differ only by an exchange in the positions of two quantifiers. A function f from R to R is called In the former case, the particular value chosen for δ can be a function of both ε and x , the variables that precede it. In

935-399: 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

#1732877032860

1020-529: 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

1105-622: 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

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

1275-502: 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

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

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

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

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

1700-455: Is a concept of simplification used in mathematical logic , model theory , and theoretical computer science . Informally, a quantified statement " ∃ x {\displaystyle \exists x} such that … {\displaystyle \ldots } " can be viewed as a question "When is there an x {\displaystyle x} such that … {\displaystyle \ldots } ?", and

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

SECTION 20

#1732877032860

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

1955-405: 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

2040-482: Is always false. A more natural way to restrict the domain of discourse uses guarded quantification . For example, the guarded quantification means In some mathematical theories , a single domain of discourse fixed in advance is assumed. For example, in Zermelo–Fraenkel set theory , variables range over all sets. In this case, guarded quantifiers can be used to mimic a smaller range of quantification. Thus in

2125-515: 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

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

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

2380-432: Is critical to meaning, as is illustrated by the following two propositions: This is clearly true; it just asserts that every natural number has a square. The meaning of the assertion in which the order of quantifiers is reversed is different: This is clearly false; it asserts that there is a single natural number s that is the square of every natural number. This is because the syntax directs that any variable cannot be

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

2550-446: Is equivalent to the logical conjunction P ( a 1 ) ∧ . . . ∧ P ( a n ) {\displaystyle P(a_{1})\land ...\land P(a_{n})} . Dually, the existentially quantified formula ∃ x ∈ D P ( x ) {\displaystyle \exists x\in D\;P(x)} is equivalent to

2635-426: Is free, while the occurrence of x and y in B ( y , x ) is bound (i.e. non-free). An interpretation for first-order predicate calculus assumes as given a domain of individuals X . A formula A whose free variables are x 1 , ..., x n is interpreted as a Boolean -valued function F ( v 1 , ..., v n ) of n arguments, where each argument ranges over the domain X . Boolean-valued means that

Satisfiability modulo theories - Misplaced Pages Continue

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

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

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

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

3060-498: Is read, "for every x that is a member of X , P applies to x or Q applies to x ". Some other quantified expressions are constructed as follows, for a formula P . These two expressions (using the definitions above) are read as "there exists a friend of Peter who likes to dance" and "all friends of Peter like to dance", respectively. Variant notations include, for set X and set members x : All of these variations also apply to universal quantification. Other variations for

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

3230-401: Is short for "nondeterministic polynomial-time complete". In this name, "nondeterministic" refers to nondeterministic Turing machines , a way of mathematically formalizing the idea of a brute-force search algorithm. Polynomial time refers to an amount of time that is considered "quick" for a deterministic algorithm to check a single solution, or for a nondeterministic Turing machine to perform

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

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

3485-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*

Satisfiability modulo theories - Misplaced Pages Continue

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

3655-797: 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

3740-591: 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 NP-complete In computational complexity theory , a problem is NP-complete when: The name "NP-complete"

3825-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}

3910-461: 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

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

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

4165-581: 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.,

4250-699: The logical disjunction P ( a 1 ) ∨ . . . ∨ P ( a n ) {\displaystyle P(a_{1})\lor ...\lor P(a_{n})} . For example, if B = { 0 , 1 } {\displaystyle B=\{0,1\}} is the set of binary digits , the formula ∀ x ∈ B x = x 2 {\displaystyle \forall x\in B\;x=x^{2}} abbreviates 0 = 0 2 ∧ 1 = 1 2 {\displaystyle 0=0^{2}\land 1=1^{2}} , which evaluates to true . Consider

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

SECTION 50

#1732877032860

4420-440: The universal quantifier ∀ {\displaystyle \forall } in the first order formula ∀ x P ( x ) {\displaystyle \forall xP(x)} expresses that everything in the domain satisfies the property denoted by P {\displaystyle P} . On the other hand, the existential quantifier ∃ {\displaystyle \exists } in

4505-402: The "∀ x " or "∃ x " might appear after or in the middle of P ( x ). Formally, however, the phrase that introduces the dummy variable is placed in front. Mathematical formulas mix symbolic expressions for quantifiers with natural language quantifiers such as, Keywords for uniqueness quantification include: Further, x may be replaced by a pronoun . For example, The order of quantifiers

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

4675-529: The conjuncts, since irrationals cannot be enumerated. A succinct, equivalent formulation which avoids these problems uses universal quantification : A similar analysis applies to the disjunction , which can be rephrased using existential quantification : It is possible to devise abstract algebras whose models include formal languages with quantification, but progress has been slow and interest in such algebra has been limited. Three approaches have been devised to date: The two most common quantifiers are

4760-493: The course of a mathematical argument. A universally quantified formula over an empty range (like ∀ x ∈ ∅ x ≠ x {\displaystyle \forall x\!\in \!\varnothing \;x\neq x} ) is always vacuously true . Conversely, an existentially quantified formula over an empty range (like ∃ x ∈ ∅ x = x {\displaystyle \exists x\!\in \!\varnothing \;x=x} )

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

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

5015-473: 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

5100-476: The example above, to express in Zermelo–Fraenkel set theory, one would write where N is the set of all natural numbers. Mathematical semantics is the application of mathematics to study the meaning of expressions in a formal language. It has three elements: a mathematical specification of a class of objects via syntax , a mathematical specification of various semantic domains and the relation between

5185-496: 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,

SECTION 60

#1732877032860

5270-488: The following statement ( using dot notation for multiplication ): This has the appearance of an infinite conjunction of propositions. From the point of view of formal languages , this is immediately a problem, since syntax rules are expected to generate finite words. The example above is fortunate in that there is a procedure to generate all the conjuncts. However, if an assertion were to be made about every irrational number , there would be no way to enumerate all

5355-399: The formula ¬ ∃ x P ( x ) {\displaystyle \neg \exists xP(x)} which expresses that nothing has the property P {\displaystyle P} . Other quantifiers are only definable within second order logic or higher order logics . Quantifiers have been generalized beginning with the work of Mostowski and Lindström . In

5440-744: The formula ∃ x P ( x ) {\displaystyle \exists xP(x)} expresses that there exists something in the domain which satisfies that property. A formula where a quantifier takes widest scope is called a quantified formula. A quantified formula must contain a bound variable and a subformula specifying a property of the referent of that variable. The most commonly used quantifiers are ∀ {\displaystyle \forall } and ∃ {\displaystyle \exists } . These quantifiers are standardly defined as duals ; in classical logic , they are interdefinable using negation . They can also be used to define more complex quantifiers, as in

5525-439: The function assumes one of the values T (interpreted as truth) or F (interpreted as falsehood). The interpretation of the formula is the function G of n -1 arguments such that G ( v 1 , ..., v n -1 ) = T if and only if F ( v 1 , ..., v n -1 , w ) = T for every w in X . If F ( v 1 , ..., v n -1 , w ) = F for at least one value of w , then G ( v 1 , ..., v n -1 ) = F . Similarly

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

5695-405: The latter case, δ can be a function only of ε (i.e., it has to be chosen independent of x ). For example, f ( x ) = x satisfies pointwise, but not uniform continuity (its slope is unbound). In contrast, interchanging the two initial universal quantifiers in the definition of pointwise continuity does not change the meaning. As a general rule, swapping two adjacent universal quantifiers with

5780-497: The meanings of some natural language quantifiers such as "some" and "all". However, many natural language quantifiers can only be analyzed in terms of generalized quantifiers . For a finite domain of discourse D = { a 1 , . . . a n } {\displaystyle D=\{a_{1},...a_{n}\}} , the universally quantified formula ∀ x ∈ D P ( x ) {\displaystyle \forall x\in D\;P(x)}

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

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

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

6120-440: The same scope (or swapping two adjacent existential quantifiers with the same scope) doesn't change the meaning of the formula (see Example here ), but swapping an existential quantifier and an adjacent universal quantifier may change its meaning. The maximum depth of nesting of quantifiers in a formula is called its " quantifier rank ". If D is a domain of x and P ( x ) is a predicate dependent on object variable x , then

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

6290-540: The set of values that the variable takes. In the examples above, the range of quantification is the set of natural numbers. Specification of the range of quantification allows us to express the difference between, say, asserting that a predicate holds for some natural number or for some real number . Expository conventions often reserve some variable names such as " n " for natural numbers, and " x " for real numbers, although relying exclusively on naming conventions cannot work in general, since ranges of variables can change in

6375-456: The statement without quantifiers can be viewed as the answer to that question. One way of classifying formulas is by the amount of quantification. Formulas with less depth of quantifier alternation are thought of as being simpler, with the quantifier-free formulas as the simplest. Every quantification involves one specific variable and a domain of discourse or range of quantification of that variable. The range of quantification specifies

6460-589: The statement, "Each of Peter's friends either likes to dance or likes to go to the beach (or both)", key aspects can be identified and rewritten using symbols including quantifiers. So, let X be the set of all Peter's friends, P ( x ) the predicate " x likes to dance", and Q ( x ) the predicate " x likes to go to the beach". Then the above sentence can be written in formal notation as ∀ x ∈ X , ( P ( x ) ∨ Q ( x ) ) {\displaystyle \forall {x}{\in }X,(P(x)\lor Q(x))} , which

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

6630-441: 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

6715-433: The two, which is usually expressed as a function from syntactic objects to semantic ones. This article only addresses the issue of how quantifier elements are interpreted. The syntax of a formula can be given by a syntax tree. A quantifier has a scope , and an occurrence of a variable x is free if it is not within the scope of a quantification for that variable. Thus in the occurrence of both x and y in C ( y , x )

6800-401: The universal proposition can be expressed as This notation is known as restricted or relativized or bounded quantification . Equivalently one can write, The existential proposition can be expressed with bounded quantification as or equivalently Together with negation, only one of either the universal or existential quantifier is needed to perform both tasks: which shows that to disprove

6885-434: The universal quantifier and the existential quantifier. The traditional symbol for the universal quantifier is " ∀ ", a rotated letter " A ", which stands for "for all" or "all". The corresponding symbol for the existential quantifier is " ∃ ", a rotated letter " E ", which stands for "there exists" or "exists". An example of translating a quantified statement in a natural language such as English would be as follows. Given

6970-492: The universal quantifier are Some versions of the notation explicitly mention the range of quantification. The range of quantification must always be specified; for a given mathematical theory, this can be done in several ways: One can use any variable as a quantified variable in place of any other, under certain restrictions in which variable capture does not occur. Even if the notation uses typed variables, variables of that type may be used. Informally or in natural language,

7055-564: 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

7140-402: The whole search. " Complete " refers to the property of being able to simulate everything in the same complexity class . More precisely, each input to the problem should be associated with a set of solutions of polynomial length, the validity of each of which can be tested quickly (in polynomial time ), such that the output for any input is "yes" if the solution set is non-empty and "no" if it

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

#859140