# 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.

• Note that 3-SAT is explicitly the problem of determining satisfiability; you're mostly talking about formulas in 3-CNF. Edited. – David Richerby Feb 28 '19 at 23:41