# How is verifying whether an assignment satisfies a boolean formula possible in polynomial time?

How can I prove that I can verify whether a boolean assignment of variables $a$ satisfies some boolean formmula $\phi$ in polynomial time?

I know that we can just plug the boolean assignment into the formula, but this seems to be a very high-level description, and I am not sure that it is a reliable one since we must simplify the formula.

Let $\varphi$ a boolean formula and $a : X_\varphi \to \{0,1\}$ an assignment of all variables that occur in $\varphi$. Now we define the evaluation function $\operatorname{eval}_a$ on variable-free boolean expressions in the following way:
\qquad \begin{align} \operatorname{eval}_a(\text{true}) &= 1 \\ \operatorname{eval}_a(\text{false}) &= 0 \\ \operatorname{eval}_a(x) &= a(x) \\ \operatorname{eval}_a(\lnot \varphi) &= 1 - \operatorname{eval}_a(\varphi) \\ \operatorname{eval}_a(\varphi \land \psi) &= \operatorname{eval}_a(\varphi) \cdot \operatorname{eval}_a(\psi) \\ \operatorname{eval}_a(\varphi \lor \psi) &= \max(\operatorname{eval}_a(\varphi), \operatorname{eval}_a(\psi)) \\ & \vdots \end{align}
Clearly, $\operatorname{eval}_a(\varphi) = 1$ if and only if $a(\varphi) \mathop{|\!\!\!==\!\!\!|} \text{true}$ (here, $a$ is continued on $\varphi$ in a syntactical manner: it replaces all variable occurrences $x$ in $\varphi$ with $a(x)$). If in doubt, perform a structural induction along the inductive definition of boolean formulae. Furthermore, $\operatorname{eval}_a$ performs about one operation per operator and literal; thus it runs in time $O(|\langle \varphi \rangle|)$.