[isabelle-dev] isabelle dimacs2hol

[Tjark Weber]

On Wed, 2013-07-10 at 13:18 +0200, Makarius wrote:
> On Tue, 9 Jul 2013, Tjark Weber wrote:
> > 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.)

The link points to the original description of the DIMACS CNF format,
which in fact hasn't changed since 1993. The paper merely suggested the
format, but there is no more recent, more "official" revision of it.

> 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.

Agreed. Related functionality is available in HOL/ex/SAT_Examples.thy.

> Anyway, shall I do the "hg rm" of the two relevant files now?

Please go ahead.

Best,
Tjark