[isabelle-dev] AFP: PAPP_Impossibility not terminating
manuel at pruvisto.org
Tue Apr 18 10:07:08 CEST 2023
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
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.
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
>> 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.
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
More information about the isabelle-dev