[isabelle-dev] isabelle dimacs2hol

[Tjark Weber]

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
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 836 bytes
Desc: This is a digitally signed message part
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20130709/4a22fb47/attachment.sig>