Unsatisfiable

Unsatisfiable describes a property of a logical formula, theory, or set of constraints when no interpretation or assignment can make all statements true simultaneously. In propositional logic, this means there is no truth assignment to the variables that renders the formula true. In first-order logic, a theory is unsatisfiable if it has no model, i.e., no structure in which all sentences of the theory hold.

An elementary example is the conjunction p ∧ ¬p, which cannot be true under any assignment, and is therefore unsatisfiable. By contrast, a formula is satisfiable if at least one assignment makes it true. The concept is central to logic, mathematics, and computer science, where researchers study the boundary between satisfiable and unsatisfiable formulas and theories.

In computational logic, the decision problem UNSAT asks whether a given propositional formula is unsatisfiable. This problem is the complement of the SAT problem (satisfiability) and is co-NP-complete, assuming standard complexity assumptions. Practical methods for proving unsatisfiability include refutation systems such as resolution, which derive an empty clause from a set of clauses, thereby certifying inconsistency.

Unsatisfiability also arises in constraint satisfaction, automated reasoning, and knowledge representation. A related notion is an unsatisfiable core, a minimal subset of constraints that is itself unsatisfiable, useful for debugging and explanation. While unsatisfiable cases have no global solution, studying them helps in understanding the structure of problems and in developing algorithms that detect inconsistencies efficiently.