Satisfiability
The problem of determining if there exists an interpretation that satisfies a given logical formula.
Satisfiability, often associated with the SAT problem, is a fundamental concept in AI and theoretical computer science involving the determination of whether a given Boolean formula can be made true by assigning appropriate truth values to variables. Its significance lies in its NP-completeness, where even slight variations in problem constraints can transition it from trivially solvable to computationally intractable. Advanced AI techniques often leverage satisfiability for tasks such as constraint satisfaction problems, optimization, and automated reasoning. SAT solvers, developed to tackle satisfiability problems, have become instrumental in software and hardware verification, planning, and other domains requiring rigorous proof of correctness or optimality.
The concept of satisfiability dates back to classic logic studies but gained prominence in computer science with Stephen Cook's seminal paper in 1971, which introduced the notion of NP-completeness. This marked a turning point, highlighting the complexity and broad applicability of the problem within computational theory.
Key contributors to the development of satisfiability include Stephen Cook, whose NP-completeness theory has shaped modern computational complexity, and Martin Davis and Hilary Putnam, who, alongside Davis' student, George Logemann, formulated the DPLL algorithm, a cornerstone in SAT solving and automated theorem proving.