[isabelle-dev] isabelle dimacs2hol

[Tjark Weber]

On Thu, 2013-08-01 at 16:41 +0200, Makarius wrote:
> On Wed, 10 Jul 2013, Tjark Weber wrote:
> Looking superficially at 
> http://isabelle.in.tum.de/repos/isabelle/file/b7a83845bc93/src/HOL/ex/SAT_Examples.thy 
> I wonder if this actually works right now.

Good question. One issue is that the theory requires a SAT solver
(zChaff or MiniSat) to work properly. These days, one could probably be
shipped as a component, but I wonder if that's worth it. People just
don't seem to use Isabelle to prove large propositional tautologies.

I still think that encodings of decidable problems into propositional
logic could probably be just as beneficial in theorem proving as
they've been in many other domains. But regarding the future of "sat",
I am rather undecided at this point.

Best,
Tjark