CNF evaluation (satisfiesB) is PolyTimeDecidable

The CNF formula evaluation $V(x,w) = \mathtt{satisfiesB}(\mathtt{decodeAssignment}(w), \mathtt{decodeFormula}(x))$ is polynomial-time decidable.

Given a binary string $x$ encoding a CNF formula $\varphi$ and a certificate $w$ encoding a truth assignment $\alpha$, this predicate evaluates whether $\alpha$ satisfies $\varphi$. The evaluation proceeds by:

1. Decoding $x$ into the formula $\varphi = c_1 \wedge \cdots \wedge c_m$ (a list of clauses, each a list of literals).
2. Decoding $w$ into the assignment $\alpha$ (the $n$-th bit of $w$ gives the truth value of variable $n$).
3. For each clause $c_i$, checking whether at least one literal evaluates to true under $\alpha$.
4. Accepting if and only if all clauses are satisfied.

Since $|\varphi|$ (total number of literal occurrences) is bounded by $|x|$ and each variable lookup into $w$ takes $O(|w|)$ time, the evaluation runs in $O(|x| \cdot |w|) \subseteq O((|x|+|w|)^2)$ steps, which is polynomial.