Minisat search graph generation

[soos.mate]

Hi!

I wrote a search graph generation extension to Minisat. It draws the
search graph that Minisat goes through. It is available at:
http://planete.inrialpes.fr/~soos/minisat_graphs/index.html It can be
used to see which parts of the CNF is hard to solve, which clauses are
causing the most propagations/conflicts, it can be used as a tool to
teach how modern SAT solvers work, and it can be used for debugging.

Also, I wrote another patch, that is very specific but it does a very
interesting thing: solves a MaxSAT problem as it were a SAT problem,
with Minisat, and runs *much* faster than normal MaxSAT solvers do.

Have fun!

Mate Soos

[soos.mate]

Hi!

with Minisat, and runs *much* faster than normal MaxSAT solvers do. It
is available at: http://planete.inrialpes.fr/~soos/minisat_errors/index.html

Have fun!

Mate Soos

[Niklas Sörensson]

Nice!

I tried it out. Here's a couple comments:

* If I run it without the -proof-log flag, it crashes with a
segmentation fault. Here's a backtrace:

Program received signal SIGSEGV, Segmentation fault.
0x08049af2 in Logger::document_proof_propagation (this=0xbfbfe430,
lit={x = 1417}, type=4, groups=0xbfafe264) at Logger.C:44
44 fprintf(proof,"node%d -> node%d
[label=\"",history[new_level],uniqueid);
#0 0x08049af2 in Logger::document_proof_propagation (this=0xbfbfe430,
lit={x = 1417}, type=4, groups=0xbfafe264) at Logger.C:44
#1 0x080512c7 in Solver::addClause (this=0xbfbfe38c, ps=@0xbfafe2ec,
group=84, wrong=false) at Solver.C:131
#2 0x0804b4e8 in parse_DIMACS_main<StreamBuffer> (in=@0xbfafe31c,
S=@0xbfbfe38c) at Main.C:180
#3 0x0804b553 in parse_DIMACS (input_stream=0x48301080,
S=@0xbfbfe38c) at Main.C:189
#4 0x0804c68d in main (argc=2, argv=0xbfbfe658) at Main.C:327
(gdb)

Argh, gmail totally messed that up. Well, maybe it's useful anyway :)

* The dot-files generated are not completely correct (according to dot
from Graphviz 2.14.1). For instance:

nik> dot -Tsvg proof0.dot > proof0.svg
Error: proof0.dot:356: syntax error near line 356
nik> tail proof0.dot
node174 [shape=box, label="221"];
node173 -> node174 [label="red. from 4766"];
node175 [shape=box, label="-398"];
node174 -> node175 [label="red. from 4797"];
node176 [shape=box, label="-309"];
node175 -> node176 [label="red. from 4870"];
node177 [shape=box, label="-610"];
node176 -> node177 [label="red. from 4886"];
node178 [shape=box, label="469"];
node177 -> node178 [label="red. from 4913"];

You can see here that the file is missing the closing brace.

From proof1.dot I get a completely different error though:

dot - Graphviz version 2.14.1 (Fri Aug 31 17:49:53 UTC 2007)
nik> dot -Tsvg proof1.dot > proof1.svg
Warning: proof1.dot:15376: string ran past end of line
Warning: proof1.dot:15377: string ran past end of line
Error: proof1.dot:15378: syntax error near line 15378
context: node7637 >>> -> <<< node7638;

nik> tail proof1.dot
node7635 [shape=box, label="427"];
node7634 -> node7635 [label="1422\n"];
node7636 [shape=box, label="-12"];
node7635 -> node7636 [label="1438\n"];
node7637 [shape=box, label="402"];
node7636 -> node7637 [label="1643\n"];
node7638 [shape=doublecircle, label="Re-starting
search"];
node7637 -> node7638;
}

Apperently dot doesn't like that there is a new-line in the string.
Isn't it possible to use \n in the strings instead?

Then, fixing proof1.dot by hand, dot still takes too long to generate
the graph. I guess this is expected in all realistic problems?

Finally, a couple of suggestions/feature requests:

- In the grouping mode, can the groups be specified separately
somehow? Perhaps as a section using DIMACS comment lins (i.e. lines
beginning with "c ")?
- Or even better, can groups be calculated automatically somehow?

Cheers,

/Niklas

[Miguel Ramírez]

Didn't find my notes after all :)

Waiting to see your paper on that

On 9/17/07, soos.mate <soos...@gmail.com> wrote:
>

[Miguel Ramírez]

Argh, pesky laptop mouse.

Just to tell you I hope to see a paper about your approach to solve
MaxSAT soon :)

Miguel Ramírez.

[soos.mate]

On 18 sep, 16:13, "Niklas Sörensson" <nikla...@gmail.com> wrote:
> Nice!
>
> I tried it out. Here's a couple comments:
>
> * If I run it without the -proof-log flag, it crashes with a
> segmentation fault. Here's a backtrace:
>
> Program received signal SIGSEGV, Segmentation fault.
> 0x08049af2 in Logger::document_proof_propagation (this=0xbfbfe430,
> lit={x = 1417}, type=4, groups=0xbfafe264) at Logger.C:44
> 44 fprintf(proof,"node%d -> node%d
> [label=\"",history[new_level],uniqueid);
> #0 0x08049af2 in Logger::document_proof_propagation (this=0xbfbfe430,
> lit={x = 1417}, type=4, groups=0xbfafe264) at Logger.C:44
> #1 0x080512c7 in Solver::addClause (this=0xbfbfe38c, ps=@0xbfafe2ec,
> group=84, wrong=false) at Solver.C:131
> #2 0x0804b4e8 in parse_DIMACS_main<StreamBuffer> (in=@0xbfafe31c,
> S=@0xbfbfe38c) at Main.C:180
> #3 0x0804b553 in parse_DIMACS (input_stream=0x48301080,
> S=@0xbfbfe38c) at Main.C:189
> #4 0x0804c68d in main (argc=2, argv=0xbfbfe658) at Main.C:327
> (gdb)
>
> Argh, gmail totally messed that up. Well, maybe it's useful anyway :)

Thanks, it was useful. I messed up the code where Minisat does
"addClause" and automatically bounds variables (this is a trick you
use that speeds up solving, great idea BTW). It should be OK now.

>
> * The dot-files generated are not completely correct (according to dot
> from Graphviz 2.14.1). For instance:
>
> nik> dot -Tsvg proof0.dot > proof0.svg
> Error: proof0.dot:356: syntax error near line 356
> nik> tail proof0.dot
> node174 [shape=box, label="221"];
> node173 -> node174 [label="red. from 4766"];
> node175 [shape=box, label="-398"];
> node174 -> node175 [label="red. from 4797"];
> node176 [shape=box, label="-309"];
> node175 -> node176 [label="red. from 4870"];
> node177 [shape=box, label="-610"];
> node176 -> node177 [label="red. from 4886"];
> node178 [shape=box, label="469"];
> node177 -> node178 [label="red. from 4913"];
>
> You can see here that the file is missing the closing brace.

proof0.dot was never tested, sorry. Fixed.

>
> From proof1.dot I get a completely different error though:
>
> dot - Graphviz version 2.14.1 (Fri Aug 31 17:49:53 UTC 2007)
> nik> dot -Tsvg proof1.dot > proof1.svg
> Warning: proof1.dot:15376: string ran past end of line
> Warning: proof1.dot:15377: string ran past end of line
> Error: proof1.dot:15378: syntax error near line 15378
> context: node7637 >>> -> <<< node7638;
>
> nik> tail proof1.dot
> node7635 [shape=box, label="427"];
> node7634 -> node7635 [label="1422\n"];
> node7636 [shape=box, label="-12"];
> node7635 -> node7636 [label="1438\n"];
> node7637 [shape=box, label="402"];
> node7636 -> node7637 [label="1643\n"];
> node7638 [shape=doublecircle, label="Re-starting
> search"];
> node7637 -> node7638;
>
> }
>
> Apperently dot doesn't like that there is a new-line in the string.
> Isn't it possible to use \n in the strings instead?

Problem was the new-line after "Re-starting", as you mentioned. Fixed.

>
> Then, fixing proof1.dot by hand, dot still takes too long to generate
> the graph. I guess this is expected in all realistic problems?

Unfortunately, yes. Dot is a very complex program, and the whole thing
could actually be written as SVG directly, since we know the complete
layout of the graph beforehand. However, it would be very difficult to
do, and less extensible+more difficult to debug.

>
> Finally, a couple of suggestions/feature requests:
>
> - In the grouping mode, can the groups be specified separately
> somehow? Perhaps as a section using DIMACS comment lins (i.e. lines
> beginning with "c ")?

Good idea, actually. Done. Groups now must be indicated with a line "c
g=NUM" after the clause.

> - Or even better, can groups be calculated automatically somehow?

I am afraid not. It would be difficult :(. But Minisat+ could be
easily be re-written to have groups, for instance! PS: because of
structural hashing, in the generated CNF, some clauses would need to
belong to more than one group :( Huh, well, that could be implemented,
too... "std::list<uint> goup" is a good candidate to replace the "uint
group" in the Clause declaration. The logging can already take care of
more than one clause doing the propagation (all the clause's groups
will be written on the edge leading to the bounded variable's box).
PS: I needed this multi-group propagation/conflict for my error-
tolerant version of Minisat.

>
> Cheers,
>
> /Niklas

Thanks for all the comments! And thanks for the great Minisat. The
fact that it is open-source (and well-documented) is one of its major
advantages, along with the fact that it is extremely fast :)

PS: New version of patches are on my website. If multi-group clauses
are needed, drop me a line here in the forum, and I will implement it
in the coming weeks.

[Arijit Shaw]

Hi,

Is this extension still available somewhere? The attached links seem broken.

[Mate Soos]

Hi,

The git history is always available, and checking out an old version takes less than 1 minute. Here is a version that I digged up & fixed up (surprisingly little had to be changed) so it compiles on modern compilers:

https://github.com/msoos/cryptominisat/tree/old-cmf-fixed-graphviz

Note that:

• This is a 13 year old version of CryptoMiniSat. It is *strongly* unsupported.
  
• You must run with -proof-log option to generate search trees which the system calls "proofs"
  
• It doesn't actually generate any "proofs", it generates the search tree for each restart. It's kind of the opposite of what a proof is :) Each restart generates a single search tree. You can name the variables/clauses, please check the README
  
• "Proofs" (i.e. restarts' search trees) are output into directory "proofs/" which must be present
  
• The 1st "proof" (ending with "proof0.dot") is always incorrectly formatted (last "}" is missing) except when the solution is found on 1st restart.
  
• It's using the dot description language [1]. I used the "dot" tool from graphviz [2] to draw the graphs
• The DOTs are huge and you will notice that the graphviz tools will die on anything even remotely non-trivial. Get ready to wait a week and stock up on a  terabyte of memory.
  
• Using of "dot" to output to SVG/PNG/etc is explained in many tutorials.
  

Again, all of this is unsupported. Good luck,

Mate

[1] https://en.wikipedia.org/wiki/DOT_%28graph_description_language%29

[2] https://graphviz.org/

--

---
You received this message because you are subscribed to the Google Groups "MiniSat" group.
To unsubscribe from this group and stop receiving emails from it, send an email to minisat+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/minisat/1ee0e5da-aafd-4cac-95c7-de955edd3588%40googlegroups.com.