John Threepwood
Reputation
Top tag
Next privilege 250 Rep.
 Oct 21 awarded Popular Question Apr 29 accepted Resolution on 3-SAT instance yields in polynomial many resolvents Apr 29 comment Resolution on 3-SAT instance yields in polynomial many resolvents Thank you for your answer. That was my mistake, thank you. Jul 4 comment Resolution on 3-SAT instance yields in polynomial many resolvents @EricTressler Thank you for the reply. Resolution is refutation complete: A SAT instance is satisfiable iff the empty clause can not be derived as resolvent. So building all resolvents is sufficient to test for satisfiability. Jul 4 comment Resolution on 3-SAT instance yields in polynomial many resolvents @EricTressler Roughly: All 1-Literal clauses: $n$ many. All 2-Literal clauses $n^2$ many. All 3-Literal clauses $n^3$ many. Calculate all clauses (polynomial many) and check for an empty clause. Jul 4 awarded Editor Jul 4 revised Resolution on 3-SAT instance yields in polynomial many resolvents edited body Jul 4 asked Resolution on 3-SAT instance yields in polynomial many resolvents Jul 3 awarded Critic Jul 3 asked Linear Arithmetic - why calling it linear? Apr 9 comment How to derive a closed form of a simple recursion? Thank you for the detailed procedure of finding the closed form. Very helpful. Sadly, I can not approve two answers as correct. Apr 9 accepted How to derive a closed form of a simple recursion? Apr 9 asked How to derive a closed form of a simple recursion? Jan 29 awarded Scholar Jan 29 accepted How to prove correctness of CNF transformation? Jan 29 comment How to prove correctness of CNF transformation? Thank you, that helped a lot. Dec 17 awarded Student Dec 17 asked How to prove correctness of CNF transformation? Aug 9 awarded Autobiographer Jul 21 awarded Supporter