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

boehmes at in.tum.de boehmes at in.tum.de
Thu May 1 23:24:48 CEST 2014

* 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.

More information about the isabelle-dev mailing list