[isabelle-dev] AFP: PAPP_Impossibility not terminating

[Manuel Eberl]

Oh dear, that is unfortunate.

PAPP_Impossibility is probably one of the most brutal benchmarks of 
low-level theorem operations we have. The SAT prover in that entry 
essentially proves a large number of clauses (a few hundred thousand) 
and then starts plugging them together in a specific, externally 
determined way until it derives the empty clause. The first part is 
quite fast and still works without any problems. The really 
resource-intensive bit is the second part, and this is the part that 
doesn't terminate anymore (or more probably, takes much longer than it 
did before).

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.

Hope that helps. If you have any questions about the code, I'll be happy 
to answer them. 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.

Manuel


On 17/04/2023 23:38, Makarius wrote:
> On 17/04/2023 14:49, Makarius wrote:
>> We have a problem with PAPP_Impossibility for quite some time.
>>
>> I am presently running a bisection to see better where it actually 
>> happens: presently the interval is Isabelle/f5aca3ed1adb .. 
>> 69ee23f83884 based on 
>> https://isabelle.sketis.net/devel/build_status/AFP/PAPP_Impossibility.csv
>>
>> Stay tuned ...
>
> The first bad revision is:
> changeset:   77808:b43ee37926a9
> user:        wenzelm
> date:        Mon Apr 10 22:38:18 2023 +0200
> summary:     performance tuning: replace Ord_List by Set();
>
>
> This is a change of the thm hyps field to make applications like 
> PAPP_Impossibility actually faster, but I did not notice that this is 
> such an application, and that it becomes very slow.
>
> Even worse, it is not sufficient to take b43ee37926a9 back, because 
> other changes on top appear to cause similar problems.
>
>
> I need to look more closely into the special SAT prover in 
> PAPP_Impossibility, to see what is really going on.
>
>
>     Makarius
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev