0
$\begingroup$

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.

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

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.