John Threepwood
Reputation
Top tag
Next privilege 250 Rep.
 Jul4 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. Jul4 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. Jul4 awarded Editor Jul4 revised Resolution on 3-SAT instance yields in polynomial many resolvents edited body Jul4 asked Resolution on 3-SAT instance yields in polynomial many resolvents Jul3 awarded Critic Jul3 asked Linear Arithmetic - why calling it linear? Apr9 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. Apr9 accepted How to derive a closed form of a simple recursion? Apr9 asked How to derive a closed form of a simple recursion? Jan29 awarded Scholar Jan29 accepted How to prove correctness of CNF transformation? Jan29 comment How to prove correctness of CNF transformation? Thank you, that helped a lot. Dec17 awarded Student Dec17 asked How to prove correctness of CNF transformation? Aug9 awarded Autobiographer Jul21 awarded Supporter