[isabelle-dev] NEWS: new internal proof-producing SAT solver

[Tjark Weber]

On Wed, 2014-05-07 at 15:41 +0200, Makarius wrote:
> How about ~~/src/HOL/ex/Sudoko.thy?  It formally depends on ZCHAFF_HOME, 
> so it is rarely run in practice.  Does it now make sense to remove that 
> condition in the ROOT file? What is tested in this theory anyway?  The 
> 'refute' / 'oops' sequences seem to be relatively soft in their 
> requirements.

The theory demonstrates how Isabelle can be used as an efficient Sudoku
solver.

zChaff is still clearly superior to the internal solver (< 1s vs. > 60s
for some problems in this theory). But the worst that should happen
with the internal solver are timeouts within Refute. I suppose if you
don't mind burning a few cycles, the condition in ROOT could be
dropped.

Moreover, it is merely a historic accident that the theory is based on
Refute. I tried switching to Nitpick just now, but I ran into a minor
issue that I'll raise in a separate thread.

Best,
Tjark