Boolean formula

A Boolean formula is a finite expression built from Boolean variables and Boolean operations. A choice of truth values determines its value. The Boolean satisfiability problem asks whether some choice makes it true.

A Boolean formula is in conjunctive normal form when it is a conjunction of Boolean clauses. It is true precisely when every clause is true; an empty conjunction is true. 3-SAT restricts each clause to at most three Boolean literals.

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.

A Boolean literal is a Boolean variable $u$ or its negation $\neg u$. The two literals have opposite truth values. A Boolean clause combines literals, and a Boolean-pair colouring gadget represents a variable and its negation by two vertices with opposite Boolean colours.

A Boolean variable takes one of two truth values. It is an input to a Boolean formula; a Boolean literal uses the variable either positively or negated.