SATProblem

SAT problem, or the satisfiability problem, asks whether a given Boolean formula has a truth assignment to its variables that makes the formula evaluate to true. In most formal treatments the input is presented in conjunctive normal form (CNF): a conjunction of clauses, each clause a disjunction of literals (a variable or its negation). For example, the formula (x1 ∨ ¬x2) ∧ (x3 ∨ x4 ∨ ¬x1) is satisfiable if there exists an assignment to x1, x2, x3, x4 that makes both clauses true.

The decision variant of SAT asks only whether such an assignment exists. SAT is the canonical NP-complete problem: the Cook–Levin theorem showed in 1971 that any problem in NP can be reduced in polynomial time to SAT, making it a central problem in computational complexity and a standard tool for proving NP-hardness.

Variants and related problems: 2-SAT, where each clause has at most two literals, can be solved in polynomial time; 3-SAT and more generally k-SAT with k ≥ 3 are NP-complete. Practical SAT instances are often solved with algorithms such as DPLL and modern conflict-driven clause learning (CDCL) solvers, which combine backtracking with clause learning, heuristics, and restarts. Local search methods (e.g., WalkSAT) are also used on hard instances.

Applications: SAT is widely used in formal verification, hardware and software verification, planning and scheduling, constraint solving, and AI. Many combinatorial problems can be encoded as SAT; Max-SAT refers to optimization variants that seek to maximize the number of satisfied clauses.