130 reputation
6
bio website stackoverflow.com
location Europe
age 28
visits member for 2 years, 2 months
seen Jul 7 '13 at 10:54

Interests: Linux, Scala, Java, C/C++, Databases, Logic, Mathematics.


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