Long running parts in CMS 3.0: [v-elim] and [probe]

[capiman]

On a hard/big CNF i see the following long running parts. It it worth that it takes so long, can it made shorter or is it even a bug that it takes so long? (see complete log below, i know there are command line options to switch these parts off)

-> Search for "c [v-elim]" (each run around 700 seconds) and "c [probe]" (each run around 180 seconds)

28 c [v-elim] elimed: 0 / 4874 / 16807 T: 710.07 s 29 c [v-elim] cl-new: 0 tried: 0 tested: 0 (-1.#J % agressive) 30 c [v-elim] subs: 0 learnt-bin rem: 0 learnt-tri rem: 0 learnt-long rem: 0 v-fix: 0 104 c [v-elim] elimed: 0 / 6892 / 16807 T: 710.71 s 105 c [v-elim] cl-new: 0 tried: 0 tested: 0 (-1.#J % agressive) 106 c [v-elim] subs: 0 learnt-bin rem: 0 learnt-tri rem: 0 learnt-long rem: 0 v-fix: 0 182 c [v-elim] elimed: 0 / 8442 / 16807 T: 829.49 s 183 c [v-elim] cl-new: 0 tried: 0 tested: 0 (-1.#J % agressive) 184 c [v-elim] subs: 0 learnt-bin rem: 0 learnt-tri rem: 0 learnt-long rem: 0 v-fix: 0 266 c [v-elim] elimed: 0 / 9748 / 16807 T: 727.05 s 267 c [v-elim] cl-new: 0 tried: 0 tested: 0 (-1.#J % agressive) 268 c [v-elim] subs: 0 learnt-bin rem: 0 learnt-tri rem: 0 learnt-long rem: 0 v-fix: 0 354 c [v-elim] elimed: 0 / 10898 / 16807 T: 721.28 s 355 c [v-elim] cl-new: 0 tried: 0 tested: 0 (-1.#J % agressive) 356 c [v-elim] subs: 0 learnt-bin rem: 0 learnt-tri rem: 0 learnt-long rem: 0 v-fix: 0

-> Seems it has not brought any advantage with this CNF using [v-elim]?

14 c [probe] 0-depth assigns: 0 bsame: 0 Flit: 0 Visited: 20686/33614(61.5%) 15 c [probe] probed: 7600(22.6%) hyperBin:21845 transR-Irred:1330 transR-Red:15 16 c [probe] P: 169.9M T: 189.44 87 c [probe] 0-depth assigns: 0 bsame: 0 Flit: 0 Visited: 21056/33614(62.6%) 88 c [probe] probed: 8334(24.8%) hyperBin:19202 transR-Irred:1158 transR-Red:65 89 c [probe] P: 195.2M T: 181.24 165 c [probe] 0-depth assigns: 0 bsame: 0 Flit: 0 Visited: 21239/33614(63.2%) 166 c [probe] probed: 8696(25.9%) hyperBin:16969 transR-Irred:676 transR-Red:119 167 c [probe] P: 211.8M T: 187.95 249 c [probe] 0-depth assigns: 0 bsame: 0 Flit: 0 Visited: 21351/33614(63.5%) 250 c [probe] probed: 8926(26.6%) hyperBin:17264 transR-Irred:512 transR-Red:199 251 c [probe] P: 224.2M T: 192.67 337 c [probe] 0-depth assigns: 0 bsame: 0 Flit: 0 Visited: 21419/33614(63.7%) 338 c [probe] probed: 9054(26.9%) hyperBin:16433 transR-Irred:80 transR-Red:86 339 c [probe] P: 234.5M T: 196.40 430 c [probe] 0-depth assigns: 0 bsame: 0 Flit: 0 Visited: 21329/33614(63.5%) 431 c [probe] probed: 8880(26.4%) hyperBin:14638 transR-Irred:52 transR-Red:301 432 c [probe] P: 243.2M T: 198.43

-> Seems it has not brought any advantage with this CNF using [probe]?

Here is the complete log:

d:\cryptominisat-23012013\cmsat>cryptominisat64 --dumpsimplified=10x10_wob6_orig_1_set_1_orig_5nnn.cnf --dumplearnt=10x10_wob 6_learnt_1_set_1_orig_5nnn.cnf 10x10_wob6_orig_1_set_1_orig_4nnn.cnf c Outputting solution to console c CryptoMiniSat version MSVC-compiled, without GIT c compiled with non-gcc compiler c Reading file '10x10_wob6_orig_1_set_1_orig_4nnn.cnf' c -- header says num vars: 17056 c -- header says num clauses: 12032860 c -- clauses added: 0 learnts, 12032860 normals c -- vars added 17056 c Parsing time: 22.16 s c [implicit] rem-bin 0 rem-tri 0 rem-litBin: 0 rem-litTri: 3 stamp:0 set-var: 0 time: 9.20 s c [clean] T: 1.7310 s c [probe] 0-depth assigns: 0 bsame: 0 Flit: 0 Visited: 20686/33614(61.5%) c [probe] probed: 7600(22.6%) hyperBin:21845 transR-Irred:1330 transR-Red:15 c [probe] P: 169.9M T: 189.44 c [timestamp] lit-rem: 0 inv-lit-rem: 0 stamp-rem: 0 c [timestamp] lit-rem: 0 inv-lit-rem: 0 stamp-rem: 0 c Need to finish asymm -- ran out of prop (=allocated time) c [vivif] cache-based irred-- cl tried 81757 cl-sh 1128 cl-rem 3 lit-rem 30050 time-out N time: 47.46 c [vivif] cache-based red-- cl tried 0 cl-sh 0 cl-rem 0 lit-rem 0 time-out N time: 0.10 c [vivif] asymm (tri+long) useful: 24/24/81752 lits-rem:123 0-depth-assigns:0 T: 0.18 s c [implicit] rem-bin 1241 rem-tri 0 rem-litBin: 0 rem-litTri: 0 stamp:0 set-var: 0 time: 6.30 s c [clean] T: 0.6960 s c blocking through: 55854 blocked: 0 T : 0.38 c AsymmTElim asymm subsumed: 0 blocked: 0 T : 0.33 c lits-rem: 706 subsSUB: 0 subsSTR: 0 T: 1.76(0.87 is overhead) s c [v-elim] elimed: 0 / 4874 / 16807 T: 710.07 s c [v-elim] cl-new: 0 tried: 0 tested: 0 (-1.#J % agressive) c [v-elim] subs: 0 learnt-bin rem: 0 learnt-tri rem: 0 learnt-long rem: 0 v-fix: 0 c [simp] link-in T: 0.59 cleanup T: 0.27 c [timestamp] lit-rem: 0 inv-lit-rem: 0 stamp-rem: 0 c [timestamp] lit-rem: 0 inv-lit-rem: 0 stamp-rem: 0 c Need to finish asymm -- ran out of prop (=allocated time) c [vivif] cache-based irred-- cl tried 81752 cl-sh 0 cl-rem 0 lit-rem 0 time-out N time: 45.57 c [vivif] cache-based red-- cl tried 0 cl-sh 0 cl-rem 0 lit-rem 0 time-out N time: 0.10 c [vivif] asymm (tri+long) useful: 4/4/81752 lits-rem:16 0-depth-assigns:0 T: 0.23 s c SCC new: 0 T: 0.19 s c [clean] T: 0.6960 s c size4: 2162 size5: 1573 larger: 78017 c [clean] T: 0.6890 s c Doing bust search for 300 conflicts c 300-long burst search learnt units:0 learnt bins: 0 LHBR: 17 c Using var act-multip 11 instead of standard 11 and act-divider 10 instead of standard 10 c rest conf freevar IrrL IrrT IrrB l/c RedL RedT RedB l/c c 6 1014 16807 81K 2429 11947K 75.8 994 12 20K 799.7 c 11 1937 16807 81K 2429 11947K 75.8 1895 21 20K 815.1 c 12 3033 16807 81K 2429 11947K 75.8 2968 35 20K 754.8 c 15 3859 16807 81K 2429 11947K 75.8 3781 40 20K 742.8 c 19 4691 16807 81K 2429 11947K 75.8 4598 48 20K 744.5 c 21 5903 16807 81K 2429 11947K 75.8 5790 55 20K 771.7 c 27 6780 16807 81K 2429 11947K 75.8 6649 64 20K 762.2 c 31 7825 16807 81K 2429 11947K 75.8 7671 75 20K 748.4 c irred lits visit: 438992K cls visit: 15920K prop: 2638K conf: 6K UIP used: 236K c red lits visit: 90638K cls visit: 1052K prop: 17K conf: 2K UIP used: 11K c sum lits visit: 529631K cls visit: 16972K prop: 2655K conf: 8K UIP used: 247K c [clean] T: 0.7430 s c vrep vars 0 lits 0 rem-bin-cls 0 rem-tri-cls 0 rem-long-cls 0 T: 1.49 s c [clean] T: 0.7310 s c lits-rem: 0 subsSUB: 152 subsSTR: 0 T: 2.06(0.97 is overhead) s c Time wasted on clean&replace&sub: 2.09 c [DBclean] Pre-removed: 0 next by propconfl c [DBclean] rem 2615 avgGlue 44.89 avgSize 1035.40 c [DBclean] remain 5079 avgGlue 31.77 avgSize 601.53 c Using var act-multip 11 instead of standard 11 and act-divider 10 instead of standard 10 c 36 8681 16807 81K 2429 11947K 75.8 5737 84 20K 620.7 c 37 9659 16807 81K 2429 11947K 75.8 6700 93 20K 660.3 c 41 10746 16807 81K 2429 11947K 75.8 7763 111 20K 700.9 c 45 11826 16807 81K 2429 11947K 75.8 8829 116 20K 706.9 c 51 12681 16807 81K 2429 11947K 75.8 9664 124 20K 719.4 c 56 13657 16807 81K 2429 11947K 75.8 10629 129 20K 739.8 c 58 14618 16807 81K 2429 11947K 75.8 11578 135 20K 740.5 c irred lits visit: 346562K cls visit: 14988K prop: 2761K conf: 5K UIP used: 267K c red lits visit: 196964K cls visit: 2849K prop: 37K conf: 3K UIP used: 15K c sum lits visit: 543526K cls visit: 17837K prop: 2798K conf: 8K UIP used: 283K c [clean] T: 0.7840 s c vrep vars 0 lits 0 rem-bin-cls 0 rem-tri-cls 0 rem-long-cls 0 T: 1.60 s c [clean] T: 0.8130 s c lits-rem: 0 subsSUB: 88 subsSTR: 0 T: 2.25(1.25 is overhead) s c Time wasted on clean&replace&sub: 2.26 c [DBclean] Pre-removed: 0 next by propconfl c [DBclean] rem 4311 avgGlue 44.53 avgSize 907.03 c [DBclean] remain 8534 avgGlue 28.11 avgSize 681.62 c SCC new: 0 T: 0.19 s c [implicit] rem-bin 0 rem-tri 0 rem-litBin: 0 rem-litTri: 0 stamp:0 set-var: 0 time: 6.48 s c [clean] T: 0.7580 s c [probe] 0-depth assigns: 0 bsame: 0 Flit: 0 Visited: 21056/33614(62.6%) c [probe] probed: 8334(24.8%) hyperBin:19202 transR-Irred:1158 transR-Red:65 c [probe] P: 195.2M T: 181.24 c [timestamp] lit-rem: 0 inv-lit-rem: 1 stamp-rem: 0 c [timestamp] lit-rem: 49 inv-lit-rem: 4 stamp-rem: 0 c Need to finish asymm -- ran out of prop (=allocated time) c [vivif] cache-based irred-- cl tried 81752 cl-sh 7 cl-rem 0 lit-rem 15 time-out N time: 49.77 c [vivif] cache-based red-- cl tried 8534 cl-sh 3827 cl-rem 0 lit-rem 1148026 time-out N time: 6.41 c [vivif] asymm (tri+long) useful: 2/33/81752 lits-rem:6 0-depth-assigns:0 T: 0.20 s c SCC new: 0 T: 0.20 s c [clean] T: 0.7570 s c vrep vars 0 lits 0 rem-bin-cls 0 rem-tri-cls 0 rem-long-cls 0 T: 1.52 s c [implicit] rem-bin 5072 rem-tri 0 rem-litBin: 0 rem-litTri: 0 stamp:0 set-var: 0 time: 6.34 s c [clean] T: 0.7330 s c blocking through: 61317 blocked: 0 T : 0.36 c AsymmTElim asymm subsumed: 0 blocked: 0 T : 0.34 c lits-rem: 658 subsSUB: 6 subsSTR: 0 T: 1.58(1.09 is overhead) s c [v-elim] elimed: 0 / 6892 / 16807 T: 710.71 s c [v-elim] cl-new: 0 tried: 0 tested: 0 (-1.#J % agressive) c [v-elim] subs: 0 learnt-bin rem: 0 learnt-tri rem: 0 learnt-long rem: 0 v-fix: 0 c [simp] link-in T: 0.72 cleanup T: 0.37 c [timestamp] lit-rem: 0 inv-lit-rem: 0 stamp-rem: 0 c [timestamp] lit-rem: 0 inv-lit-rem: 0 stamp-rem: 0 c Need to finish asymm -- ran out of prop (=allocated time) c [vivif] cache-based irred-- cl tried 81752 cl-sh 0 cl-rem 0 lit-rem 0 time-out N time: 49.29 c [vivif] cache-based red-- cl tried 8527 cl-sh 0 cl-rem 0 lit-rem 0 time-out N time: 5.52 c [vivif] asymm (tri+long) useful: 4/4/81752 lits-rem:12 0-depth-assigns:0 T: 0.22 s c SCC new: 0 T: 0.21 s c [clean] T: 0.7460 s c size4: 2162 size5: 1573 larger: 78017 c [clean] T: 0.7200 s c Doing bust search for 300 conflicts c 300-long burst search learnt units:0 learnt bins: 0 LHBR: 1 c Using var act-multip 11 instead of standard 11 and act-divider 10 instead of standard 10 c rest conf freevar IrrL IrrT IrrB l/c RedL RedT RedB l/c c 67 16962 16807 81K 2429 11945K 75.8 9469 158 34K 559.8 c 71 17982 16807 81K 2429 11945K 75.8 10475 164 34K 583.3 c 75 18899 16807 81K 2429 11945K 75.8 11379 170 34K 598.0 c 80 20K 16807 81K 2429 11945K 75.8 12502 178 34K 622.5 c 85 20K 16807 81K 2429 11945K 75.8 13394 184 34K 631.9 c 90 22K 16807 81K 2429 11945K 75.8 14446 192 34K 643.4 c 94 22K 16807 81K 2429 11945K 75.8 15327 199 34K 661.5 c 98 24K 16807 81K 2429 11945K 75.8 16720 209 34K 676.3 c irred lits visit: 514627K cls visit: 18767K prop: 3133K conf: 6K UIP used: 273K c red lits visit: 190892K cls visit: 3059K prop: 50K conf: 3K UIP used: 17K c sum lits visit: 705519K cls visit: 21826K prop: 3184K conf: 9K UIP used: 291K c [clean] T: 0.7550 s c vrep vars 0 lits 0 rem-bin-cls 0 rem-tri-cls 0 rem-long-cls 0 T: 1.54 s c [clean] T: 0.7630 s c lits-rem: 0 subsSUB: 37 subsSTR: 0 T: 1.92(1.39 is overhead) s c Time wasted on clean&replace&sub: 1.93 c [DBclean] Pre-removed: 0 next by propconfl c [DBclean] rem 5728 avgGlue 44.83 avgSize 977.59 c [DBclean] remain 11421 avgGlue 22.24 avgSize 525.77 c Using var act-multip 11 instead of standard 11 and act-divider 10 instead of standard 10 c 102 25K 16807 81K 2429 11945K 75.8 11816 220 34K 529.7 c 108 26K 16807 81K 2429 11945K 75.8 12929 228 34K 563.0 c 112 27K 16807 81K 2429 11945K 75.8 14202 234 34K 593.7 c 116 28K 16807 81K 2429 11945K 75.8 15357 240 34K 620.6 c 120 29K 16807 81K 2429 11945K 75.8 16429 244 34K 628.3 c 124 30K 16807 81K 2429 11945K 75.8 17441 251 34K 642.8 c 127 31K 16807 81K 2429 11945K 75.8 18370 258 34K 656.0 c 133 32K 16807 81K 2429 11945K 75.8 19442 264 34K 659.0 c 138 33K 16807 81K 2429 11945K 75.8 20K 268 34K 668.2 c irred lits visit: 528321K cls visit: 19652K prop: 3397K conf: 6K UIP used: 302K c red lits visit: 385898K cls visit: 6613K prop: 86K conf: 4K UIP used: 26K c sum lits visit: 914219K cls visit: 26265K prop: 3484K conf: 10K UIP used: 328K c [clean] T: 0.7600 s c vrep vars 0 lits 0 rem-bin-cls 0 rem-tri-cls 0 rem-long-cls 0 T: 1.59 s c [clean] T: 0.8150 s c lits-rem: 0 subsSUB: 23 subsSTR: 0 T: 2.12(1.64 is overhead) s c Time wasted on clean&replace&sub: 2.13 c [DBclean] Pre-removed: 0 next by propconfl c [DBclean] rem 6985 avgGlue 38.22 avgSize 972.50 c [DBclean] remain 13947 avgGlue 22.28 avgSize 512.87 c SCC new: 0 T: 0.21 s c [implicit] rem-bin 0 rem-tri 0 rem-litBin: 0 rem-litTri: 0 stamp:0 set-var: 0 time: 6.14 s c [clean] T: 0.7610 s c [probe] 0-depth assigns: 0 bsame: 0 Flit: 0 Visited: 21239/33614(63.2%) c [probe] probed: 8696(25.9%) hyperBin:16969 transR-Irred:676 transR-Red:119 c [probe] P: 211.8M T: 187.95 c [timestamp] lit-rem: 0 inv-lit-rem: 0 stamp-rem: 0 c [timestamp] lit-rem: 128 inv-lit-rem: 1481 stamp-rem: 0 c Need to finish asymm -- ran out of prop (=allocated time) c [vivif] cache-based irred-- cl tried 81752 cl-sh 3 cl-rem 0 lit-rem 5 time-out N time: 53.62 c [vivif] cache-based red-- cl tried 13947 cl-sh 4857 cl-rem 0 lit-rem 1496192 time-out N time: 8.54 c [vivif] asymm (tri+long) useful: 2/32/81752 lits-rem:6 0-depth-assigns:0 T: 0.19 s c SCC new: 0 T: 0.21 s c [clean] T: 0.7360 s c vrep vars 0 lits 0 rem-bin-cls 0 rem-tri-cls 0 rem-long-cls 0 T: 1.51 s c [implicit] rem-bin 8827 rem-tri 0 rem-litBin: 0 rem-litTri: 0 stamp:0 set-var: 0 time: 6.34 s c [clean] T: 0.7660 s c blocking through: 64886 blocked: 0 T : 0.36 c AsymmTElim asymm subsumed: 0 blocked: 0 T : 0.34 c lits-rem: 630 subsSUB: 4 subsSTR: 1 T: 1.62(1.15 is overhead) s c [v-elim] elimed: 0 / 8442 / 16807 T: 829.49 s c [v-elim] cl-new: 0 tried: 0 tested: 0 (-1.#J % agressive) c [v-elim] subs: 0 learnt-bin rem: 0 learnt-tri rem: 0 learnt-long rem: 0 v-fix: 0 c [simp] link-in T: 0.75 cleanup T: 0.40 c [timestamp] lit-rem: 0 inv-lit-rem: 0 stamp-rem: 0 c [timestamp] lit-rem: 0 inv-lit-rem: 0 stamp-rem: 0 c Need to finish asymm -- ran out of prop (=allocated time) c [vivif] cache-based irred-- cl tried 81752 cl-sh 0 cl-rem 0 lit-rem 0 time-out N time: 53.14 c [vivif] cache-based red-- cl tried 13937 cl-sh 0 cl-rem 0 lit-rem 0 time-out N time: 7.26 c [vivif] asymm (tri+long) useful: 4/4/81752 lits-rem:12 0-depth-assigns:0 T: 0.23 s c SCC new: 0 T: 0.20 s c [clean] T: 0.7200 s c size4: 2162 size5: 1573 larger: 78017 c [clean] T: 0.7270 s c Doing bust search for 300 conflicts c 300-long burst search learnt units:0 learnt bins: 0 LHBR: 0 c Using var act-multip 11 instead of standard 11 and act-divider 10 instead of standard 10 c rest conf freevar IrrL IrrT IrrB l/c RedL RedT RedB l/c c 145 35K 16807 81K 2429 11945K 75.8 14793 283 42K 430.5 c 148 36K 16807 81K 2429 11945K 75.8 16086 296 42K 468.7 c 152 37K 16807 81K 2429 11945K 75.8 16910 306 42K 485.8 c 154 38K 16807 81K 2429 11945K 75.8 17907 314 42K 520.9 c 156 39K 16807 81K 2429 11945K 75.8 18704 323 42K 539.0 c 160 40K 16807 81K 2429 11945K 75.8 19515 326 42K 544.7 c 163 41K 16807 81K 2429 11945K 75.8 20K 331 42K 554.4 c 169 41K 16807 81K 2429 11945K 75.8 21K 339 42K 567.0 c 175 42K 16807 81K 2429 11945K 75.8 22K 343 43K 576.3 c 178 44K 16807 81K 2429 11945K 75.8 23K 352 43K 602.1 c 183 45K 16807 81K 2429 11945K 75.8 24K 364 43K 616.2 c irred lits visit: 680157K cls visit: 22532K prop: 3663K conf: 6K UIP used: 307K c red lits visit: 385443K cls visit: 5876K prop: 101K conf: 4K UIP used: 27K c sum lits visit: 1065600K cls visit: 28408K prop: 3764K conf: 11K UIP used: 334K c [clean] T: 0.7900 s c vrep vars 0 lits 0 rem-bin-cls 0 rem-tri-cls 0 rem-long-cls 0 T: 1.60 s c [clean] T: 0.7770 s c lits-rem: 0 subsSUB: 22 subsSTR: 0 T: 2.26(1.77 is overhead) s c Time wasted on clean&replace&sub: 2.27 c [DBclean] Pre-removed: 0 next by propconfl c [DBclean] rem 8126 avgGlue 41.99 avgSize 840.78 c [DBclean] remain 16232 avgGlue 23.71 avgSize 504.08 c Using var act-multip 11 instead of standard 11 and act-divider 10 instead of standard 10 c 185 46K 16807 81K 2429 11945K 75.8 18055 370 43K 565.4 c 188 47K 16807 81K 2429 11945K 75.8 18879 375 43K 587.8 c 193 48K 16807 81K 2429 11945K 75.8 19673 381 43K 596.4 c 197 49K 16807 81K 2429 11945K 75.8 20K 388 43K 608.9 c 200 50K 16807 81K 2429 11945K 75.8 21K 392 43K 627.1 c 203 51K 16807 81K 2429 11945K 75.8 22K 394 43K 633.5 c 209 52K 16807 81K 2429 11945K 75.8 23K 397 43K 645.4 c 212 53K 16807 81K 2429 11945K 75.8 24K 401 43K 653.8 c 215 54K 16807 81K 2429 11945K 75.8 25K 408 43K 663.6 c 219 55K 16807 81K 2429 11945K 75.8 26K 414 43K 674.2 c rest conf freevar IrrL IrrT IrrB l/c RedL RedT RedB l/c c 223 56K 16807 81K 2429 11945K 75.8 27K 421 43K 680.9 c irred lits visit: 531236K cls visit: 21361K prop: 3902K conf: 6K UIP used: 360K c red lits visit: 620820K cls visit: 10091K prop: 150K conf: 6K UIP used: 38K c sum lits visit: 1152056K cls visit: 31453K prop: 4053K conf: 12K UIP used: 398K c [clean] T: 0.8530 s c vrep vars 0 lits 0 rem-bin-cls 0 rem-tri-cls 0 rem-long-cls 0 T: 1.69 s c [clean] T: 0.8320 s c lits-rem: 0 subsSUB: 22 subsSTR: 0 T: 2.65(2.11 is overhead) s c Time wasted on clean&replace&sub: 2.66 c [DBclean] Pre-removed: 0 next by propconfl c [DBclean] rem 9253 avgGlue 43.57 avgSize 996.37 c [DBclean] remain 18486 avgGlue 21.89 avgSize 528.12 c SCC new: 0 T: 0.20 s c [implicit] rem-bin 0 rem-tri 0 rem-litBin: 0 rem-litTri: 0 stamp:0 set-var: 0 time: 6.12 s c [clean] T: 0.8070 s c [probe] 0-depth assigns: 0 bsame: 0 Flit: 0 Visited: 21351/33614(63.5%) c [probe] probed: 8926(26.6%) hyperBin:17264 transR-Irred:512 transR-Red:199 c [probe] P: 224.2M T: 192.67 c [timestamp] lit-rem: 0 inv-lit-rem: 0 stamp-rem: 0 c [timestamp] lit-rem: 174 inv-lit-rem: 89 stamp-rem: 0 c Need to finish asymm -- ran out of prop (=allocated time) c [vivif] cache-based irred-- cl tried 81752 cl-sh 9 cl-rem 0 lit-rem 13 time-out N time: 55.69 c [vivif] cache-based red-- cl tried 18486 cl-sh 5771 cl-rem 0 lit-rem 1854117 time-out N time: 14.92 c [vivif] asymm (tri+long) useful: 0/33/81752 lits-rem:0 0-depth-assigns:0 T: 0.27 s c SCC new: 0 T: 0.25 s c [clean] T: 0.9100 s c vrep vars 0 lits 0 rem-bin-cls 0 rem-tri-cls 0 rem-long-cls 0 T: 1.93 s c [implicit] rem-bin 10718 rem-tri 0 rem-litBin: 0 rem-litTri: 0 stamp:0 set-var: 0 time: 6.77 s c [clean] T: 0.8000 s c blocking through: 67661 blocked: 0 T : 0.39 c AsymmTElim asymm subsumed: 0 blocked: 0 T : 0.34 c lits-rem: 844 subsSUB: 1 subsSTR: 1 T: 1.92(1.41 is overhead) s c [v-elim] elimed: 0 / 9748 / 16807 T: 727.05 s c [v-elim] cl-new: 0 tried: 0 tested: 0 (-1.#J % agressive) c [v-elim] subs: 0 learnt-bin rem: 0 learnt-tri rem: 0 learnt-long rem: 0 v-fix: 0 c [simp] link-in T: 0.95 cleanup T: 0.47 c [timestamp] lit-rem: 0 inv-lit-rem: 0 stamp-rem: 0 c [timestamp] lit-rem: 0 inv-lit-rem: 0 stamp-rem: 0 c Need to finish asymm -- ran out of prop (=allocated time) c [vivif] cache-based irred-- cl tried 81752 cl-sh 0 cl-rem 0 lit-rem 0 time-out N time: 56.75 c [vivif] cache-based red-- cl tried 18483 cl-sh 0 cl-rem 0 lit-rem 0 time-out N time: 10.68 c [vivif] asymm (tri+long) useful: 4/4/81752 lits-rem:12 0-depth-assigns:0 T: 0.23 s c SCC new: 0 T: 0.22 s c [clean] T: 0.7700 s c size4: 2162 size5: 1573 larger: 78017 c [clean] T: 0.7450 s c Doing bust search for 300 conflicts c 300-long burst search learnt units:0 learnt bins: 0 LHBR: 1 c Using var act-multip 11 instead of standard 11 and act-divider 10 instead of standard 10 c rest conf freevar IrrL IrrT IrrB l/c RedL RedT RedB l/c c 230 57K 16807 81K 2429 11944K 75.8 19278 433 49K 447.8 c 235 58K 16807 81K 2429 11944K 75.8 20K 439 49K 480.4 c 237 60K 16807 81K 2429 11944K 75.8 21K 449 49K 509.9 c 239 62K 16807 81K 2429 11944K 75.8 23K 464 49K 536.8 c 244 62K 16807 81K 2429 11944K 75.8 24K 464 49K 555.7 c 246 63K 16807 81K 2429 11944K 75.8 25K 470 49K 586.9 c 250 64K 16807 81K 2429 11944K 75.8 26K 476 49K 617.9 c 253 66K 16807 81K 2429 11944K 75.8 27K 480 49K 633.8 c 257 67K 16807 81K 2429 11944K 75.8 28K 490 49K 649.2 c 259 67K 16807 81K 2429 11944K 75.8 29K 490 49K 662.2 c 265 68K 16807 81K 2429 11944K 75.8 30K 494 49K 668.0 c irred lits visit: 768642K cls visit: 26686K prop: 4445K conf: 7K UIP used: 416K c red lits visit: 591859K cls visit: 9695K prop: 167K conf: 6K UIP used: 42K c sum lits visit: 1360501K cls visit: 36381K prop: 4612K conf: 14K UIP used: 458K c [clean] T: 0.8620 s c vrep vars 0 lits 0 rem-bin-cls 0 rem-tri-cls 0 rem-long-cls 0 T: 1.67 s c [clean] T: 0.8380 s c lits-rem: 0 subsSUB: 19 subsSTR: 0 T: 2.86(2.38 is overhead) s c Time wasted on clean&replace&sub: 2.87 c [DBclean] Pre-removed: 0 next by propconfl c [DBclean] rem 10385 avgGlue 41.35 avgSize 902.13 c [DBclean] remain 20753 avgGlue 21.20 avgSize 570.20 c Using var act-multip 11 instead of standard 11 and act-divider 10 instead of standard 10 c 270 69K 16807 81K 2429 11944K 75.8 20K 501 49K 570.2 c 272 70K 16807 81K 2429 11944K 75.8 21K 503 49K 597.4 c 276 71K 16807 81K 2429 11944K 75.8 22K 508 49K 614.9 c 280 72K 16807 81K 2429 11944K 75.8 23K 511 49K 629.3 c 284 73K 16807 81K 2429 11944K 75.8 24K 513 49K 637.9 c 287 74K 16807 81K 2429 11944K 75.8 25K 518 49K 647.6 c 291 75K 16807 81K 2429 11944K 75.8 26K 524 49K 658.8 c 295 75K 16807 81K 2429 11944K 75.8 26K 526 49K 669.8 c 299 76K 16807 81K 2429 11944K 75.8 27K 530 49K 682.0 c rest conf freevar IrrL IrrT IrrB l/c RedL RedT RedB l/c c 302 78K 16807 81K 2429 11944K 75.8 29K 536 49K 706.8 c 305 80K 16807 81K 2429 11944K 75.8 31K 553 49K 721.1 c 309 81K 16807 81K 2429 11944K 75.8 31K 558 49K 725.2 c 312 81K 16807 81K 2429 11944K 75.8 32K 566 49K 733.8 c 316 82K 16807 81K 2429 11944K 75.8 33K 566 49K 740.2 c 318 83K 16807 81K 2429 11944K 75.8 34K 567 49K 748.8 c irred lits visit: 799316K cls visit: 28983K prop: 4832K conf: 7K UIP used: 452K c red lits visit: 1052075K cls visit: 17622K prop: 233K conf: 8K UIP used: 55K c sum lits visit: 1851392K cls visit: 46605K prop: 5065K conf: 15K UIP used: 507K c [clean] T: 0.8790 s c vrep vars 0 lits 0 rem-bin-cls 0 rem-tri-cls 0 rem-long-cls 0 T: 1.72 s c [clean] T: 0.8520 s c lits-rem: 0 subsSUB: 9 subsSTR: 0 T: 3.30(2.82 is overhead) s c Time wasted on clean&replace&sub: 3.31 c [DBclean] Pre-removed: 0 next by propconfl c [DBclean] rem 11568 avgGlue 40.23 avgSize 1144.08 c [DBclean] remain 23127 avgGlue 20.32 avgSize 551.17 c SCC new: 0 T: 0.21 s c [implicit] rem-bin 0 rem-tri 0 rem-litBin: 0 rem-litTri: 0 stamp:0 set-var: 0 time: 6.22 s c [clean] T: 0.8000 s c [probe] 0-depth assigns: 0 bsame: 0 Flit: 0 Visited: 21419/33614(63.7%) c [probe] probed: 9054(26.9%) hyperBin:16433 transR-Irred:80 transR-Red:86 c [probe] P: 234.5M T: 196.40 c [timestamp] lit-rem: 1 inv-lit-rem: 0 stamp-rem: 0 c [timestamp] lit-rem: 382 inv-lit-rem: 866 stamp-rem: 0 c Need to finish asymm -- ran out of prop (=allocated time) c [vivif] cache-based irred-- cl tried 81752 cl-sh 7 cl-rem 0 lit-rem 6 time-out N time: 59.44 c [vivif] cache-based red-- cl tried 23127 cl-sh 7052 cl-rem 2 lit-rem 2566921 time-out N time: 16.03 c [vivif] asymm (tri+long) useful: 0/30/81752 lits-rem:0 0-depth-assigns:0 T: 0.19 s c SCC new: 0 T: 0.21 s c [clean] T: 0.7660 s c vrep vars 0 lits 0 rem-bin-cls 0 rem-tri-cls 0 rem-long-cls 0 T: 1.59 s c [implicit] rem-bin 12872 rem-tri 0 rem-litBin: 0 rem-litTri: 0 stamp:0 set-var: 0 time: 6.35 s c [clean] T: 0.7670 s c blocking through: 71023 blocked: 0 T : 0.39 c AsymmTElim asymm subsumed: 0 blocked: 0 T : 0.35 c lits-rem: 778 subsSUB: 5 subsSTR: 0 T: 2.11(1.63 is overhead) s c [v-elim] elimed: 0 / 10898 / 16807 T: 721.28 s c [v-elim] cl-new: 0 tried: 0 tested: 0 (-1.#J % agressive) c [v-elim] subs: 0 learnt-bin rem: 0 learnt-tri rem: 0 learnt-long rem: 0 v-fix: 0 c [simp] link-in T: 1.02 cleanup T: 0.61 c [timestamp] lit-rem: 0 inv-lit-rem: 0 stamp-rem: 0 c [timestamp] lit-rem: 0 inv-lit-rem: 0 stamp-rem: 0 c Need to finish asymm -- ran out of prop (=allocated time) c [vivif] cache-based irred-- cl tried 81752 cl-sh 0 cl-rem 0 lit-rem 0 time-out N time: 60.63 c [vivif] cache-based red-- cl tried 23120 cl-sh 0 cl-rem 0 lit-rem 0 time-out N time: 14.06 c [vivif] asymm (tri+long) useful: 4/4/81752 lits-rem:16 0-depth-assigns:0 T: 0.23 s c SCC new: 0 T: 0.20 s c [clean] T: 0.7560 s c size4: 2162 size5: 1573 larger: 78017 c [clean] T: 0.7650 s c Doing bust search for 300 conflicts c 300-long burst search learnt units:0 learnt bins: 0 LHBR: 0 c Using var act-multip 11 instead of standard 11 and act-divider 10 instead of standard 10 c rest conf freevar IrrL IrrT IrrB l/c RedL RedT RedB l/c c 324 84K 16807 81K 2429 11944K 75.8 24K 571 52K 453.4 c 329 85K 16807 81K 2429 11944K 75.8 24K 579 52K 476.0 c 334 86K 16807 81K 2429 11944K 75.8 25K 589 52K 493.3 c 340 87K 16807 81K 2429 11944K 75.8 26K 597 52K 520.7 c 347 88K 16807 81K 2429 11944K 75.8 28K 605 52K 541.7 c 349 89K 16807 81K 2429 11944K 75.8 28K 607 52K 558.8 c 353 90K 16807 81K 2429 11944K 75.8 29K 609 52K 577.2 c 357 91K 16807 81K 2429 11944K 75.8 30K 617 52K 590.9 c 359 92K 16807 81K 2429 11944K 75.8 31K 621 52K 607.9 c 364 93K 16807 81K 2429 11944K 75.8 32K 625 52K 621.4 c 371 94K 16807 81K 2429 11944K 75.8 33K 630 52K 632.3 c 373 95K 16807 81K 2429 11944K 75.8 34K 635 52K 649.0 c 377 97K 16807 81K 2429 11944K 75.8 36K 639 52K 673.5 c 379 97K 16807 81K 2429 11944K 75.8 36K 641 52K 683.6 c 383 99K 16807 81K 2429 11944K 75.8 38K 645 52K 703.8 c irred lits visit: 998258K cls visit: 32494K prop: 5135K conf: 8K UIP used: 510K c red lits visit: 982156K cls visit: 15948K prop: 269K conf: 8K UIP used: 60K c sum lits visit: 1980414K cls visit: 48442K prop: 5405K conf: 17K UIP used: 571K c [clean] T: 0.8330 s c vrep vars 0 lits 0 rem-bin-cls 0 rem-tri-cls 0 rem-long-cls 0 T: 1.72 s c [clean] T: 0.8470 s c lits-rem: 0 subsSUB: 16 subsSTR: 0 T: 3.50(2.95 is overhead) s c Time wasted on clean&replace&sub: 3.52 c [DBclean] Pre-removed: 0 next by propconfl c [DBclean] rem 12818 avgGlue 39.74 avgSize 936.80 c [DBclean] remain 25621 avgGlue 20.83 avgSize 587.24 c Using var act-multip 11 instead of standard 11 and act-divider 10 instead of standard 10 c 389 100K 16807 81K 2429 11944K 75.8 26K 647 52K 606.7 c 393 101K 16807 81K 2429 11944K 75.8 27K 648 52K 626.9 c 397 102K 16807 81K 2429 11944K 75.8 28K 653 52K 649.6 c 402 103K 16807 81K 2429 11944K 75.8 29K 655 52K 664.1 c rest conf freevar IrrL IrrT IrrB l/c RedL RedT RedB l/c c 405 104K 16807 81K 2429 11944K 75.8 30K 665 52K 676.7 c 411 105K 16807 81K 2429 11944K 75.8 31K 669 52K 690.1 c 414 107K 16807 81K 2429 11944K 75.8 33K 674 52K 703.2 c 419 108K 16807 81K 2429 11944K 75.8 34K 676 52K 714.8 c 424 109K 16807 81K 2429 11944K 75.8 35K 682 52K 724.7 c 428 110K 16807 81K 2429 11944K 75.8 36K 686 52K 736.1 c 432 111K 16807 81K 2429 11944K 75.8 37K 692 52K 748.5 c 438 112K 16807 81K 2429 11944K 75.8 38K 696 52K 757.7 c 444 113K 16807 81K 2429 11944K 75.8 39K 700 52K 768.0 c 447 114K 16807 81K 2429 11944K 75.8 40K 705 52K 779.1 c 452 115K 16807 81K 2429 11944K 75.8 41K 706 52K 787.5 c 457 116K 16807 81K 2429 11944K 75.8 42K 716 52K 797.1 c irred lits visit: 1032096K cls visit: 36130K prop: 5794K conf: 8K UIP used: 603K c red lits visit: 1731440K cls visit: 27611K prop: 379K conf: 10K UIP used: 83K c sum lits visit: 2763537K cls visit: 63742K prop: 6173K conf: 18K UIP used: 687K c [clean] T: 0.9540 s c vrep vars 0 lits 0 rem-bin-cls 0 rem-tri-cls 0 rem-long-cls 0 T: 1.79 s c [clean] T: 0.9180 s c lits-rem: 0 subsSUB: 14 subsSTR: 0 T: 4.28(3.72 is overhead) s c Time wasted on clean&replace&sub: 4.29 c [DBclean] Pre-removed: 0 next by propconfl c [DBclean] rem 14176 avgGlue 41.36 avgSize 1192.71 c [DBclean] remain 28338 avgGlue 21.93 avgSize 598.86 c SCC new: 0 T: 0.20 s c [implicit] rem-bin 0 rem-tri 0 rem-litBin: 0 rem-litTri: 0 stamp:0 set-var: 0 time: 6.22 s c [clean] T: 0.8100 s c [probe] 0-depth assigns: 0 bsame: 0 Flit: 0 Visited: 21329/33614(63.5%) c [probe] probed: 8880(26.4%) hyperBin:14638 transR-Irred:52 transR-Red:301 c [probe] P: 243.2M T: 198.43 c [timestamp] lit-rem: 0 inv-lit-rem: 0 stamp-rem: 0 c [timestamp] lit-rem: 213 inv-lit-rem: 805 stamp-rem: 0 c Need to finish asymm -- ran out of prop (=allocated time) c [vivif] cache-based irred-- cl tried 81752 cl-sh 6 cl-rem 0 lit-rem 9 time-out N time: 65.13 c [vivif] cache-based red-- cl tried 28338 cl-sh 8589 cl-rem 1 lit-rem 3239170 time-out N time: 23.37 c [vivif] asymm (tri+long) useful: 2/31/81752 lits-rem:3 0-depth-assigns:0 T: 0.21 s c SCC new: 0 T: 0.18 s c [clean] T: 0.8420 s c vrep vars 0 lits 0 rem-bin-cls 0 rem-tri-cls 0 rem-long-cls 0 T: 1.69 s c [implicit] rem-bin 12859 rem-tri 0 rem-litBin: 0 rem-litTri: 0 stamp:0 set-var: 0 time: 6.37 s c [clean] T: 0.9080 s c blocking through: 74419 blocked: 0 T : 0.44 c AsymmTElim asymm subsumed: 0 blocked: 0 T : 0.33

[msoos]

I think I might have fixed some of this.. can you please run this again, with "--verb 3"? Just one or two of these [v-elim] is good enough for me to see what is going on, I think. Thank you!

[capiman]

I think vivif is now fast, probe still takes long?

Here is the log output: d:\cryptominisat-30012013\cmsat>cryptominisat64test --verb 3 --dumpsimplified=10x10_wob6_orig_1_set_1_orig_5nnnt.cnf --dumple arnt=10x10_wob6_learnt_1_set_1_orig_5nnnt.cnf 10x10_wob6_orig_1_set_1_orig_4nnn.cnf c Outputting solution to console c CryptoMiniSat version MSVC-compiled, without GIT c compiled with non-gcc compiler c Reading file '10x10_wob6_orig_1_set_1_orig_4nnn.cnf' c -- header says num vars: 17056 c -- header says num clauses: 12032860 c -- clauses added: 0 learnts, 12032860 normals c -- vars added 17056 c Parsing time: 13.48 s c Rearrange lits in clauses 0.14 s c [implicit] rem-bin 0 rem-tri 0 rem-litBin: 0 rem-litTri: 3 stamp:0 set-var: 0 time: 6.00 s c [clean] T: 0.5880 s c -------- PROBE STATS ---------- c probe time : 126.51 c 0-depth-assigns : 0 (0.00 % vars) c bothsame : 0 (0.00 % visited) c probed : 6914 (54.65 probe/sec) c failed : 0 (0.00 % of probes) c visited : 0.02 M lits (60.52 % of available lits) c bin add : 20193 (0.17 % of bins) c irred bin rem : 1252 (0.01 % of bins) c red bin rem : 10 (0.00 % of bins) c time : 126.51 s c CONFLS stats c conflicts : 0 (0.00 / sec) c conflsBinIrred : 0 (-1.#J %) c conflsBinRed : 0 (-1.#J %) c conflsTriIrred : 0 (-1.#J %) c conflsTriIrred : 0 (-1.#J %) c conflsLongIrred : 0 (-1.#J %) c conflsLongRed : 0 (-1.#J %) c DEBUG((int)numConflicts - (int)(conflsBinIrred + conflsBinRed c + conflsTriIrred + conflsTriRed + conflsLongIrred + conflsLongRed) = 0 c PROP stats c Mbogo-props : 169.92 (1.34 / sec) c Mprops : 5.09 (0.04 / sec) c propsUnit : 0 (0.00 % of propagations) c propsBinIrred : 5059823 (99.42 % of propagations) c propsBinRed : 2078 (0.04 % of propagations) c propsTriIred : 2110 (0.04 % of propagations) c propsTriRed : 0 (0.00 % of propagations) c propsLongIrred : 18498 (0.36 % of propagations) c propsLongRed : 0 (0.00 % of propagations) c LHBR : 0 (0.00 % of long propagations) c LHBR only by 3-long : 0 (-1.#J % of LHBR) c -------- PROBE STATS END ---------- c [stamp] lit-rem: 0 inv-lit-rem: 0 stamp-rem: 0 c [stamp] lit-rem: 0 inv-lit-rem: 0 stamp-rem: 0 c Need to finish asymm -- ran out of prop (=allocated time) c [vivif] longirred tried: 25/81757 cl-rem:25 lits-rem:348 c [vivif] tri tri-shorten: 0 lit-rem: 0 0-depth ass: 0 time: 0.07 c -------- ASYMM STATS -------- c time : 0.15 (0.15 per call) c timed out : 1 (100.00 % of calls) c asymm/checked/potential : 25 /25/81757 c lits-rem : 348 c 0-depth-assigns : 0 (0.00 % of vars) c --> cache-based on irred cls c time : 18.27 c shrinked/tried/total : 0 /36276/81757 c subsumed/tried/total : 0 /36276/81757 c lits-rem : 0 c called : 1 (100.00 % ran out of time) c --> cache-based on red cls c time : 0.07 c shrinked/tried/total : 0 /0/0 c subsumed/tried/total : 0 /0/0 c lits-rem : 0 c called : 1 (0.00 % ran out of time) c -------- ASYMM STATS END -------- c [implicit] rem-bin 914 rem-tri 0 rem-litBin: 0 rem-litTri: 0 stamp:0 set-var: 0 time: 5.53 s c [clean] T: 0.6200 s c subs: 0 tried: 6092 T: 0.6450 c streng sub: 0 str: 307 tried: 963 T: 0.1000 c [block] long through: 55856 tried: 55856 blocked: 0 T : 0.31 c [block] implicit tried: 2428 bin: 0 tri: 0 finished: Y T : 0.16 c AsymmTElim asymm subsumed: 0 blocked: 0 T : 0.37 c -------- Simplifier STATS ---------- c time : 3.34 (32.08 % var-elim) c v-elimed : 36 (0.21 % vars) c v-elimed: 36 / 3697 / 16807 c 0-depth assigns : 0 (0.00 % vars) c lit-rem-str : 614 c cl-new : 10803 c tried to elim : 36 (100.00 % agressively) c cl-subs : 1190 (0.01 % clauses) c blocked : 0 (0.00 % of irred clauses) c asymmSub : 0 c elim-bin-lt-cl : 29 c elim-tri-lt-cl : 0 c elim-long-lt-cl : 0 c lt-bin added due to v-elim: 0 c cl-elim-bin : 14789 c cl-elim-tri : 6 c cl-elim-long : 253 c cl-elim-avg-s : 2.46 c -------- Simplifier STATS END ---------- c [stamp] lit-rem: 0 inv-lit-rem: 0 stamp-rem: 0 c [stamp] lit-rem: 0 inv-lit-rem: 0 stamp-rem: 0 c Need to finish asymm -- ran out of prop (=allocated time) c [vivif] longirred tried: 4/91117 cl-rem:4 lits-rem:12 c [vivif] tri tri-shorten: 0 lit-rem: 0 0-depth ass: 0 time: 0.07 c -------- ASYMM STATS -------- c time : 0.18 (0.18 per call) c timed out : 1 (100.00 % of calls) c asymm/checked/potential : 4 /4/91117 c lits-rem : 12 c 0-depth-assigns : 0 (0.00 % of vars) c --> cache-based on irred cls c time : 17.17 c shrinked/tried/total : 1060 /33296/91117 c subsumed/tried/total : 0 /33296/91117 c lits-rem : 28689 c called : 1 (100.00 % ran out of time) c --> cache-based on red cls c time : 0.07 c shrinked/tried/total : 0 /0/0 c subsumed/tried/total : 0 /0/0 c lits-rem : 0 c called : 1 (0.00 % ran out of time) c -------- ASYMM STATS END -------- c ----- SCC STATS -------- c time : 0.17 (0.17 per call) c called : 1 (0.00 new found per call) c found : 0 (-1.#J % of all found) c ----- SCC STATS END -------- c [clean] T: 0.6080 s c Reordered variables T: 0.77 c Rearrange lits in clauses 0.16 s c Simplifying finished c size4: 2160 size5: 1566 larger: 87391 c [clean] T: 0.6090 s c Doing bust search for 300 conflicts c 300-long burst search learnt units:0 learnt bins: 0 LHBR: 4 c Using var act-multip 11 instead of standard 11 and act-divider 10 instead of standard 10 c rest conf freevar IrrL IrrT IrrB l/c RedL RedT RedB l/c c 4 1157 16771 91 K 2422 11932K 71.3 1124 19 19245 844.9 c 9 1990 16771 91 K 2422 11932K 71.3 1937 36 19246 834.5 c 13 2870 16771 91 K 2422 11932K 71.3 2795 45 19246 835.5 c 16 3870 16771 91 K 2422 11932K 71.3 3771 57 19246 831.6 c 19 4788 16771 91 K 2422 11932K 71.3 4674 63 19249 837.7 c 26 6115 16771 91 K 2422 11932K 71.3 5977 73 19339 826.1 c 31 7433 16771 91 K 2422 11932K 71.3 7276 80 19349 810.3 c th 1 cleaning getNextCleanLimit(): 8000 numConflicts : 8003 SumConfl: 8003 maxConfls:16000 Trail size: 249 c irred lits visit: 467491 K cls visit: 17448 K prop: 2782 K conf: 6 K UIP used: 229 K c red lits visit: 94328 K cls visit: 1242 K prop: 17 K conf: 2 K UIP used: 10 K c sum lits visit: 561819 K cls visit: 18691 K prop: 2800 K conf: 8 K UIP used: 240 K c [clean] T: 0.6350 s c --------- VAR REPLACE STATS ---------- c time : 1.29 (1.29 per call) c trees' crown : 0 (0.00 % of vars) c 0-depth assigns : 0 (0.00 % vars) c lits replaced : 0 c bin cls removed : 0 c tri cls removed : 0 c long cls removed : 0 c long lits removed : 0 c --------- VAR REPLACE STATS END ---------- c [clean] T: 0.6420 s c subs: 146 tried: 4562 T: 0.7800 c [subs] long subBySub: 146 subByStr: 0 lits-rem-str: 0 T: 1.59(0.81 is overhead) s c Time wasted on clean&replace&sub: 1.60 c ------ CLEANING STATS --------- c pre-removed : 0 (0.00 % long learnt clauses) c pre-removed lits : 0 (0.00 % long learnt lits) c pre-removed cl avg size : -1.#J c pre-removed cl avg glue : -1.#J c pre-removed cl avg num resolutions: -1.#J c clean by glue : 0 (0.00 % cleans) c clean by size : 0 (0.00 % cleans) c clean by prop&confl : 1 (100.00 % cleans) c cleaned cls : 3916 (50.00 % long learnt clauses) c cleaned lits : 3549274 (56.19 % long learnt lits) c cleaned cl avg size : 906.35 c cleaned avg glue : 43.99 c remain cls : 3770 (48.14 % long learnt clauses) c remain lits : 2578929 (40.82 % long learnt lits) c remain cl avg size : 684.07 c remain avg glue : 35.05 c ------ CLEANING STATS END --------- c consolidated memory. Num cls:94887 new size:10595356 new maxSize:16000000 c Using var act-multip 11 instead of standard 11 and act-divider 10 instead of standard 10 c 34 8438 16771 91 K 2422 11932K 71.3 4199 86 19368 687.2 c 37 9333 16771 91 K 2422 11932K 71.3 5076 95 19370 706.9 c 41 10195 16771 91 K 2422 11932K 71.3 5924 104 19372 706.5 c 44 11101 16771 91 K 2422 11932K 71.3 6816 107 19436 714.5 c 47 12395 16771 91 K 2422 11932K 71.3 8086 118 19436 723.5 c 52 14780 16771 91 K 2422 11932K 71.3 10420 143 19447 757.9 c 54 15622 16771 91 K 2422 11932K 71.3 11234 153 19499 765.3 c thread(maxconfl) Trail size: 249 over maxConfls c ------ THIS ITERATION SOLVING STATS ------- c restarts : 56 c time : 47.16 c decisions : 115269 (0.06 % random) c decisions : 115269 (1.54 % flipped polarity) c decisions/conflicts : 7.20 c CONFLS stats c conflicts : 16001 (339.26 / sec) c conflsBinIrred : 0 (0.00 %) c conflsBinRed : 0 (0.00 %) c conflsTriIrred : 125 (0.78 %) c conflsTriIrred : 4 (0.02 %) c conflsLongIrred : 11773 (73.58 %) c conflsLongRed : 4099 (25.62 %) c DEBUG((int)numConflicts - (int)(conflsBinIrred + conflsBinRed c + conflsTriIrred + conflsTriRed + conflsLongIrred + conflsLongRed) = 0 c LEARNT stats c units learnt : 0 (0.00 % of conflicts) c bins learnt : 1 (0.01 % of conflicts) c tris learnt : 158 (0.99 % of conflicts) c long learnt : 15842 (99.01 % of conflicts) c otf-subs : 172 (1.07 % of conflicts) c otf-subs learnt : 172 (100.00 % otf subsumptions) c otf-subs lits gained : 597 (3.47 lits/otf subsume) c SEAMLESS HYPERBIN&TRANS-RED stats c advProp called : 56 c hyper-bin add bin : 0 (0.00 bin/call) c trans-red rem irred bin : 0 (0.00 bin/call) c trans-red rem red bin : 0 (0.00 bin/call) c CONFL LITS stats c orig : 17366589 (1085.34 lit/confl) c rec-min effective : 12427 (77.66 % attempt successful) c rec-min lits : 3804776 (21.91 % less overall) c bin-min call% : 60.68 (70.90 % attempt successful) c bin-min lits : 580006 (3.34 % less overall) c stamp-min call% : 60.68 (22.06 % attempt successful) c stamp-min lits : 33373 (0.19 % less overall) c final avg : 809.23 c Memory used : 0.00 MB c all-threads sum CPU time : 47.16 s c PROP stats c Mbogo-props : 428.91 (9.09 / sec) c Mprops : 16.02 (0.34 / sec) c propsUnit : 0 (0.00 % of propagations) c propsBinIrred : 10013413 (62.49 % of propagations) c propsBinRed : 18175 (0.11 % of propagations) c propsTriIred : 197944 (1.24 % of propagations) c propsTriRed : 1968 (0.01 % of propagations) c propsLongIrred : 5605047 (34.98 % of propagations) c propsLongRed : 73059 (0.46 % of propagations) c LHBR : 258 (0.00 % of long propagations) c LHBR only by 3-long : 45 (17.44 % of LHBR) c props/decision : 139.02 c props/conflict : 1001.49 c ------ THIS ITERATION SOLVING STATS ------- c irred lits visit: 408699 K cls visit: 15890 K prop: 2822 K conf: 5 K UIP used: 255 K c red lits visit: 198991 K cls visit: 3078 K prop: 39 K conf: 3 K UIP used: 15 K c sum lits visit: 607691 K cls visit: 18969 K prop: 2861 K conf: 8 K UIP used: 271 K c [clean] T: 0.6750 s c --------- VAR REPLACE STATS ---------- c time : 1.36 (1.36 per call) c trees' crown : 0 (0.00 % of vars) c 0-depth assigns : 0 (0.00 % vars) c lits replaced : 0 c bin cls removed : 0 c tri cls removed : 0 c long cls removed : 0 c long lits removed : 0 c --------- VAR REPLACE STATS END ---------- c [clean] T: 0.6770 s c subs: 80 tried: 2956 T: 0.8280 c [subs] long subBySub: 80 subByStr: 0 lits-rem-str: 0 T: 1.83(1.00 is overhead) s c Time wasted on clean&replace&sub: 1.85 c ------ CLEANING STATS --------- c pre-removed : 0 (0.00 % long learnt clauses) c pre-removed lits : 0 (0.00 % long learnt lits) c pre-removed cl avg size : -1.#J c pre-removed cl avg glue : -1.#J c pre-removed cl avg num resolutions: -1.#J c clean by glue : 0 (0.00 % cleans) c clean by size : 0 (0.00 % cleans) c clean by prop&confl : 1 (100.00 % cleans) c cleaned cls : 5804 (50.00 % long learnt clauses) c cleaned lits : 5767599 (64.57 % long learnt lits) c cleaned cl avg size : 993.73 c cleaned avg glue : 43.19 c remain cls : 5724 (49.31 % long learnt clauses) c remain lits : 3051165 (34.16 % long learnt lits) c remain cl avg size : 533.05 c remain avg glue : 23.05 c ------ CLEANING STATS END --------- c consolidated memory. Num cls:96841 new size:11098856 new maxSize:27430280 c Rearrange lits in clauses 0.24 s c ----- SCC STATS -------- c time : 0.17 (0.17 per call) c called : 1 (0.00 new found per call) c found : 0 (-1.#J % of all found) c ----- SCC STATS END -------- c [implicit] rem-bin 0 rem-tri 0 rem-litBin: 0 rem-litTri: 0 stamp:0 set-var: 0 time: 5.49 s c [clean] T: 0.6340 s c -------- PROBE STATS ---------- c probe time : 147.03 c 0-depth-assigns : 0 (0.00 % vars) c bothsame : 0 (0.00 % visited) c probed : 7540 (51.28 probe/sec) c failed : 0 (0.00 % of probes) c visited : 0.02 M lits (61.42 % of available lits) c bin add : 17795 (0.15 % of bins) c irred bin rem : 423 (0.00 % of bins) c red bin rem : 33 (0.00 % of bins) c time : 147.03 s c CONFLS stats c conflicts : 0 (0.00 / sec) c conflsBinIrred : 0 (-1.#J %) c conflsBinRed : 0 (-1.#J %) c conflsTriIrred : 0 (-1.#J %) c conflsTriIrred : 0 (-1.#J %) c conflsLongIrred : 0 (-1.#J %) c conflsLongRed : 0 (-1.#J %) c DEBUG((int)numConflicts - (int)(conflsBinIrred + conflsBinRed c + conflsTriIrred + conflsTriRed + conflsLongIrred + conflsLongRed) = 0 c PROP stats c Mbogo-props : 195.22 (1.33 / sec) c Mprops : 5.56 (0.04 / sec) c propsUnit : 0 (0.00 % of propagations) c propsBinIrred : 5529510 (99.41 % of propagations) c propsBinRed : 7614 (0.14 % of propagations) c propsTriIred : 2041 (0.04 % of propagations) c propsTriRed : 0 (0.00 % of propagations) c propsLongIrred : 15733 (0.28 % of propagations) c propsLongRed : 55 (0.00 % of propagations) c LHBR : 0 (0.00 % of long propagations) c LHBR only by 3-long : 0 (-1.#J % of LHBR) c -------- PROBE STATS END ---------- c [stamp] lit-rem: 57 inv-lit-rem: 29 stamp-rem: 0 c [stamp] lit-rem: 28 inv-lit-rem: 57 stamp-rem: 0 c Need to finish asymm -- ran out of prop (=allocated time) c [vivif] longirred tried: 32/91117 cl-rem:1 lits-rem:2 c [vivif] tri tri-shorten: 0 lit-rem: 0 0-depth ass: 0 time: 0.08 c -------- ASYMM STATS -------- c time : 0.16 (0.16 per call) c timed out : 1 (100.00 % of calls) c asymm/checked/potential : 1 /32/91117 c lits-rem : 2 c 0-depth-assigns : 0 (0.00 % of vars) c --> cache-based on irred cls c time : 19.38 c shrinked/tried/total : 7838 /35378/91117 c subsumed/tried/total : 0 /35378/91117 c lits-rem : 178132 c called : 1 (100.00 % ran out of time) c --> cache-based on red cls c time : 2.63 c shrinked/tried/total : 2810 /5724/5724 c subsumed/tried/total : 0 /5724/5724 c lits-rem : 629804 c called : 1 (0.00 % ran out of time) c -------- ASYMM STATS END -------- c ----- SCC STATS -------- c time : 0.17 (0.17 per call) c called : 1 (0.00 new found per call) c found : 0 (-1.#J % of all found) c ----- SCC STATS END -------- c [clean] T: 0.6480 s c --------- VAR REPLACE STATS ---------- c time : 1.33 (1.33 per call) c trees' crown : 0 (0.00 % of vars) c 0-depth assigns : 0 (0.00 % vars) c lits replaced : 0 c bin cls removed : 0 c tri cls removed : 0 c long cls removed : 0 c long lits removed : 0 c --------- VAR REPLACE STATS END ---------- c [implicit] rem-bin 3766 rem-tri 0 rem-litBin: 0 rem-litTri: 0 stamp:0 set-var: 0 time: 5.60 s c [clean] T: 0.6420 s c subs: 589 tried: 3408 T: 0.6610 c streng sub: 95 str: 711 tried: 493 T: 0.1050 c [block] long through: 61047 tried: 57107 blocked: 0 T : 0.37 c [block] implicit tried: 2422 bin: 0 tri: 0 finished: Y T : 0.18 c AsymmTElim asymm subsumed: 0 blocked: 0 T : 0.41 c -------- Simplifier STATS ---------- c time : 3.28 (21.62 % var-elim) c v-elimed : 2 (0.01 % vars) c v-elimed: 2 / 5217 / 16771 c 0-depth assigns : 0 (0.00 % vars) c lit-rem-str : 1422 c cl-new : 1637 c tried to elim : 2 (100.00 % agressively) c cl-subs : 687 (0.01 % clauses) c blocked : 0 (0.00 % of irred clauses) c asymmSub : 0 c elim-bin-lt-cl : 0 c elim-tri-lt-cl : 0 c elim-long-lt-cl : 47 c lt-bin added due to v-elim: 0 c cl-elim-bin : 1791 c cl-elim-tri : 0 c cl-elim-long : 13 c cl-elim-avg-s : 2.60 c -------- Simplifier STATS END ---------- c [stamp] lit-rem: 0 inv-lit-rem: 0 stamp-rem: 0 c [stamp] lit-rem: 0 inv-lit-rem: 0 stamp-rem: 0 c Need to finish asymm -- ran out of prop (=allocated time) c [vivif] longirred tried: 4/92060 cl-rem:4 lits-rem:12 c [vivif] tri tri-shorten: 0 lit-rem: 0 0-depth ass: 0 time: 0.08 c -------- ASYMM STATS -------- c time : 0.22 (0.22 per call) c timed out : 1 (100.00 % of calls) c asymm/checked/potential : 4 /4/92060 c lits-rem : 12 c 0-depth-assigns : 0 (0.00 % of vars) c --> cache-based on irred cls c time : 18.75 c shrinked/tried/total : 0 /33044/92060 c subsumed/tried/total : 0 /33044/92060 c lits-rem : 0 c called : 1 (100.00 % ran out of time) c --> cache-based on red cls c time : 2.32 c shrinked/tried/total : 0 /5670/5670 c subsumed/tried/total : 0 /5670/5670 c lits-rem : 0 c called : 1 (0.00 % ran out of time) c -------- ASYMM STATS END -------- c ----- SCC STATS -------- c time : 0.17 (0.17 per call) c called : 1 (0.00 new found per call) c found : 0 (-1.#J % of all found) c ----- SCC STATS END -------- c [clean] T: 0.6530 s c Reordered variables T: 0.83 c Rearrange lits in clauses 0.22 s c Simplifying finished c size4: 3703 size5: 2577 larger: 85780 c [clean] T: 0.6590 s c Doing bust search for 300 conflicts c 300-long burst search learnt units:0 learnt bins: 0 LHBR: 58 c Using var act-multip 11 instead of standard 11 and act-divider 10 instead of standard 10 c rest conf freevar IrrL IrrT IrrB l/c RedL RedT RedB l/c c 63 16916 16769 92 K 2422 11930K 71.6 6575 165 33 K 477.7 c 68 17803 16769 92 K 2422 11930K 71.6 7438 177 33 K 509.6 c 73 18676 16769 92 K 2422 11930K 71.6 8300 181 33 K 542.7 c 75 19968 16769 92 K 2422 11930K 71.6 9569 190 33 K 582.1 c 81 20 K 16769 92 K 2422 11930K 71.6 10432 203 33 K 608.7 c 86 21 K 16769 92 K 2422 11930K 71.6 11445 208 33 K 626.3 c 89 22 K 16769 92 K 2422 11930K 71.6 12422 222 33 K 643.3

[msoos]

Probe is also fixed as per previous fix, I believe :)

[capiman]

Can you please have a look on the [v-elim] time of the following output? (sources from 14.03.2013, marked with "* HERE *")

c 174280 32336K 6797 6061K 22K 106K 4.1 5254K 0 0 39.8 c 174288 32337K 6797 6061K 22K 106K 4.1 5255K 0 0 39.8 c 174295 32338K 6797 6061K 22K 106K 4.1 5255K 0 0 39.8 c irred lits visit: 0K cls visit: 0K prop: 14722K conf: 636K UIP used: 7852K c red lits visit: 0K cls visit: 0K prop: 31101K conf: 2650K UIP used: 16714K c sum lits visit: 0K cls visit: 0K prop: 45823K conf: 3286K UIP used: 24567K c [clean] T: 3.9240 s c vrep vars 0 lits 0 rem-bin-cls 0 rem-tri-cls 0 rem-long-cls 0 T: 6.80 s c [clean] T: 3.9560 s c [DBclean] Pre-removed: 0 clean type will be propconfl c [DBclean] rem 2628000 avgGlue 22.47 avgSize 49.74 c [DBclean] remain 2628001 avgGlue 13.85 avgSize 29.91 T 11.38 c SCC new: 0 T: 0.06 s c Cache cleaned. Updated: 0 K Cleaned: 0 K Freed: 0 K T: 0.01 c [bcache] 0-depth ass: 0 BXprop: 0 T: 0.06 c [implicit] sub bin: 0 tri: 0 (stamp: 0, cache: 0) T: 0.21 T-out: Y c [clean] T: 1.7770 s c [probe] 0-depth assigns: 0 bsame: 0 Flit: 0 Visited: 13594/13594(100.0%) c [probe] probed: 13594(100.0%) hyperBin:0 transR-Irred:0 transR-Red:0 c [probe] P: 410.5M T: 11.52 c [stamp] lit-rem: 0 inv-lit-rem: 0 stamp-cl-rem: 0 c [bintri] lit-rem: 0 cl-sub: 0 c [cache] lit-rem: 97 cl-sub: 0 c [stamp] lit-rem: 0 inv-lit-rem: 0 stamp-cl-rem: 0 c [bintri] lit-rem: 527 cl-sub: 0 c [cache] lit-rem: 14410 cl-sub: 0 c [vivif] cache-based irred-- cl tried 50005 cl-sh 97 cl-rem 0 lit-rem 97 time-out Y time: 2.58 c [vivif] cache-based red-- cl tried 2708 cl-sh 2093 cl-rem 0 lit-rem 14937 time-out Y time: 0.90 c [vivif] asymm (tri+long) useful: 0/430/6061402 lits-rem:0 0-depth-assigns:0 T: 0.76 s time-out: Y c [implicit] sub bin: 0 tri: 0 (stamp: 0, cache: 0) T: 0.20 T-out: Y c SCC new: 0 T: 0.07 s c [clean] T: 1.7760 s c vrep vars 0 lits 0 rem-bin-cls 0 rem-tri-cls 0 rem-long-cls 0 T: 3.44 s c [clean] T: 1.7870 s c [block] long through: 623309 tried: 434770 blocked: 0 T : 0.60 c [block] implicit tried: 22001 bin: 0 tri: 0 finished: Y T : 0.65 c [subs] long subBySub: 29 subByStr: 0 lits-rem-str: 58 T: 10.38(9.91 is overhead) s

* HERE *

c [v-elim] elimed: 1 / 8588 / 6797 T: 626.57 s

* HERE *

c [v-elim] cl-new: 2417 tried: 1 tested: 1 (100.00 % agressive) c [v-elim] subs: 0 learnt-bin rem: 0 learnt-tri rem: 0 learnt-long rem: 69174 v-fix: 0 c [simp] link-in T: 6.58 cleanup T: 3.34 c [implicit] str lit bin: 0 lit tri: 0 (by tri: 0) (by stamp: 0) set-var: 0 T: 0.11 T-out: Y c [implicit] sub bin: 0 tri: 0 (stamp: 0, cache: 0) T: 0.19 T-out: Y c Cache cleaned. Updated: 0 K Cleaned: 0 K Freed: 0 K T: 0.01 c [stamp] lit-rem: 0 inv-lit-rem: 0 stamp-cl-rem: 0 c [bintri] lit-rem: 0 cl-sub: 0 c [cache] lit-rem: 0 cl-sub: 0 c [stamp] lit-rem: 0 inv-lit-rem: 0 stamp-cl-rem: 0 c [bintri] lit-rem: 0 cl-sub: 0 c [cache] lit-rem: 0 cl-sub: 0 c [vivif] cache-based irred-- cl tried 20551 cl-sh 0 cl-rem 0 lit-rem 0 time-out Y time: 1.74 c [vivif] cache-based red-- cl tried 2478 cl-sh 0 cl-rem 0 lit-rem 0 time-out Y time: 0.90 c [vivif] asymm (tri+long) useful: 0/159/6061318 lits-rem:0 0-depth-assigns:0 T: 0.73 s time-out: Y c SCC new: 0 T: 0.07 s c [clean] T: 1.9360 s c size4: 5983735 size5: 0 larger: 77583 c [clean] T: 1.7430 s c Doing bust search for 300 conflicts c 300-long burst search learnt units:0 learnt bins: 0 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 174298 32338K 6796 6061K 22K 106K 4.1 2559K 0 0 29.6 c 174299 32342K 6796 6061K 22K 106K 4.1 2563K 0 0 29.7 c 174303 32345K 6796 6061K 22K 106K 4.1 2565K 0 0 29.7 c 174305 32346K 6796 6061K 22K 106K 4.1 2566K 0 0 29.7

Is more than 10 minutes ok or too long?

[msoos]

I think I have just partially fixed this. However, please open a new issue with the offending CNF file and just state that the v-elim is too long. I will then debug, I promise. It is an issue I agree, so it has to be fixed, and I want to fix it. But a nice example file would be useful. Thanks!