|
|
|
|
|
|
by 53x15
2169 days ago
|
|
|
I think neel_k was referring to the fact that when a DPLL or CDCL solver concludes UNSAT you can take the trace its backtracking activity and rewrite it from the bottom up as a resolution refutation. So in this sense the solvers are finding resolution proofs. |
|
|