[isabelle-dev] NEWS: new internal proof-producing SAT solver
makarius at sketis.net
Wed May 7 15:41:31 CEST 2014
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
More information about the isabelle-dev