satisfiable

Satisfiable refers to the existence of an assignment or interpretation that makes a logical formula true. In propositional logic, a formula is satisfiable if there exists a truth assignment to its propositional variables that makes the formula evaluate to true. If no such assignment exists, the formula is unsatisfiable. A formula that is true under every possible assignment is called valid, and is also satisfiable by any assignment.

In first-order logic and in model theory, satisfiability is defined relative to a structure (model). A sentence is satisfiable if there exists a structure in which it is true. A set of sentences is satisfiable if there is some model in which all sentences hold. A theory is satisfiable if it has at least one model. Satisfiability thus concerns whether a given collection of statements can be true together in some interpretation.

Examples illustrate the idea. The propositional formula P ∨ Q is satisfiable (for instance, P = true, Q = false). The conjunction P ∧ ¬P is unsatisfiable. A theory containing contradictory axioms, such as ∀x P(x) and ∃x ¬P(x), is unsatisfiable because no structure can satisfy both simultaneously.

Computationally, the satisfiability problem (SAT) asks whether a given propositional formula is satisfiable and is NP-complete in general. Restricted variants include 2-SAT, solvable in polynomial time, and Horn-SAT, solvable in linear time. In first-order logic, satisfiability is, in general, undecidable. Practical methods often extend to satisfiability modulo theories (SMT), combining SAT with domain-specific theories like arithmetic.