2 ms·
When he says "sub-expressions", he means it in the program-code sense. Really, he's saying: why don't we try to refactor the proof? And, since it's so large, w
by scott_s 13y ago
When he says "sub-expressions", he means it in the program-code sense. Really, he's saying: why don't we try to refactor the proof?
And, since it's so large, we probably can't do it by hand. So we would need to develop techniques to do it automatically. (Or semi-automatically.)
- ColinWright 13y agoBut the proof isn't large, just the output of the search. Assuming my understanding of the problem and the result are correct, the reporting on this is so poor as to be meaningless and misleading. As such, the comments are well-meaning, but (to me) seem meaningless. Of course, my "understanding" may be completely wrong.
- scott_s 13y agoLet's avoid the use of the word "proof", which I address above. Is it possible to do any analysis of the output of the SAT solver, the certificate, to gain any insight into the problem? That's what the poster was asking.
- ColinWright 13y agoUsing that context, I have no knowledge of the form the certificate takes, so I can't venture an opinion at all in this case. I suspect the answer is "no", but that's just on general principles.