Boolean Satisfiability (SAT)

SAT asks whether a Boolean formula can be made true by some assignment of true and false to its variables.

The problem

Given a Boolean formula built from variables, AND, OR, and NOT, the satisfiability problem asks: is there an assignment of true/false to the variables that makes the whole formula true? If yes, the formula is satisfiable; if no assignment works, it is unsatisfiable.

Conjunctive normal form

SAT is usually studied with formulas in conjunctive normal form: an AND of clauses, each clause an OR of literals (variables or their negations). The formula is true only when every clause has at least one true literal. 3-SAT restricts every clause to exactly three literals and is still NP-complete.

Why it is hard

With n variables there are 2^n possible assignments. Brute force checks them all, which is exponential. SAT was the first problem proved NP-complete by the Cook-Levin theorem, making it the archetype of computationally hard problems.

The verification asymmetry

Checking a proposed satisfying assignment is trivial: substitute the values and evaluate, in linear time. This gap between easy checking and hard searching is exactly what places SAT in NP and what the P vs NP question is about.

SAT solvers in practice

Despite worst-case hardness, modern SAT solvers handle formulas with millions of variables on real-world instances, using conflict-driven clause learning and clever heuristics. They power hardware verification, planning, and software analysis. The worst case remains exponential, but many practical instances are far from worst case.

A small example

The formula (A OR B) AND (NOT A OR C) AND (NOT B OR NOT C) is satisfiable: set A true, B false, C true, and every clause has a true literal. Adding the clause (NOT A OR NOT C) would make this assignment fail, and checking whether any assignment still works is the search that SAT solvers automate.