# Satisfiability

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$ is satisfiable because it is true when $x=3$ and $y=6$ , while the formula $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$ is valid over the integers, but $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 $+$ in a formula such as $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 $+$ , 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.