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

Mate Soos soos.mate at gmail.com
Mar 18 Jan 11:16:20 CET 2011

Hash: SHA1

Hi Vegard,

On 01/18/2011 12:38 AM, Vegard Nossum wrote:
> 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 :-)

This sounds awesome :) You should write a small news story to:
www.satlive.org. I am sure the research community would highly
appreciate this work!

By the way, now that you are talking about this, I have an idea. What if
CryptoMiniSat could be used as part of this toolchain in the following
manner. CryptoMS takes as input a file from e.g. stdin, then does some
restarts, then outputs the changed file (obtainable at the moment
through --dumporig=FILENAME) to stdout. Then, this pipe-thing could work
very well, right? I might just implement this feature, actually. This
could have some interesting properties. For example, if you write a tool
"remove-set-vars" that would remove variables that are already set from
the CNF and reuse those variables (i.e. "1 0\n2 3 0\n2 -3\n" would
become "1 2 0\n1 -2\n"), then this would be nice in terms of memory
usage. Memory is typically allocated for every variable, regardless if
it is used or not. This can be alleviated by lingeling-type
programming-acrobatism, but a pipe-based-toolchain could do this
automagically, *much* more cleanly.

Again, great work!



- -- 
Mate Soos
Security Research Labs
Version: GnuPG v1.4.10 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org/


More information about the Cryptominisat-devel mailing list