Speed comparison between CMS 2.9.x and CMS 3.0

[capiman]

Just want to point you to a CNF (already often used by me) which is much slower with CMS 3.0 compared to CMS 2.9.x

It can be downloaded:

http://guest.engelschall.com/~martin/6x6.cnf.gz

I call it with --maxsolutions=1000 / --maxsol=1000 and write results to a result file.

Here are some measured times (but not done one free machine, so other performance hungry applications running in parallel, but it gives general hint about speed of this CNF):

CMS 2.9.6 -> 1703 seconds CMS 2.9.7 -> 1477 seconds

CMS 3.0 (sources from 28.03.2013) -> 11160 seconds CMS 3.0 (sources from 02.04.2013) -> 11425 seconds

A few hundreds seconds more or less does not matter, i think CMS 2.9.6 and CMS 2.9.7 need around the same time?

But difference between CMS 2.9.x and CMS 3.0 is around factor 6.5 to 7.5.

Perhaps restart is the problem, i will test this next by adding all solutions by negative clause, so no restart is needed.

Are there perhaps suggested command line options for CMS 3.0, so it behaves like CMS 2.9.6.

But i think this is not a general topic, because i think i have seen calculation which take endless with 2.9.6, but were solvable with CMS 3.0. As always it depends on the CNF you try to solve and a lot of luck, that solver takes the optimal variables first.

[capiman]

NOTE: Pay attention that you are not overwriting your input CNFs due to changed command line format!!!

cms30 file1.cnf file2.cnf -> OK

cms297 file1.cnf file2.cnf -> Now you have overwritten file2.cnf !!!

Correct: cms297 --alsoread=file1.cnf file2.cnf

[capiman]

I have done another test tonight. As written above i took the 260 solutions from above, inverted them, so they are filtered out and called CMS in different versions. I called them 3 times, with same input and alternating sequence, just to rule out PC is sometimes heavier in use than during other situations.

d:\cryptominisat-3.0-02042013\cmsat\cryptominisat64 6x6_neg.cnf f:\6x6\6x6.cnf > cms30_1.txt d:\cryptominisat-2.9.7\cmsat\cryptominisat64 --alsoread=6x6_neg.cnf f:\6x6\6x6.cnf > cms297_1.txt

d:\cryptominisat-3.0-02042013\cmsat\cryptominisat64 6x6_neg.cnf f:\6x6\6x6.cnf > cms30_2.txt d:\cryptominisat-2.9.7\cmsat\cryptominisat64 --alsoread=6x6_neg.cnf f:\6x6\6x6.cnf > cms297_2.txt

d:\cryptominisat-3.0-02042013\cmsat\cryptominisat64 6x6_neg.cnf f:\6x6\6x6.cnf > cms30_3.txt d:\cryptominisat-2.9.7\cmsat\cryptominisat64 --alsoread=6x6_neg.cnf f:\6x6\6x6.cnf > cms297_3.txt

Here are the results (sorted after CMS version, no multi-threading!):

grep "c CPU time" *.txt cms297_1.txt:c CPU time : 891.03 s cms297_2.txt:c CPU time : 1385.61 s cms297_3.txt:c CPU time : 1470.97 s

grep "Total time" *.txt cms30_1.txt:c Total time : 6632.45 cms30_2.txt:c Total time : 6143.89 cms30_3.txt:c Total time : 6461.11

So the calculation restart (due to --maxsol) seems to be not to be the problem.

[msoos]

I just added the option "--presimp". If you launch with "--presimp 0" it should work much faster. Can you please tell me how much faster it is now?

[capiman]

Tests to find the 260 solutions of 6x6.cnf:

These are (again) the results from previous tests:

CMS 2.9.6 -> 1703 seconds CMS 2.9.7 -> 1477 seconds

CMS 3.0 (sources from 28.03.2013) -> 11160 seconds CMS 3.0 (sources from 02.04.2013) -> 11425 seconds

Now

CMS 3.0 (sources from 06.04.2013 and --presimp=0) -> 9145s

[capiman]

CMS 3.0 (sources from 06.04.2013 and WITHOUT "--presimp=0") -> 10403s

[capiman]

I have done a small test, where i measured the time to find a solution:

With 2.9.7 it looks like the following (from beginning, first 20 of 260 solutions):

c Needed 16.30 seconds from 0.12 to 16.43 c Needed 18.56 seconds from 16.43 to 34.99 c Needed 27.14 seconds from 35.01 to 62.15 c Needed 5.93 seconds from 62.15 to 68.08 c Needed 3.48 seconds from 68.08 to 71.56 c Needed 0.00 seconds from 71.56 to 71.56 c Needed 2.11 seconds from 71.57 to 73.68 c Needed 0.50 seconds from 73.68 to 74.18 c Needed 1.51 seconds from 74.18 to 75.69 c Needed 7.22 seconds from 75.69 to 82.91 c Needed 0.02 seconds from 82.91 to 82.93 c Needed 0.00 seconds from 82.93 to 82.93 c Needed 5.77 seconds from 82.93 to 88.70 c Needed 42.50 seconds from 88.70 to 131.20 c Needed 2.53 seconds from 131.20 to 133.72 c Needed 5.33 seconds from 133.72 to 139.06 c Needed 0.00 seconds from 139.07 to 139.07 c Needed 0.01 seconds from 139.07 to 139.09 c Needed 0.02 seconds from 139.09 to 139.10 c Needed 2.00 seconds from 139.10 to 141.10 ...

-> Minimum is 0.00 seconds to find a new solution.

With CMS 3.0 it looks like the following (from beginning, first 20 of 260 solutions):

c Needed 29.97 seconds from 0.25 to 30.22 c Needed 14.79 seconds from 30.23 to 45.02 c Needed 14.51 seconds from 45.08 to 59.59 c Needed 14.96 seconds from 59.59 to 74.55 c Needed 14.55 seconds from 74.57 to 89.12 c Needed 14.90 seconds from 89.14 to 104.04 c Needed 14.32 seconds from 104.05 to 118.37 c Needed 14.20 seconds from 118.39 to 132.58 c Needed 14.52 seconds from 132.58 to 147.11 c Needed 30.84 seconds from 147.12 to 177.96 c Needed 27.66 seconds from 177.96 to 205.62 c Needed 19.95 seconds from 205.64 to 225.59 c Needed 17.99 seconds from 225.59 to 243.58 c Needed 16.00 seconds from 243.59 to 259.60 c Needed 33.37 seconds from 259.62 to 292.98 c Needed 20.59 seconds from 293.00 to 313.59 c Needed 16.50 seconds from 313.61 to 330.11 c Needed 17.44 seconds from 330.13 to 347.57 c Needed 25.47 seconds from 347.57 to 373.04 c Needed 41.48 seconds from 373.04 to 414.52 ...

-> Minimum is 14.20 seconds to find a new solution.

This is the part where CMS 3.0 needed the 14.20 seconds:

c SCC new: 0 T: 0.02 s c Cache cleaned. Updated: 0 K Cleaned: 0 K Freed: 0 K T: 0.02 c [bcache] 0-depth ass: 0 BXprop: 0 T: 0.02 c [implicit] sub bin: 0 tri: 0 (stamp: 0, cache: 0) T: 0.03 T-out: N w-visit: 2560 c [probe] lits : 0.64M act vars: 1.27K BP+HP todo: 2736.00M c [clean] T: 0.0160 s c [probe] NumProps after perf multi: 1368.00M after numcall multi: 2122.92M (<- final) c [probe] 0-depth assigns: 0 bsame: 0 Flit: 0 Visited: 2536/2536(100.0%) c [probe] probed: 2482(97.9%) hyperBin:16218 transR-Irred:0 transR-Red:30 c [probe] BP: 217.5M HP: 101.0M T: 3.73 c [cl-str] stamp-based lit-rem: 0 inv-lit-rem: 0 stamp-cl-rem: 0 c [cl-str] bintri-based lit-rem: 61 cl-sub: 0 c [cl-str] cache-based lit-rem: 2987 cl-sub: 0 c [cl-str] stamp-based lit-rem: 0 inv-lit-rem: 0 stamp-cl-rem: 0 c [cl-str] bintri-based lit-rem: 303 cl-sub: 5 c [cl-str] cache-based lit-rem: 3004 cl-sub: 0 c [asymm] longirred tried: 1445/8514 cl-rem:3 lits-rem:21 T: 0.58 T-out: Y c [vivif] cache-based irred-- cl tried 8514 cl-sh 109 cl-rem 0 lit-rem 3048 time-out N T: 1.33 c [vivif] cache-based red-- cl tried 881 cl-sh 150 cl-rem 5 lit-rem 3307 time-out N T: 0.11 c [vivif] asymm (tri+long) useful: 3/1445/8514 lits-rem:21 0-depth-assigns:0 T: 0.58 s time-out: Y c [implicit] sub bin: 15315 tri: 0 (stamp: 0, cache: 0) T: 0.08 T-out: N w-visit: 2560 c SCC new: 0 T: 0.02 s c [clean] T: 0.0150 s c vrep vars 0 lits 0 rem-bin-cls 0 rem-tri-cls 0 rem-long-cls 0 T: 0.03 s c [clean] T: 0.0150 s c [simp] mem usage for occur of irred 2 MB c [simp] mem usage for occur of red 1 MB c [simp] Not linked in red 105/876 (11.99 %) c Mem for watches : 6 MB c #try to eliminate: 1268 c #var-elim: 36 c #time-out: N c #time: 5.32 c [subs] long subBySub: 4108 subByStr: 54 lits-rem-str: 794 T: 0.42(0.03 is overhead) s c [v-elim] elimed: 36 / 1504 / 1268 T: 5.32 s T-out: 0 c [v-elim] cl-new: 4663 tried: 36 tested: 1268 (100.00 % agressive) c [v-elim] subs: 193 learnt-bin rem: 883 learnt-tri rem: 0 learnt-long rem: 0 v-fix: 0 c [simp] link-in T: 0.02 cleanup T: 0.02 c [implicit] str lit bin: 0 lit tri: 0 (by tri: 0) (by stamp: 0) set-var: 0 T: 0.11 T-out: N w-visit: 2560 c [implicit] sub bin: 0 tri: 0 (stamp: 0, cache: 0) T: 0.05 T-out: N w-visit: 2560 c Cache cleaned. Updated: 0 K Cleaned: 6 K Freed: 7 K T: 0.02 c [cl-str] stamp-based lit-rem: 0 inv-lit-rem: 0 stamp-cl-rem: 0 c [cl-str] bintri-based lit-rem: 290 cl-sub: 313 c [cl-str] cache-based lit-rem: 144430 cl-sub: 0 c [cl-str] stamp-based lit-rem: 0 inv-lit-rem: 0 stamp-cl-rem: 0 c [cl-str] bintri-based lit-rem: 0 cl-sub: 0 c [cl-str] cache-based lit-rem: 0 cl-sub: 0 c [asymm] longirred tried: 1358/8221 cl-rem:132 lits-rem:1801 T: 0.59 T-out: Y c [vivif] cache-based irred-- cl tried 8534 cl-sh 3884 cl-rem 313 lit-rem 144720 time-out N T: 1.28 c [vivif] cache-based red-- cl tried 868 cl-sh 0 cl-rem 0 lit-rem 0 time-out N T: 0.11 c [vivif] asymm (tri+long) useful: 132/1358/8221 lits-rem:1801 0-depth-assigns:0 T: 0.59 s time-out: Y c SCC new: 0 T: 0.02 s c [clean] T: 0.0160 s c calculated reachability. T: 0.016 c size4: 472 size5: 464 larger: 7285 c [clean] T: 0.0160 s c Doing bust search for 300 conflicts c 300-long burst search learnt units:0 learnt bins: 0 c percent of negative polarities set: 0.96 % (this is used to choose restart type) c Chose restart type glue-based c Using var act-multip 11 instead of standard 11 and act-divider 10 instead of standard 10 c 154 38K 1232 8221 314 143K 20.3 1166 287 38K 91.8 c irred prop: 18K conf: 0K UIP used: 3K c red prop: 0K conf: 0K UIP used: 0K c sum lits visit: 0K cls visit: 0K prop: 19K conf: 0K UIP used: 3K c [clean] T: 0.0160 s c [DBclean] Hard limit would be: 938850 c [DBclean] Pre-removed: 0 clean type will be propconfl c [DBclean] rem 248 avgGlue 14.28 avgSize 113.54 c [DBclean] remain 918 avgGlue 7.97 avgSize 85.89 T 0.02 c Verified 8221 clauses. s SATISFIABLE v ... c Number of solutions found until now: 8 c Needed 14.20 seconds from 118.39 to 132.58

[capiman]

Some more measurements (but machine was again heavy in use, so perhaps not right numbers, copy to a editor with fixed font, perhaps only valid for 6x6.cnf):

6407.89 seconds -> --presimp=0 --varelim=0 --vivif=0 6539.74 seconds -> --presimp=0 --varelim=0 --vivif=0 --probe=0 6567.27 seconds -> --presimp=0 --vivif=0 6728.98 seconds -> --presimp=0 --varelim=0 6887.64 seconds -> --presimp=0 --varelim=0 --probe=0 6912.89 seconds -> --varelim=0 --vivif=0 --probe=0 7569.12 seconds -> --presimp=0 --probe=0 7756.54 seconds -> --varelim=0 --probe=0 7764.98 seconds -> --varelim=0 7970.16 seconds -> --presimp=0 --probe=0 8761.88 seconds -> --probe=0 8974.00 seconds -> --varelim=0 --vivif=0 9099.71 seconds -> --vivif=0 9366.26 seconds -> (none of the parameters) 9547.31 seconds -> --presimp=0 9970.53 seconds -> --probe=0 --vivif=0

[capiman]

Yesterdays version needed: c Total time : 107626.19 This is almost 30 hours to solve. Command line used: cryptominisat64 --maxsol=1000 --dumpres=6x6.res 6x6.cnf Correct number of solutions was found.

Here a part of the output:

... c Number of solutions found until now: 223 c [clean] T: 1.9190 s c [clean] T: 1.9660 s c vrep vars 0 lits 0 rem-bin-cls 0 rem-tri-cls 0 rem-long-cls 0 T: 3.99 s c Found components: 1 BP: 2.30M time: 5.99 s c large component 0 size: 1205 c Not printed total small (<300 vars) components:0 vars: 0 c Only one component, not handling it separately c SCC new: 0 T: 0.02 s c Cache cleaned. Updated: 0 K Cleaned: 0 K Freed: 0 K T: 0.03 c [bcache] 0-depth ass: 0 BXprop: 0 T: 0.02 c [implicit] sub bin: 0 tri: 0 (stamp: 0, cache: 0) T: 0.09 T-out: N w-visit: 2560 c [probe] lits : 119.15M act vars: 1.21K BP+HP todo: 1824.00M c [clean] T: 2.0280 s c [probe] NumProps after perf multi: 912.00M after numcall multi: 2694.21M (<- final) c [probe] time spent updating cache during probing: 0.1% c [probe] 0-depth assigns: 0 bsame: 0 Flit: 0 Visited: 2374/2410(98.5%) c [probe] probed: 2278(94.5%) hyperBin:21881 transR-Irred:0 transR-Red:138 c [probe] BP: 2588.7M HP: 101.6M T: 91.48 c [cl-str] stamp-based lit-rem: 0 inv-lit-rem: 0 stamp-cl-rem: 0 c [cl-str] bintri-based lit-rem: 0 cl-sub: 0 c [cl-str] cache-based lit-rem: 0 cl-sub: 0 c [cl-str] stamp-based lit-rem: 0 inv-lit-rem: 0 stamp-cl-rem: 0 c [cl-str] bintri-based lit-rem: 0 cl-sub: 370 c [cl-str] cache-based lit-rem: 0 cl-sub: 0 c [cl-str] stamp-based lit-rem: 0 inv-lit-rem: 0 stamp-cl-rem: 0 c [cl-str] bintri-based lit-rem: 343 cl-sub: 0 c [cl-str] cache-based lit-rem: 2690 cl-sub: 0 c [cl-str] stamp-based lit-rem: 0 inv-lit-rem: 0 stamp-cl-rem: 0 c [cl-str] bintri-based lit-rem: 2063 cl-sub: 82 c [cl-str] cache-based lit-rem: 77692 cl-sub: 18 c [asymm] longirred tried: 27/9821 cl-rem:14 lits-rem:204 T: 3.49 T-out: Y c [vivif] cache-based irred-- cl tried 9821 cl-sh 113 cl-rem 0 lit-rem 3033 time-out N T: 3.45 c [vivif] cache-based red-- cl tried 3955 cl-sh 2898 cl-rem 100 lit-rem 79755 time-out Y T: 3.42 c [vivif] asymm (tri+long) useful: 14/27/9821 lits-rem:204 0-depth-assigns:0 T: 3.51 s time-out: Y c [implicit] sub bin: 20510 tri: 0 (stamp: 0, cache: 0) T: 0.42 T-out: N w-visit: 2560 c SCC new: 0 T: 0.01 s c [clean] T: 2.1990 s c vrep vars 0 lits 0 rem-bin-cls 0 rem-tri-cls 0 rem-long-cls 0 T: 4.16 s c [clean] T: 2.1690 s c [simp] mem usage for occur of irred 3 MB c [simp] mem usage for occur of red 1807 MB c [simp] Not linking in red due to excessive expected memory usage c [simp] Not linked in red 801914/801914 (100.00 %) c Mem for watches : 63 MB (1165.18 %) c #try to eliminate: 1205 c #var-elim: 36 c #time-out: N c #time: 14.90 c [subs] long subBySub: 3678 subByStr: 390 lits-rem-str: 244 T: 10.87(5.99 is overhead) s c [v-elim] elimed: 36 / 37716 / 1205 T: 14.91 s T-out: 0 c [v-elim] cl-new: 4506 tried: 36 tested: 1205 (100.00 % agressive) c [v-elim] subs: 303 learnt-bin rem: 1175 learnt-tri rem: 0 learnt-long rem: 0 v-fix: 0 c [simp] link-in T: 0.67 cleanup T: 5.32 c [implicit] str lit bin: 0 lit tri: 0 (by tri: 0) (by stamp: 0) set-var: 0 T: 0.08 T-out: N w-visit: 2560 c [implicit] sub bin: 0 tri: 0 (stamp: 0, cache: 0) T: 0.20 T-out: N w-visit: 2560 c Cache cleaned. Updated: 0 K Cleaned: 6 K Freed: 7 K T: 0.03 c [cl-str] stamp-based lit-rem: 0 inv-lit-rem: 0 stamp-cl-rem: 0 c [cl-str] bintri-based lit-rem: 0 cl-sub: 275 c [cl-str] cache-based lit-rem: 0 cl-sub: 0 c [cl-str] stamp-based lit-rem: 0 inv-lit-rem: 0 stamp-cl-rem: 0 c [cl-str] bintri-based lit-rem: 0 cl-sub: 319 c [cl-str] cache-based lit-rem: 0 cl-sub: 0 c [cl-str] stamp-based lit-rem: 0 inv-lit-rem: 0 stamp-cl-rem: 0 c [cl-str] bintri-based lit-rem: 253 cl-sub: 0 c [cl-str] cache-based lit-rem: 127168 cl-sub: 0 c [cl-str] stamp-based lit-rem: 0 inv-lit-rem: 0 stamp-cl-rem: 0 c [cl-str] bintri-based lit-rem: 2040 cl-sub: 63 c [cl-str] cache-based lit-rem: 72741 cl-sub: 15 c [asymm] longirred tried: 32/9278 cl-rem:30 lits-rem:553 T: 3.56 T-out: Y c [vivif] cache-based irred-- cl tried 9278 cl-sh 3667 cl-rem 0 lit-rem 127421 time-out N T: 4.51 c [vivif] cache-based red-- cl tried 3753 cl-sh 2762 cl-rem 78 lit-rem 74781 time-out Y T: 3.85 c [vivif] asymm (tri+long) useful: 30/32/9278 lits-rem:553 0-depth-assigns:0 T: 3.57 s time-out: Y c SCC new: 0 T: 0.02 s c [clean] T: 2.3090 s c calculated reachability. T: 0.015 c size4: 535 size5: 579 larger: 8164 c [clean] T: 2.0280 s c Doing burst search for 300 conflicts c 300-long burst search learnt units:0 learnt bins: 3 c percent of negative polarities set: 96.07 % (this is used to choose restart type) c Chose restart type glue-based c Using var act-multip 11 instead of standard 11 and act-divider 10 instead of standard 10 c 4945 1290K 1169 9278 278 125K 20.9 801K 2030 45K 147.7 c 4947 1291K 1169 9278 278 125K 20.9 802K 2035 45K 147.6 c Verified 9278 clauses. c Verified 9278 clauses. s SATISFIABLE v ... c Number of solutions found until now: 224 c SCC new: 0 T: 0.13 s c Cache cleaned. Updated: 0 K Cleaned: 0 K Freed: 0 K T: 0.01 c [bcache] 0-depth ass: 1 BXprop: 0 T: 0.02 c [implicit] sub bin: 0 tri: 0 (stamp: 0, cache: 0) T: 0.31 T-out: N w-visit: 2560 c [probe] lits : 119.11M act vars: 1.20K BP+HP todo: 1824.00M c [clean] T: 4.7110 s c [probe] NumProps after perf multi: 912.00M after numcall multi: 2696.60M (<- final) c [probe] time spent updating cache during probing: 0.1% c [clean] T: 2.6050 s c [probe] 0-depth assigns: 1 bsame: 0 Flit: 1 Visited: 2384/2408(99.0%) c [probe] probed: 2305(95.7%) hyperBin:22426 transR-Irred:96 transR-Red:671 c [probe] BP: 2594.0M HP: 98.0M T: 149.10 c [cl-str] stamp-based lit-rem: 0 inv-lit-rem: 0 stamp-cl-rem: 0 c [cl-str] bintri-based lit-rem: 0 cl-sub: 2 c [cl-str] cache-based lit-rem: 0 cl-sub: 0 c [cl-str] stamp-based lit-rem: 0 inv-lit-rem: 0 stamp-cl-rem: 0 c [cl-str] bintri-based lit-rem: 0 cl-sub: 383 c [cl-str] cache-based lit-rem: 0 cl-sub: 0 c [cl-str] stamp-based lit-rem: 0 inv-lit-rem: 0 stamp-cl-rem: 0 c [cl-str] bintri-based lit-rem: 66 cl-sub: 1 c [cl-str] cache-based lit-rem: 3083 cl-sub: 0 c [cl-str] stamp-based lit-rem: 0 inv-lit-rem: 0 stamp-cl-rem: 0 c [cl-str] bintri-based lit-rem: 2540 cl-sub: 84 c [cl-str] cache-based lit-rem: 71965 cl-sub: 16 c [asymm] longirred tried: 23/9655 cl-rem:8 lits-rem:171 T: 6.32 T-out: Y c [vivif] cache-based irred-- cl tried 9657 cl-sh 212 cl-rem 1 lit-rem 3149 time-out N T: 7.89 c [vivif] cache-based red-- cl tried 3690 cl-sh 2792 cl-rem 100 lit-rem 74505 time-out Y T: 6.63 c [vivif] asymm (tri+long) useful: 8/23/9655 lits-rem:171 0-depth-assigns:0 T: 6.32 s time-out: Y c [implicit] sub bin: 20612 tri: 9 (stamp: 0, cache: 0) T: 0.70 T-out: N w-visit: 2560 c SCC new: 0 T: 0.11 s c [clean] T: 4.0560 s c vrep vars 0 lits 0 rem-bin-cls 0 rem-tri-cls 0 rem-long-cls 0 T: 7.93 s c [clean] T: 3.8530 s c [simp] mem usage for occur of irred 3 MB c [simp] mem usage for occur of red 1789 MB c [simp] Not linking in red due to excessive expected memory usage c [simp] Not linked in red 795365/795365 (100.00 %) c Mem for watches : 76 MB (1397.18 %) c #try to eliminate: 1203 c #var-elim: 36 c #time-out: N c #time: 32.48 c [subs] long subBySub: 3396 subByStr: 382 lits-rem-str: 244 T: 23.17(12.50 is overhead) s c [v-elim] elimed: 36 / 37884 / 1203 T: 32.54 s T-out: 0 c [v-elim] cl-new: 4500 tried: 36 tested: 1203 (100.00 % agressive) c [v-elim] subs: 306 learnt-bin rem: 1163 learnt-tri rem: 0 learnt-long rem: 0 v-fix: 0 c [simp] link-in T: 1.03 cleanup T: 11.47 c [implicit] str lit bin: 0 lit tri: 4 (by tri: 1) (by stamp: 0) set-var: 0 T: 0.30 T-out: N w-visit: 2560 c [implicit] sub bin: 4 tri: 0 (stamp: 0, cache: 0) T: 0.30 T-out: N w-visit: 2560 c Cache cleaned. Updated: 0 K Cleaned: 7 K Freed: 9 K T: 0.14 c [cl-str] stamp-based lit-rem: 0 inv-lit-rem: 0 stamp-cl-rem: 0 c [cl-str] bintri-based lit-rem: 0 cl-sub: 278 c [cl-str] cache-based lit-rem: 0 cl-sub: 0 c [cl-str] stamp-based lit-rem: 0 inv-lit-rem: 0 stamp-cl-rem: 0 c [cl-str] bintri-based lit-rem: 0 cl-sub: 362 c [cl-str] cache-based lit-rem: 0 cl-sub: 0 c [cl-str] stamp-based lit-rem: 0 inv-lit-rem: 0 stamp-cl-rem: 0 c [cl-str] bintri-based lit-rem: 267 cl-sub: 0 c [cl-str] cache-based lit-rem: 126471 cl-sub: 0 c [cl-str] stamp-based lit-rem: 0 inv-lit-rem: 0 stamp-cl-rem: 0 c [cl-str] bintri-based lit-rem: 2351 cl-sub: 84 c [cl-str] cache-based lit-rem: 71635 cl-sub: 13 c [asymm] longirred tried: 40/9390 cl-rem:37 lits-rem:760 T: 7.32 T-out: Y c [vivif] cache-based irred-- cl tried 9390 cl-sh 3658 cl-rem 0 lit-rem 126738 time-out N T: 8.39 c [vivif] cache-based red-- cl tried 3764 cl-sh 2823 cl-rem 97 lit-rem 73986 time-out Y T: 7.50 c [vivif] asymm (tri+long) useful: 38/40/9390 lits-rem:761 0-depth-assigns:0 T: 7.32 s time-out: Y c SCC new: 0 T: 0.02 s c [clean] T: 4.1970 s c calculated reachability. T: 0.000 c size4: 550 size5: 588 larger: 8252 c [clean] T: 4.7270 s c Doing burst search for 300 conflicts c 300-long burst search learnt units:0 learnt bins: 0 c percent of negative polarities set: 96.07 % (this is used to choose restart type) c Chose restart type glue-based c Using var act-multip 11 instead of standard 11 and act-divider 10 instead of standard 10 c 4951 1292K 1167 9390 281 124K 20.9 795K 2023 44K 147.4 c Verified 9390 clauses. c Verified 9390 clauses. s SATISFIABLE v ... c Number of solutions found until now: 225