What is the Boolean satisfiability problem?

What is the Boolean satisfiability problem?

The Boolean satisfiability problem, often referred to as SAT or Boolean SAT, is a fundamental decision problem in computer science and logic. It involves determining if there exists an interpretation that satisfies a given Boolean formula. In other words, it checks whether the variables of a given Boolean formula can be consistently replaced by the values TRUE or FALSE in such a way that the formula evaluates to TRUE. If this is possible, the formula is called satisfiable. If no such assignment exists, the formula is unsatisfiable.

A Boolean formula is built from variables and operators AND (conjunction, denoted by ∧), OR (disjunction, ∨), NOT (negation, ¬), and parentheses. The Boolean satisfiability problem is of central importance in many areas of computer science, including artificial intelligence, model checking, and automatic theorem proving.

SAT solvers are algorithms that establish whether a Boolean expression is satisfiable. They take a Boolean logic formula as input and return whether the formula is satisfiable or not. SAT solvers have practical applications in various fields, such as finding the set of compatible package versions in Python's conda, formal model checking, formal verification of pipelined microprocessors, automatic test pattern generation, routing of FPGAs, planning, and scheduling problems.

The Boolean satisfiability problem is known to be NP-complete, as established by the Cook-Levin theorem. This means that no polynomial-time algorithm is known for solving it in the worst case. Despite this, efficient and scalable algorithms for SAT have been developed, capable of handling large problem instances.