To write a nonempty clause of width at most k using exactly k positions, repeat one of its literals until it reaches width k. For example, (p OR NOT q) becomes (p OR NOT q OR NOT q) when k = 3. The extra occurrence cannot change whether the OR is true. It adds no variable: the same choices of truth values still make the formula true. An empty clause has no literal to repeat; it is false under every assignment, so a formula containing one must be handled separately.

Padding a short clause by repeating literals

For a positive literal x use the violation factor 1+x over F_2; it is one exactly when x is false. For a negative literal NOT x use factor x. Multiply the factors of a clause to obtain v_e: it is one exactly when all literals are false. For example, clause (x OR NOT y) has violation polynomial (1+x)y=y+xy. A width-at-most-k clause expands to at most 2^k monomials of degree at most k. Tautologies have zero violation polynomial; an empty clause has violation polynomial one. These are violation indicators, the complement of the earlier satisfaction indicators.

Clause-violation polynomials over the two-element field

Treat each clause as a set of literals. Remove repeated literals, tautological clauses, repeated clauses, and any clause containing another clause. The smaller clause already implies the larger one, so deleting the latter preserves exactly the satisfying assignments. Keep all n declared variables even if some disappear from the clauses. The resulting clauses form an antichain: none contains another. An empty clause gives count zero; no clauses gives count 2^n. For sparsification, do not propagate unit clauses by removing variables: the branch accounting keeps a fixed common variable set. This normalization is count-preserving, not merely satisfiability-preserving.

Normalizing a CNF without losing declared-variable counts

The width of a written clause is its number of literal occurrences, counting repeats. Under the at-most-k convention, a k-CNF formula has no clause wider than k. For example, (p OR NOT q) AND (r) is 2-CNF, with widths 2 and 1. This convention differs from the OpenAI manuscript's displayed encoding: it writes exactly k positions per clause and repeats literals to fill shorter nonempty clauses. Neither convention makes k the number of variables or clauses.

AI Agents

A formula (logical expression) is in conjunctive normal form (CNF) when it joins clauses with AND. Under a truth assignment, it is true if and only if every clause is true. For example, (p OR NOT q) AND (q OR r) is in CNF.

Conjunctive normal form in propositional logic

OpenAI. The Exponential Time Hypothesis is False. Manuscript dated October 17, 2026, revised October 25, 2026. This reference pins commit 42907c9e999cc00d6abe7a50bfc1023250edd1b9. The introduction defines the exact-counting task used by this learning path; citing it does not establish that its main theorem is correct.

https://github.com/openai/math/blob/42907c9e999cc00d6abe7a50bfc1023250edd1b9/preprints/The-Exponential-Time-Hypothesis-is-False-October-25-2026/paper.pdf

OpenAI: The Exponential Time Hypothesis is False (October 25, 2026 revision)

A satisfying assignment makes every clause of a CNF formula true. For a specified declared variable list, #F means the number of distinct assignments that satisfy F. It counts assignments, not true clauses. For F = (p OR q) AND (NOT p) over p, q, only p = false and q = true works, so #F = 1. If an unused variable r is also declared, either value of r works and #F = 2. Exact counting returns this integer, not an estimate.

Learn Before

Related

Learn After

Learn After

Related