kSAT

k-SAT is a decision problem in propositional logic and computational complexity concerning boolean formulas in conjunctive normal form (CNF) where each clause contains exactly k literals. The input specifies a set of boolean variables and a conjunction of disjunctions of k literals, and the question is whether there exists a truth assignment to the variables that makes the entire conjunction true.

For k = 2, the problem is known as 2-SAT and is solvable in polynomial time, with linear-time algorithms based on implication graphs and strongly connected components. For any k ≥ 3, k-SAT is NP-complete; in particular, 3-SAT is NP-complete, and this hardness extends to all higher k through reductions. This means that, unless P = NP, no polynomial-time algorithm is known for general k-SAT.

In practice, solving k-SAT instances relies on a range of algorithmic approaches. DPLL-based backtracking solvers perform systematic search with constraint propagation, while modern SAT solvers incorporate heuristics, learning, and various optimizations. Local search methods, such as WalkSAT, attempt to find satisfying assignments by iteratively flipping variables to reduce clause violations.

Random k-SAT studies the satisfiability of formulas generated by choosing clauses uniformly at random. A phase transition is observed: as the clause-to-variable ratio α increases, instances transition from likely satisfiable to likely unsatisfiable. For 3-SAT, this threshold is around αc ≈ 4.267; for larger k, αc grows approximately as 2^k ln 2.

Applications of k-SAT include hardware and software verification, planning, and various AI problems. Variants and related problems include monotone k-SAT (no negated literals) and problems focusing on approximate or probabilistic satisfiability.