[Cryptominisat-devel] [Off-topic] New project: cnf-utils

Vegard Nossum vegard.nossum at gmail.com
Mar 18 Jan 00:38:30 CET 2011


Hi,

Sorry in advance for a slightly off-topic post. I just wanted to let
you know that I've started a new project, cnf-utils, which aims to
implement a set of command-line tools for the manipulation of DIMACS
CNF files in a similar manner to the traditional UNIX text-file
utilities (sort, grep, etc.). So far, I have included these programs:
cnf-cat, cnf-clause, cnf-grep, cnf-pack, cnf-propagate,
cnf-shuffle-clauses, cnf-shuffle-literals, cnf-shuffle-variables,
cnf-sort-clauses, cnf-sort-literals, and cnf-stat. A brief description
and usage example of each (and, of course, also the code itself) can
be found here:

http://github.com/vegard/cnf-utils

Most of the commands take CNF as input and produce CNF as output, so
one could build chains of commands using pipes, e.g.:

$ cnf-grep 5192 test.cnf | cnf-pack | cnf-propagate |
cnf-sort-literals | cnf-sort-clauses
p cnf 6 10
-6 3 0
-5 -4 -3 0
-5 3 4 0
-4 3 5 0
-3 -2 -1 0
[...]

The result can even be piped directly to cryptominisat. I'm not sure
exactly how useful that is in practice yet, though, but it can be done
;-)

This is very much a work in progress, but I figured that I can't be
the only one who ever needs these things and that others might be
interested too. My to-do list contains: a tool for removing duplicate
or tautological clauses, a tool for carrying out resolution on
specific literals, a more robust CNF parser, more knobs to cnf-grep,
more (possibly useful ;-)) statistics to cnf-stat, and other things,
which I will probably implement as the need arises. Patches are always
welcome, however :-)


Vegard



More information about the Cryptominisat-devel mailing list