3SAT

3-SAT is a decision problem in computational complexity theory. An instance consists of a Boolean formula in conjunctive normal form, where the formula is an AND of clauses, each clause being a disjunction of exactly three literals (variables or their negations). The question is whether there exists an assignment of truth values to the variables that makes the entire formula true.

3-SAT is a canonical NP-complete problem. It is in NP because a candidate assignment can be verified to satisfy all clauses in time linear in the input size. It is NP-hard because any instance of SAT can be transformed in polynomial time into an equivalent 3-CNF instance: clauses longer than three literals are replaced by a conjunction of new clauses introducing fresh variables, and clauses with fewer than three literals can be augmented to three by repetition or by adding new literals. Therefore, a polynomial-time algorithm for 3-SAT would imply a polynomial-time algorithm for SAT, and hence P = NP.

3-SAT plays a central role in complexity theory and in reductions proving the NP-completeness of many other problems. Related problems include monotone 3-SAT, where clauses contain only positive or only negated literals, and k-SAT in general (clauses with k literals). Among these, 2-SAT is solvable in polynomial time, while k-SAT for k ≥ 3 is NP-complete.

In practice, 3-SAT formulations appear in logic synthesis, formal verification, constraint satisfaction, and various artificial intelligence tasks, where it models the requirement that a set of ternary constraints can be simultaneously satisfied.