Graph Theory37 sections · 1633 units
Open in Course

Vocabulary - Clause

(OR of literals)

A clause is a constraint formed by ORing literals together. A literal is a variable or its negation. Each clause must evaluate to true. "x OR y" is a clause with two literals. "NOT x OR NOT y OR z" is a clause with three literals. In 22-SAT, every clause has exactly two literals.

Clauses are the building blocks of SAT formulas. They express constraints that must all be true simultaneously. A formula is the AND of all its clauses, so every single clause must be satisfied.