Satisfiability

A (well-formed) formula is satisfiable if there is some interpretation in which it holds true. Else, it is unsatisfiable

More causally, if a formula can be made true with some combination of variables, it is valid. If there is no possible way to make it true, it is unsatisfiable.

Definition §

Satisfiability ^definition

A well-formed formula $P$ in a formal language $L$ is satisfiable if it is true under at least one model, $M$. That is, there exists an $M$ such that:

$$M\models P$$

Similarly, $P$ is unsatisfiable if there is no model in which it holds true. This is usually notated as:

$$/\models P$$

$$\models \neg P$$

$$P\models \perp$$

They all mean the same thing - that there is no model that can make $P$ true.

Equisatisfiability §

Equisatisfiability ^definition-equisatisfiability

Two formulas, $F$ and $G$ are equisatisfiable iff:

$$G\text{ is satisfiable iff }F\text{ is satisfiable}$$

This is notated as:

$$F\approx G$$

Equisatisfiability is weaker than logical equivalence but is still a useful property. It is important to note that the model, $M$ that satisfies $F$ can be different from the model, $N$ that satisfies $G$.

In Propositional Logic §

In propositional logic, a proposition is unsatisfiable if:

• It is a contradiction, that is, false under every valuation
• Equivalently, its corresponding truth table has a column of only False

Also, the problem of satisfiability for any proposition (known as the SAT Problem) is decidable

In Predicate Logic §

In predicate logic, satisfiability is undecidable.

Theorems §