Inmathematical logic, aformula issatisfiable if it is true under some assignment of values to itsvariables. For example, the formula${\displaystyle x+3=y}$ is satisfiable because it is true when${\displaystyle x=3}$ and${\displaystyle y=6}$, while the formula${\displaystyle x+1=x}$ is not satisfiable over the integers. The dual concept to satisfiability isvalidity; a formula isvalid if every assignment of values to its variables makes the formula true. For example,${\displaystyle x+3=3+x}$ is valid over the integers, but${\displaystyle x+3=y}$ is not.

Formally, satisfiability is studied with respect to a fixed logic defining thesyntax of allowed symbols, such asfirst-order logic,second-order logic orpropositional logic. Rather than being syntactic, however, satisfiability is asemantic property because it relates to themeaning of the symbols, for example, the meaning of${\displaystyle +}$ in a formula such as${\displaystyle x+1=x}$. Formally, we define aninterpretation (ormodel) to be an assignment of values to the variables and an assignment of meaning to all other non-logical symbols, and a formula is said to be satisfiable if there is some interpretation which makes it true.^[1] While this allows non-standard interpretations of symbols such as${\displaystyle +}$, one can restrict their meaning by providing additionalaxioms. Thesatisfiability modulo theories problem considers satisfiability of a formula with respect to aformal theory, which is a (finite or infinite) set of axioms.

Satisfiability and validity are defined for a single formula, but can be generalized to an arbitrary theory or set of formulas: a theory is satisfiable if at least one interpretation makes every formula in the theory true, and valid if every formula is true in every interpretation. For example, theories of arithmetic such asPeano arithmetic are satisfiable because they are true in the natural numbers. This concept is closely related to theconsistency of a theory, and in fact is equivalent to consistency for first-order logic, a result known asGödel's completeness theorem. The negation of satisfiability is unsatisfiability, and the negation of validity is invalidity. These four concepts are related to each other in a manner exactly analogous toAristotle'ssquare of opposition.

Theproblem of determining whether a formula inpropositional logic is satisfiable isdecidable, and is known as theBoolean satisfiability problem, or SAT. In general, the problem of determining whether a sentence offirst-order logic is satisfiable is not decidable. Inuniversal algebra,equational theory, andautomated theorem proving, the methods ofterm rewriting,congruence closure andunification are used to attempt to decide satisfiability. Whether a particulartheory is decidable or not depends whether the theory isvariable-free and on other conditions.^[2]

Forclassical logics with negation, it is generally possible to re-express the question of the validity of a formula to one involving satisfiability, because of the relationships between the concepts expressed in the above square of opposition. In particular φ is valid if and only if ¬φ is unsatisfiable, which is to say it is false that ¬φ is satisfiable. Put another way, φ is satisfiable if and only if ¬φ is invalid.

For logics without negation, such as thepositive propositional calculus, the questions of validity and satisfiability may be unrelated. In the case of thepositive propositional calculus, the satisfiability problem is trivial, as every formula is satisfiable, while the validity problem isco-NP complete.

In the case ofclassical propositional logic, satisfiability is decidable for propositional formulae. In particular, satisfiability is anNP-complete problem, and is one of the most intensively studied problems incomputational complexity theory.

Forfirst-order logic (FOL), satisfiability isundecidable. More specifically, it is aco-RE-complete problem and therefore notsemidecidable.^[3] This fact has to do with the undecidability of the validity problem for FOL. The question of the status of the validity problem was posed firstly byDavid Hilbert, as the so-calledEntscheidungsproblem. The universal validity of a formula is a semi-decidable problem byGödel's completeness theorem. If satisfiability were also a semi-decidable problem, then the problem of the existence of counter-models would be too (a formula has counter-models iff its negation is satisfiable). So the problem of logical validity would be decidable, which contradicts theChurch–Turing theorem, a result stating the negative answer for the Entscheidungsproblem.

Inmodel theory, anatomic formula is satisfiable if there is a collection of elements of astructure that render the formula true.^[4] IfA is a structure, φ is a formula, anda is a collection of elements, taken from the structure, that satisfy φ, then it is commonly written that

A ⊧ φ [a]

If φ has no free variables, that is, if φ is anatomic sentence, and it is satisfied byA, then one writes

A ⊧ φ

In this case, one may also say thatA is a model for φ, or that φ istrue inA. IfT is a collection of atomic sentences (a theory) satisfied byA, one writes

A ⊧T

A problem related to satisfiability is that offinite satisfiability, which is the question of determining whether a formula admits afinite model that makes it true. For a logic that has thefinite model property, the problems of satisfiability and finite satisfiability coincide, as a formula of that logic has a model if and only if it has a finite model. This question is important in the mathematical field offinite model theory.

Finite satisfiability and satisfiability need not coincide in general. For instance, consider thefirst-order logic formula obtained as theconjunction of the following sentences, where${\displaystyle a_0}$ and${\displaystyle a_1}$ areconstants:

• ${\displaystyle R(a_0,a_1)}$
• ${\displaystyle \mathrm{\forall }xy(R(x,y)\to \mathrm{\exists }zR(y,z))}$
• ${\displaystyle \mathrm{\forall }xyz(R(y,x)\wedge R(z,x)\to y=z))}$
• ${\displaystyle \mathrm{\forall }x\mathrm{\neg }R(x,a_0)}$

The resulting formula has the infinite model${\displaystyle R(a_0,a_1),R(a_1,a_2),\dots }$, but it can be shown that it has no finite model (starting at the fact${\displaystyle R(a_0,a_1)}$ and following the chain of${\displaystyle R}$atoms that must exist by the second axiom, the finiteness of a model would require the existence of a loop, which would violate the third and fourth axioms, whether it loops back on${\displaystyle a_0}$ or on a different element).

Thecomputational complexity of deciding satisfiability for an input formula in a given logic may differ from that of deciding finite satisfiability; in fact, for some logics, only one of them isdecidable.

For classicalfirst-order logic, finite satisfiability isrecursively enumerable (in classRE) andundecidable byTrakhtenbrot's theorem applied to the negation of the formula.

Numerical constraints^[clarify] often appear in the field ofmathematical optimization, where one usually wants to maximize (or minimize) an objective function subject to some constraints. However, leaving aside the objective function, the basic issue of simply deciding whether the constraints are satisfiable can be challenging or undecidable in some settings. The following table summarizes the main cases.

Table source: Bockmayr and Weispfenning.^[5]: 754

For linear constraints, a fuller picture is provided by the following table.

Table source: Bockmayr and Weispfenning.^[5]: 755

• 2-satisfiability
• Boolean satisfiability problem
• Circuit satisfiability
• Karp's 21 NP-complete problems
• Validity
• Constraint satisfaction

• Boolos, George; Burgess, John; Jeffrey, Richard (2007).Computability and Logic (5th ed.). Cambridge University Press.

• Daniel Kroening;Ofer Strichman (2008).Decision Procedures: An Algorithmic Point of View. Springer Science & Business Media.ISBN 978-3-540-74104-6.
• A. Biere; M. Heule; H. van Maaren; T. Walsh, eds. (2009).Handbook of Satisfiability. IOS Press.ISBN 978-1-60750-376-7.

• Concepts in logic
• Logical truth
• Model theory
• Philosophy of logic

• Articles with short description
• Short description is different from Wikidata
• All Wikipedia articles needing clarification
• Wikipedia articles needing clarification from July 2021