[isabelle-dev] AFP: PAPP_Impossibility not terminating

[Manuel Eberl]

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 
much.

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.

Manuel


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? 
> https://isabelle-dev.sketis.net/source/isabelle/browse/default/src/HOL/Tools/sat.ML$348
>
>
>> 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.
>
>
>     Makarius
>