Re:The undeserved status of the pigeon-hole principle (1991)
by 53x15 on Saturday July 04, 2020 @08:52PM
(#23735912)
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.
[ Parent
| on HN ]
There are no comments on this comment yet.