[isabelle-dev] isabelle dimacs2hol
tjark.weber at it.uu.se
Tue Jul 9 12:32:02 CEST 2013
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.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 836 bytes
Desc: This is a digitally signed message part
More information about the isabelle-dev