segmentation fault with minisat 2.2.0

[Matthew Gwynne]

Hi,

minisat-2.2.0 segfaulted on the following instance:

  http://cs.swan.ac.uk/~csmg/E3_SAT_genhorn_44_4.cnf.tar.bz2

If there is any other additional information I can provide to help debug this, please let me know.

Thanks in advance,

Matthew Gwynne
http://cs.swan.ac.uk/~csmg/

P.S - I've CCed Oliver Kullmann as he is the one who experienced the segfault but he had problems posting to google groups.

[Nuno S]

Disable the pre-processing performed by the SimpSolver.

I experienced some segmentation faults in such simplifications and turning them off solved the problem. However, the searches become more expensive.

[Michael Tautschnig]

Hi,

> minisat-2.2.0 segfaulted on the following instance:
>
> http://cs.swan.ac.uk/~csmg/E3_SAT_genhorn_44_4.cnf.tar.bz2
>
> If there is any other additional information I can provide to help debug
> this, please let me know.
>

[...]

Which OS and compiler are you using? How much memory is available on this
system? Could you provide the log of all the output up to the segfault? How long
does it (approximately) take to reach it?

Best,
Michael

[Niklas Sörensson]

Hi,

I'm guessing you're running out of memory on this one as I can see that this is an example where MiniSat's clause-removal heuristics is just too stupid. It never removes anything, and the learned clauses have approximately 6-7k literals on average.

You will probably have more luck with glucose on this example.

/Niklas

--
 
---
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.
For more options, visit https://groups.google.com/groups/opt_out.
 
 

[Matthew Gwynne]

Hi,

On Thursday, May 9, 2013 6:07:53 PM UTC+1, Michael Tautschnig wrote:

Which OS and compiler are you using? How much memory is available on this
system? Could you provide the log of all the output up to the segfault? How long
does it (approximately) take to reach it?

Best,
Michael

The environment and output is as follows:
 

uname -a

Linux cs-wsok 3.4.33-2.24-desktop #1 SMP PREEMPT Tue Feb 26 03:34:33 UTC 2013 (5f00a32) x86_64 x86_64 x86_64 GNU/Linux

Suse 11.2
gcc 4.5.4
32 GB

WARNING: for repeatability, setting FPU to use double precision
============================[ Problem Statistics ]=============================
|                                                                             |
|  Number of variables:        449957                                         |
|  Number of clauses:         5813349                                         |
|  Parse time:                   1.48 s                                       |
|  Eliminated clauses:           0.07 Mb                                      |
|  Simplification time:         30.28 s                                       |
|                                                                             |
=============================[ Search Statistics ]==============================
| Conflicts  |          ORIGINAL         |          LEARNT          | Progress |
|            |    Vars  Clauses Literals |    Limit  Clauses Lit/Cl |          |
================================================================================
|        100 |  442204  5743581 16942396 |  2105979       99    397 |  0.862 % |
|        250 |  442204  5743581 16942396 |  2316577      249   4873 |  0.862 % |
|        475 |  442204  5743581 16942396 |  2548235      474   3813 |  0.862 % |
|        812 |  442204  5743581 16942396 |  2803058      811   4412 |  0.862 % |
|       1318 |  442204  5743581 16942396 |  3083364     1317   3286 |  0.862 % |
|       2077 |  442204  5743581 16942396 |  3391701     2076   3860 |  0.862 % |
|       3216 |  442204  5743581 16942396 |  3730871     3215   7226 |  0.862 % |
|       4924 |  442204  5743581 16942396 |  4103958     4923   6864 |  0.862 % |
|       7486 |  442204  5743581 16942396 |  4514354     7485   6624 |  0.862 % |
|      11330 |  442204  5743581 16942396 |  4965789    11329   7940 |  0.862 % |
|      17096 |  442204  5743581 16942396 |  5462368    17095   8600 |  0.862 % |
|      25745 |  442204  5743536 16942306 |  6008605    25744   7993 |  0.862 % |
|      38719 |  429713  5743536 16942306 |  6609466    38717   8907 |  3.638 % |


Time unknown.

Please just run it on your machine and see what happens.

Thanks,

Matthew Gwynne
http://cs.swan.ac.uk/~csmg/

[Matthew Gwynne]

Hi,

On Thursday, May 9, 2013 6:39:13 PM UTC+1, Niklas Sörensson wrote:

I'm guessing you're running out of memory on this one as I can see that this is an example where MiniSat's clause-removal heuristics is just too stupid. It never removes anything, and the learned clauses have approximately 6-7k literals on average.

I think that at segfault time it used only 15% of memory.

You will probably have more luck with glucose on this example.

Glucose, at least version 2.0, performs worse on these examples than
minisat.


Thanks,

Matthew
http://cs.swan.ac.uk/~csmg/

 

[Matthew Gwynne]

Hi,

On Thursday, May 9, 2013 3:59:40 PM UTC+1, Nuno S wrote:

Disable the pre-processing performed by the SimpSolver.

I experienced some segmentation faults in such simplifications and turning them off solved the problem. However, the searches become more expensive.

 We also experience a segfault with "minisat -no-pre" using the following instance:

  http://cs.swan.ac.uk/~csmg/E2_SAT_genhorn_35_5.cnf.tar.bz2

Thanks,

Matthew
http://cs.swan.ac.uk/~csmg/

[Mate Soos]

Hi Matthew,

CryptoMiniSat current master solves this in about 600s on my machine,
with some 0.5GB of mem used. However, this is probably the exception,
and as Niklas pointed out, the extremely large clauses would inhibit
most SAT solvers from solving these problems if many learnt clauses need
to be stored in memory. I would try lingeling, it's extremely
memory-efficient as Armin Biere puts a lot of effort into memory and
cache usage.

Cheers,

Mate

[Matthew Gwynne]

Hi Mate,

On Monday, May 13, 2013 12:38:33 PM UTC+1, msoos wrote:

CryptoMiniSat current master solves this in about 600s on my machine,
with some 0.5GB of mem used. However, this is probably the exception,
and as Niklas pointed out, the extremely large clauses would inhibit
most SAT solvers from solving these problems if many learnt clauses need
to be stored in memory. I would try lingeling, it's extremely
memory-efficient as Armin Biere puts a lot of effort into memory and
cache usage.

We haven't tried the latest cryptominisat yet (only 2.9.6), but we plan to do so soon! Sure, lingeling doesn't run out of memory, although I think in this instance it just ran out of time instead. OKsolver, PrecoSAT and cryptominisat-2.9.6 were actually better here (this particular instance is solvable using full failed literal elimination). We actually fully understand these instances (from a theoretical/structural standpoint) and know they are unsatisfiable. We are running experiments to see how different solvers react to certain different translations.

Matthew