A CNF formula has $n$ indexed Boolean variables. A literal is a variable and a polarity; a clause is a disjunction of literals and a formula is a conjunction of clauses. Width at most $k$ means at most $k$ literals in each clause. The empty conjunction is true and an empty clause is false.

The binary encoding gives $n$, the number of clauses, each clause length, and each literal's index and sign, in that order. Natural numbers use unary followed by a zero. This self-delimiting encoding has polynomial length in $n$ and the usual explicit formula size. Polynomial factors in its full length are retained in the SAT running-time bounds; the exponential parameter is $n$, not the number of clauses or encoded bits. Unused indexed variables, repeated literals and repeated clauses are allowed.