On Thu, 1 May 2014, boeh...@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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
