Satisfiability is the problem of determining whether there exists an assignment of values to variables that makes a logical formula true, most prominently the Boolean satisfiability problem (SAT). SAT is the canonical NP-complete problem, and modern SAT solvers can decide formulas with millions of variables despite this worst-case hardness. Satisfiability provides a unifying computational substrate for verification, planning, scheduling and many forms of automated reasoning.
Overview
- Decides whether a logical formula can be made true by some variable assignment.
- Boolean SAT is the canonical NP-complete decision problem.
- Practical solvers handle very large instances via conflict-driven clause learning.
Key aspects
- Conjunctive normal form encoding of constraints.
- Conflict-driven clause learning and backtracking search.
- Decision versus optimisation framings of feasibility.
- Reductions that encode diverse problems as SAT instances.
Applications
- Hardware and software formal verification.
- Automated planning and scheduling.
- Combinatorial design and configuration.
- Encoding for theorem proving and AI reasoning.