I've learned about tableau calculus which is a decision procedure solving the problem of satisfiability of a first order logic formula. Now I'm wondering why this technique can't be used to solve the satisfiability problem (SAT)?
$\begingroup$
$\endgroup$
Add a comment
|
1 Answer
$\begingroup$
$\endgroup$
It can be, but the solution process is equivalent to converting a CNF formula to DNF, which is NP-hard. You will at worst end up exploring an exponential number of disjunction branches.
answered Jun 3, 2014 at 23:51