[isabelle-dev] isabelle dimacs2hol
makarius at sketis.net
Wed Jul 10 13:18:08 CEST 2013
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
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?
More information about the isabelle-dev