Satisfiability Solver (SAT)

Most SAT (satisfiability) solvers accept a formula in CNF form. SAT solvers are used as an engine for all sorts of problems in computer science from circuit layout to AI.

SAT is an NP-Complete problem.

2-SAT is a very specific version, where each clause is a disjunction of two variables (these variables be negated).

There is an algorithm for converting any propositional logic formula into CNF in linear time by adding extra variables, called the Tseytin Transformation.