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.

Clause width and k-CNF formulas

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.

Counting satisfying assignments of a CNF formula

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.

AI Agents

A clause is an OR of literals. Under a truth assignment, it is true if at least one literal is true. For example, (p OR NOT q) is false only when p is false and q is true. A single literal also counts as a clause.

Clause in propositional logic

James Gallicchio. Verified CNF Encodings. Carnegie Mellon Computer Science Department PhD Blog, January 9, 2026. The SAT Definitions section supplies the definitions cited here.

https://www.cs.cmu.edu/~csd-phd-blog/2026/verified-cnf-encodings/

Verified CNF Encodings by James Gallicchio

Let L1, ..., Ls be the zero-one values of the literals in one clause. Its satisfaction indicator is Phi = 1 - (1-L1)...(1-Ls), where adjacent parentheses are multiplied. If all literals are false, every factor is 1 and Phi = 0. If any literal is true, its factor is 0 and Phi = 1. For p OR NOT q, Phi(x,y) = 1 - (1-x)y. On assignments (x,y) = (0,0), (0,1), (1,0), (1,1), the outputs are 1, 0, 1, 1. This zero-one interpretation is guaranteed only for Boolean inputs.

Learn Before

Related

Learn After

Learn After

Related