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

Mate Soos soos.mate at gmail.com
Mar 18 Jan 11:29:28 CET 2011

Hash: SHA1

Hi Again,

On 01/18/2011 11:16 AM, Mate Soos wrote:
> 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.

Just thought through that you could dump the variable mapping to a
temporary file, then re-read that to extend the found solution to the
original problem's solutions, again through pipes, but then options
would be needed:

cat problem.cnf | cnf-propagate | cnf-remove-set-vars --extdata=tmpfile
| cryptominisat --dumporig=stdout | cnf-remove-set-vars --extend
- --extdata=tmpfile

(note: every info printed by SAT solvers is standardised to start with a
"c" in front, and the solution is clearly parsable with "s" in front,
and "v" in front of the satisfying assignment)

That command-line already sounds fun to me, but I am sure you can come
up with a cleaner syntax, judging from the work you have already done ;)



PS: Have you fuzz-tested your programs? Maybe a fuzz-tester such as that
by Armin Biere would be helpful.

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