Fine-grained complexity of 3-CNF formula evaluation It's well known that 3-SAT is in NP, which means that one can evaluate a 3-CNF formula in polynomial time. However, I was wondering what the tightest upper bound is for formula verification, expressed in big-O notation or some other way.

My best guess is that 3-CNF formulas can be verified in linear time in the number of clauses. Each clause has two disjunctions and up to three negations, which should each require one step to evaluate. If you count replacing a literal with its assigned value as a step, that gives you at most 8 steps per clause. Then, once all the clauses are evaluated, you should need [# of clauses] - 1 steps to compute all the conjunctions between them. So with $x$ clauses, that's at most $8x + x - 1 = 9x - 1$ steps total, which is $O(x)$.

Obviously, if I'm wrong about that, please let me know, and if there are even better time bounds (either theoretical or practical), I would love to hear about those as well.
Yes, you are correct.  Your analysis is fine.  It takes linear time.

It's also easy to see that it's not possible to do better than linear time: any algorithm will have to read the entire input (in the worst case), which itself takes linear time.