Satisfying assignment ($v\models F$)

A satisfying assignment is a complete Boolean valuation $v$ for which a Boolean formula $F$ has truth value one, written $v\models F$. The notation describes a relation between the Boolean valuation and the Boolean formula. For the example in Boolean satisfiability problem, $(0,1,0)$ is a model of a Boolean formula $F$, whereas $(0,0,0)$ is not. SAT asks for existence of at least one satisfying assignment, rather than for every Boolean valuation to work; the latter condition makes $F$ a tautology.

For each $0\le k\le 2^n$, a propositional formula over $n$ specified variables can have exactly $k$ satisfying assignments and length $O(n^2)$. For $0<k<2^n$, interpret a Boolean valuation as the binary number $x_1\cdots x_n$ and test whether it is less than $k=b_1\cdots b_n$.

For every position $i$ with $b_i=1$, use a conjunction asserting that all earlier bits equal $b_j$ and $x_i=0$, leaving later bits unrestricted. Take the disjunction of these terms. Each satisfying assignment has a unique first differing position, so the terms are disjoint, and their counts sum to ${\sum }_{i:b_i=1}{2}^{n-i}=k$. Their combined length is $O(1+2+\cdots +n)=O(n^2)$. Use logical falsity and logical truth at the two endpoints. The count is over all $n$ variables, including those absent from an individual term or from the whole formula.

For a CNF input with $n$ Boolean variables, $m$ Boolean clauses, and $L$ Boolean literal occurrences, first check that the supplied Boolean valuation gives each input Boolean variable exactly one truth value. Evaluate each Boolean literal by lookup or logical negation, each Boolean clause by logical disjunction, and the Boolean formula by logical conjunction. Indexed Boolean variables and constant-cost lookups give an $O(n+m+L)$ operation count; with a finite binary string encoding the check still takes polynomial time. Thus a satisfying assignment is a certificate in computational complexity for SAT, proving that SAT belongs to NP. Finding it by exhaustive checking can require $2^n$ candidate Boolean valuations; this enumeration cost is not a lower bound on every possible SAT algorithm.^[ref]