[Cryptominisat-devel] Some small testing results: compile errors and reproduceable crashes

Martin Maurer meinemailingliste at online.de
Mar 11 Jan 10:04:04 CET 2011


Hello Mate,

through GIT i see you are working on three different versions / branches:

cryptominisat-11012011-cluster129-fixed
cryptominisat-11012011-cluster129-extra
cryptominisat-11012011-agilityBasedRestart

I took the three branches (version from 11.01.2011 morning) and have done a 
few tests.

Compiling issues:

cryptominisat-11012011-cluster129-fixed: No compile problem
cryptominisat-11012011-cluster129-extra: No compile problem

cryptominisat-11012011-agilityBasedRestart

        myConf.simpBurstSConf *= 1.0f + std::max(0.2f*(float)num, 2.0f);
        myConf.simpStartMult *= 1.0f - std::max(0.1f*(float)num, 0.7f);
        myConf.simpStartMMult *= 1.0f - std::max(0.1f*(float)num, 0.7f);

still makes problem. I have changed it to this

        myConf.simpBurstSConf *= 1.0f + max(0.2f*(float)num, 2.0f);
        myConf.simpStartMult *= 1.0f - max(0.1f*(float)num, 0.7f);
        myConf.simpStartMMult *= 1.0f - max(0.1f*(float)num, 0.7f);

Then i can compile also this version on windows.

I have run the created versions on my 6x6.cnf:

*********************************************************************************************

cryptominisat-11012011-cluster129-fixed: Finds 260 solutions, which is 
correct. Runtime: ~ 2379.55s (doing other thing parallel...)

*********************************************************************************************

cryptominisat-11012011-cluster129-extra: Crashes even before first solution. 
Last lines are:

c Added 13 vars  tried: 80000 time: 2.53
c ORs :     13 avg-s:  0.0 cl-sh:     0 l-rem:      0 b-add:     26 v-rep: 
0 cl-rem: 1393 avg s: 1
43.1 T:    3.36
c lits-rem:      5359  cl-subs:     1337  v-elim:      0  v-fix:    0  time: 
5.00 s
c learnt bin added due to v-elim: 0
c vivif2 --  cl tried     4372 cl shrink       10 lits rem         49 time: 
0.01
c vivif2 --  cl tried    15401 cl shrink     1312 lits rem       3426 time: 
0.07
c asymm  cl-useful: 8/870/4366 lits-rem:17 time: 0.23
c calculated reachability. Time: 0.01
c  N dy   457     69906      1239      4365    180424     15398    361980 
703497      9.42   no data

Doing it again:

c Added 13 vars  tried: 80000 time: 1.97
c ORs :     13 avg-s:  0.0 cl-sh:     0 l-rem:      0 b-add:     26 v-rep: 
0 cl-rem: 1393 avg s: 1
43.1 T:    2.62
c lits-rem:      5359  cl-subs:     1337  v-elim:      0  v-fix:    0  time: 
4.13 s
c learnt bin added due to v-elim: 0
c vivif2 --  cl tried     4372 cl shrink       10 lits rem         49 time: 
0.01
c vivif2 --  cl tried    15401 cl shrink     1312 lits rem       3426 time: 
0.07
c asymm  cl-useful: 8/870/4366 lits-rem:17 time: 0.22
c calculated reachability. Time: 0.01
c  N dy   457     69906      1239      4365    180424     15398    361980 
703497      9.42   no data

Looks to be the same position, where crash happens in both trials.

*********************************************************************************************

cryptominisat-11012011-agilityBasedRestart: Crashes after a few found 
solutions:

c vivif2 --  cl tried     4446 cl shrink        0 lits rem          0 time: 
0.01
c vivif2 --  cl tried    32732 cl shrink     1807 lits rem       2709 time: 
0.16
c vivif2 --  cl tried     4446 cl shrink        0 lits rem          0 time: 
0.01
c vivif2 --  cl tried    32731 cl shrink        0 lits rem          0 time: 
0.14
c asymm  cl-useful: 2/571/4446 lits-rem:3 time: 0.27
c subs with bin:        4  lits-rem:         0  v-fix:    0  time:  1.35 s
c Subs w/ non-existent bins:   1212 time:  0.20 s
c ORs :   2543 avg-s: 57.1 cl-sh:   328 l-rem:   5454 b-add:      1 v-rep: 
0 cl-rem: 0 avg s: -1.$ T:    0.26
c Added 13 vars  tried: 23507 time: 0.81
c ORs :     13 avg-s:  0.0 cl-sh:  8343 l-rem:   8343 b-add:     26 v-rep: 
0 cl-rem: 9 avg s: 5.3 T:    0.85
c lits-rem:      2399  cl-subs:     1322  v-elim:      0  v-fix:    0  time: 
3.57 s
c calculated reachability. Time: 0.01
c  N dy   458    219684      1235      4452    175461     30189    430357 
1269241     69.60     18.26
c  F st   458    219684      1235      4452    175461     30189    430357 
1269241     69.60     18.26

Tried again cryptominisat-11012011-agilityBasedRestart: Again crashed after 
a few found solutions:

c vivif2 --  cl tried     4446 cl shrink        0 lits rem          0 time: 
0.01
c vivif2 --  cl tried    32732 cl shrink     1807 lits rem       2709 time: 
0.14
c vivif2 --  cl tried     4446 cl shrink        0 lits rem          0 time: 
0.01
c vivif2 --  cl tried    32731 cl shrink        0 lits rem          0 time: 
0.13
c asymm  cl-useful: 2/571/4446 lits-rem:3 time: 0.22
c subs with bin:        4  lits-rem:         0  v-fix:    0  time:  1.26 s
c Subs w/ non-existent bins:   1212 time:  0.19 s
c ORs :   2543 avg-s: 57.1 cl-sh:   328 l-rem:   5454 b-add:      1 v-rep: 
0 cl-rem: 0 avg s: -1.$ T:    0.25
c Added 13 vars  tried: 23507 time: 0.70
c ORs :     13 avg-s:  0.0 cl-sh:  8343 l-rem:   8343 b-add:     26 v-rep: 
0 cl-rem: 9 avg s: 5.3 T:    0.73
c lits-rem:      2399  cl-subs:     1322  v-elim:      0  v-fix:    0  time: 
3.18 s
c calculated reachability. Time: 0.01
c  N dy   458    219684      1235      4452    175461     30189    430357 
1269241     69.60     18.26
c  F st   458    219684      1235      4452    175461     30189    430357 
1269241     69.60     18.26

Looks like it is crashing in the same area. vivif2 numbers are same in first 
/ second trial.
2 lines statistical output (just before crash) are also the same.

*********************************************************************************************

All my tests are using the following command line (with exe from different 
branches)

cryptominisat64.exe --threads=1 --maxsolutions=100000 --dumplearnts=6x6_learnt.cnf 
 --maxdumplearnts=2 6x6.cnf

Best regards,

Martin




More information about the Cryptominisat-devel mailing list