On Mon, 2013-07-08 at 11:09 +0200, Makarius wrote: > Does the Isabelle tool "dimacs2hol" from 2004 still have a purpose? > > The DIMACS CNF format appears to be an old proposal for SAT, predating > newer things like SMT-LIB. So this looks like a candidate for deletion.
DIMACS CNF remains the standard input format for SAT solvers. Describing it as outdated wouldn't do justice to the SAT research community. I used the tool in order to benchmark the Isabelle/HOL integration of SAT solvers. This requires a full round trip, i.e., not just export of propositional Isabelle/HOL formulae into DIMACS CNF, but also import of DIMACS CNF benchmarks into Isabelle/HOL. I doubt the tool has seen much usage beyond that. Personally, I am not opposed to its deletion. Best, Tjark
signature.asc
Description: This is a digitally signed message part
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
