On Tue, 9 Jul 2013, Tjark Weber wrote:
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.
You have a link there from 2004, pointing to a paper from 1993, which
seems to predate what they call the "official" DIMACS CNF format. (On Mac
OS X I even failed to open that DVI file on the spot.)
So at first sight it looks unmaintained, and the usual reaction is either
to brush it up, or keep the history in the history (via "hg rm").
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 vaguely remember a private discussion about the performance of inner
syntax parsing in this respect. For a realistic import one would bypass
that anyway, i.e. not generate source files to parse them again, but read
things directly via some Isabelle/ML functions. Incidently, this recent
thread on isabelle-users
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2013-May/msg00118.html
shows that the inner syntax parser is not the only bottle-neck, due to so
many add-on layers in the term-check phase (and repeated term certify).
Anyway, shall I do the "hg rm" of the two relevant files now?
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
