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

[Makarius]

On Thu, 1 May 2014, boehmes at in.tum.de wrote:

> * New internal SAT solver "dpll_p" that produces models and proof traces.
>
> This refers to Isabelle/848d507584db. The added SAT solver should be more 
> efficient than the internal SAT solvers "dpll" and "enumerate". Since the 
> solver "dpll_p" produces proof traces, the tactics sat and satx can be 
> applied to prove propositional goals without the need for quick_and_dirty.

Great.  I see more SAT related cleanup coming after that (presently at 
Isabelle/2f73ef9eb272).  It looks like the proof methods "sat" and "satx" 
and the command 'refute' have seen a renaissance.

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.


 	Makarius