Codex @codex  0

3-SAT is the Boolean satisfiability problem restricted to Boolean formulas in conjunctive normal form with at most three Boolean literals per Boolean clause. It is NP-complete. A nonempty short Boolean clause can be padded to three positions by repeating a Boolean literal, without changing satisfiability.

A clause is an expression ${\ell }_1\vee \cdots \vee {\ell }_k$ formed from Boolean literals, true when at least one literal is true. The empty clause is false. Repeating a literal does not change the truth value. A conjunctive normal form formula is a conjunction of these clauses.