Concept
Satisfiability
Overview
In mathematical logic, a formula is satisfiable if it is true under some assignment of values to its variables. For example, the formula
x
+
3
=
y
{\displaystyle x+3=y}
is satisfiable because it is true when
x
=
3
{\displaystyle x=3}
and
y
=
6
{\displaystyle y=6}
, while the formula
x
+
1
=
x
{\displaystyle x+1=x}
is not satisfiable over the integers. The dual concept to satisfiability is validity; a formula is valid if every assignment of values to its variables makes the formula true. For example,
x
+
3
=
3
+
x
{\displaystyle x+3=3+x}
is valid over the integers, but
x
+
3
=
y
{\displaystyle x+3=y}
is not.
Formally, satisfiability is studied with respect to a fixed logic defining the syntax of allowed symbols, such as first-order logic, second-order logic or propositional logic. Rather than being syntactic, however, satisfiability is a semantic property because it relates to the meaning of the symbols, for example, the meaning of
+
{\displaystyle +}
in a formula such as
x
+
1
=
x
{\displaystyle x+1=x}
. Formally, we define an interpretation (or model) 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. While this allows non-standard interpretations of symbols such as
+
{\displaystyle +}
, one can restrict their meaning by providing additional axioms. The satisfiability modulo theories problem considers satisfiability of a formula with respect to a formal 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 as Peano arithmetic are satisfiable because they are true in the natural numbers. This concept is closely related to the consistency of a theory, and in fact is equivalent to consistency for first-order logic, a result known as Gö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 to Aristotle's square of opposition.
The problem of determining whether a formula in propositional logic is satisfiable is decidable, and is known as the Boolean satisfiability problem, or SAT. In general, the problem of determining whether a sentence of first-order logic is satisfiable is not decidable. In universal algebra, equational theory, and automated theorem proving, the methods of term rewriting, congruence closure and unification are used to attempt to decide satisfiability. Whether a particular theory is decidable or not depends whether the theory is variable-free and on other conditions.
Overview adapted from Wikipedia (CC BY-SA 4.0; see the article history for authors).
Possible passages
Found by search and not yet checked by a person; they may only mention the idea in passing.
Thus there arises a classification of modes of formation, or in the language commonly used by mathematicians, a classification of Functions. Any number, considered as formed from any other number, is called a function of it; and there are as many kinds of functions as there are modes of formation. The simple functions are by no means numerous, most functions being formed by the combination of several of the…
John Stuart Mill, A System of Logic, Ratiocinative and Inductive
States what Satisfiability is.
The common measure must be some one thing, and also from agreement (for which reason it is called νόμισμα), for this makes all things commensurable: in fact, all things are measured by money. Let B represent ten minæ, A a house worth five minæ, or in other words half B, C a bed worth 1/10th of B: it is clear then how many beds are equal to one house, namely, five. It is obvious also that exchange was thus conducted…
Aristotle, The Nicomachean ethics of Aristotle
States what Satisfiability is; the author is tied to Satisfiability in the knowledge graph.
Any such select set is called the set of postulates, or premises, from which the reasoning proceeds. The reasoning is nothing else than the exhibition of the whole pattern of general conditions involved in the pattern derived from the selected postulates.
Alfred North Whitehead, Science and the modern world
States what Satisfiability is.
Related ideas
- First-order logic
- Gödel's completeness theorem
- Logical conjunction
- Propositional logic
- Mathematical logic
- Model theory
- Validity (logic)
- Peano axioms
- Semantics
- Aristotle
- Second-order logic
- Variable (mathematics)
- Well-formed formula
- Logical constant
- Atomic formula
- Syntax (logic)
- Classical logic
- Computational complexity theory
- Consistency
- David Hilbert
- Decision problem
- Axiom
- Entscheidungsproblem
Place in the tradition
Part of Outline of logic.