Cheap and Secure Web Hosting Provider : See Now

[Solved]: Solving SAT using tableau calculus

, , No Comments
Problem Detail: 

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)?

Asked By : lukstei

Answered By : Kyle Jones

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.

Best Answer from StackOverflow

Question Source :

3.2K people like this

 Download Related Notes/Documents


Post a Comment

Let us know your responses and feedback