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

Mate Soos soos.mate at gmail.com
Mer 12 Jan 15:25:29 CET 2011


-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

Hi Martin,

On 01/11/2011 10:04 AM, Martin Maurer wrote:
> through GIT i see you are working on three different versions / branches:
> 
> cryptominisat-11012011-cluster129-fixed
> cryptominisat-11012011-cluster129-extra
> cryptominisat-11012011-agilityBasedRestart

Yes :)

> I took the three branches (version from 11.01.2011 morning) and have done a 
> few tests.
> 
> Compiling issues:
> 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 fixed this with an #ifdef, hope it works now :)

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

This was meant to be the fixed version, so I am happy :) This will be
released as 2.9.0 in the very near future. I fixed a ton of bug inside,
so I hope this is _rock solid_. Anyone willing to test would be very
welcome to do so! I am not tuning anything now, just waiting for a
cluster run to finish, and maybe I will launch another cluster run to
test multi-threaded performance.

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

Maybe I didn't merge the -fixed into the tree at this point. I checked
and it seems OK now. Beware that this version is using ER and the
solution-banning is wrong here (i.e. may find infinite no. of
solutions). This is a very experimental branch, expect misbehaviour.

> 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

I have just merged cluster129-fixed into this branch. It seems to work,
but again ER is messing things up in terms of no. of solutions. Will fix :)

> 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

Thanks for this very thorough bug report. There were multiple very nasty
bugs, some reported by different people, including you, researchers,
etc. I think we are nearing release quality for branch cluster129-fixed.
Branch agiltybasedRestart is meant to be far more advanced, but
currently is badly broken from a performance point of view.

Thank you again, and looking forward to any bugs that are in
"cluster129-fixed"

Bests,

Mate

PS: I don't intend to fix any performance bug in cluster129-fixed.
Performance tuning has been killing me for far too long -> see
agilityBasedRestart :D

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

iEYEARECAAYFAk0tudkACgkQsTOOstKb0jmyOwCfdJmB+8HuG1yYo6aH+YeYCWNY
5+EAn3TMvi3VbClrC0LlteoMjrJG6VgI
=PuIT
-----END PGP SIGNATURE-----



More information about the Cryptominisat-devel mailing list