[isabelle-dev] AFP: PAPP_Impossibility not terminating
manuel at pruvisto.org
Tue Apr 18 11:37:33 CEST 2023
I do know of that one as well, but it uses some old and rather obscure
SAT solvers (with some custom patches even, I think) and a different
proof format as well (that isn't really used by any modern SAT solvers,
I think). Also, as I recall there was only one suppoerted SAT solver
that I managed to find, compile, and run. And then the approach didn't
really scale to my kind of setting. In earlier versions of the same
entry I had SAT instances with 20 million clauses, which was simply too
My implementation uses the DRAT format, which seems to be a kind of
de-facto standard in the SAT community nowadays.
I did take some inspiration from the implementation you linked though. I
don't think they had to do any of the low-level fine-tuning with hyps
that I had to do though.
On 18/04/2023 11:04, Makarius wrote:
> On 18/04/2023 10:07, Manuel Eberl wrote:
>> I did notice at the time that the vast majority of the time was spent
>> in taking the union of the hyps of the different theorems being
>> combined, so I made sure that when I create the theorems, they all
>> have pointer-equal hyps, which sped things up phenomenally.
> Did you re-invent this yourself, or did you see it here?
>> I should also still have a few smaller example applications of that
>> SAT solver lying around that one could use; there the difference
>> between the old and the new version would perhaps not be "2 minutes"
>> vs "non-termination" but rather something like "almost instant" and
>> "half a minute" or so, which may make debugging less painful.
> It would be great to have such small benchmark examples. Please send
> them to me privately.
More information about the isabelle-dev