Search All of the Math Forum:
Views expressed in these public forums are not endorsed by
Drexel University or The Math Forum.


quasi
Posts:
10,232
Registered:
7/15/05


Re: Boolean satisfiability
Posted:
Dec 12, 2013 6:13 AM


Steeve Beroard wrote: > >So you mean by stating that "any unsatisfiable CNF is equivalent >to a CNF with all combination of variables and their negation" > s to give a particular method of resolution?
Not exactly.
In general, the new CNF will have exponential size relative to the size of the original CNF, so any particular method used to determine its satisfiability will have exponential time cost relative to the size of the original CNF (not necessarily exponential relative to its own size, but that's irrelevant).
Rather than talk about it abstractly, take an actual example so you can compare the sizes of the two CNFs.
quasi



