Wrong result with --maxsol=x and latest CMS 3.x

[capiman]

Sources used: 7fa2162dffb517f58264ec6deb45bcb7a617b199

Command line used: D:\cryptominisat-18122013\cmsat>cryptominisat64 --bva=0 --maxsol=1000000 --input=solution_brendan_10x10_reduced_test.cnf --in put=f:\10x10\10x10_new_dec2011.cnf --dumpres=10x10_0_to_24_without_bva.res

I got two result, but CNF (according to CMS 2.9.9) has only 1 solution. I was happy to find a second solution, but both found solutions were equal. So it looks like the found solutions is not "filtered out", via AddClause in main.cpp. Perhaps due to the recent changes (veriable remapping), something is not "re-entrant" capable?

Here is the log output, perhaps it is helpful. Both solution were almost found one after the other.

... c 2063 517K 7895 34K 2144 3842K 48.9 94K 1579 287K 416.1 c 2076 519K 7895 34K 2144 3842K 48.9 96K 1580 287K 422.1 c irred prop: 23645K conf: 14K UIP used: 3038K c red prop: 6161K conf: 35K UIP used: 1549K c sum lits visit: 0K cls visit: 0K prop: 29806K conf: 50K UIP used: 4588K c [clean] T: 0.2180 s c [DBclean] Hard long cls limit would be: 9042K c [DBclean] Locked: 500 skipped: 2482 c [DBclean] Pre-removed: 0 clean type will be propconfl c [DBclean] rem 49303 avgGlue 48.68 avgSize 665.89 c [DBclean] remain 49303 avgGlue 11.30 avgSize 183.83 T 0.36 c Using var act-multip 11 instead of standard 11 and act-divider 10 instead of standard 10 c 2078 521K 7895 34K 2144 3842K 48.9 49K 1584 287K 185.7 c 2090 523K 7895 34K 2144 3842K 48.9 51K 1585 287K 203.0 c 2099 525K 7895 34K 2144 3842K 48.9 53K 1587 287K 216.7 c 2105 527K 7894 34K 2144 3842K 48.9 55K 1594 287K 234.3 c 2112 529K 7894 34K 2144 3842K 48.9 57K 1594 287K 252.9 c 2119 531K 7894 34K 2144 3842K 48.9 59K 1596 287K 264.0 c 2130 533K 7894 34K 2144 3842K 48.9 61K 1597 287K 277.3 c rest conf freevar IrrL IrrT IrrB l/c RedL RedT RedB l/c c 2142 535K 7894 34K 2144 3842K 48.9 63K 1597 287K 289.6 c 2144 537K 7894 34K 2144 3842K 48.9 65K 1604 287K 297.4 c 2157 539K 7894 34K 2144 3842K 48.9 67K 1607 287K 305.3 c 2157 541K 7894 34K 2144 3842K 48.9 69K 1610 287K 306.6 c 2163 543K 7894 34K 2144 3842K 48.9 71K 1611 287K 312.6 c 2170 545K 7894 34K 2144 3842K 48.9 73K 1615 287K 322.2 c 2176 547K 7894 34K 2144 3842K 48.9 74K 1618 287K 328.0 s SATISFIABLE v -1 2 -3 -4 ... c Number of solutions found until now: 1 c clause size stats. size4: 1387 size5: 871 larger: 33054 c [clean] T: 0.1870 s c 2184 549K 8052 35K 2149 3933K 49.6 76K 1617 287K 335.8 c Doing burst search for 300 conflicts c 300-long burst search learnt units:0 learnt bins: 1 c percent of negative polarities set: 99.13 % (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 2185 549K 8052 35K 2149 3933K 49.6 76K 1622 287K 336.1 s SATISFIABLE v -1 2 -3 -4 ... c Number of solutions found until now: 2 c clause size stats. size4: 1387 size5: 871 larger: 33051 c [clean] T: 0.2020 s c 2186 549K 8052 35K 2149 3933K 49.8 76K 1622 287K 336.1 c Doing burst search for 300 conflicts c 300-long burst search learnt units:0 learnt bins: 0 c percent of negative polarities set: 99.13 % (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 2187 550K 8052 35K 2149 3933K 49.8 77K 1626 287K 336.1 c new bins since last SCC: 91931 free vars %:1141.72 c [clean] T: 0.1870 s c SCC new: 0 T: 0.03 s c 2195 552K 8052 35K 2149 3933K 49.8 79K 1628 287K 340.7 c 2207 554K 8052 35K 2149 3933K 49.8 81K 1631 287K 348.2 c 2214 556K 8052 35K 2149 3933K 49.8 82K 1632 287K 359.8 c 2226 558K 8052 35K 2149 3933K 49.8 84K 1638 287K 365.7 c 2240 560K 8052 35K 2149 3933K 49.8 86K 1640 287K 374.5 c 2254 562K 8052 35K 2149 3933K 49.8 88K 1642 287K 382.7 c 2263 564K 8052 35K 2149 3933K 49.8 90K 1645 287K 387.6 c 2269 566K 8052 35K 2149 3933K 49.8 92K 1646 287K 391.9

I am currently testing with different CNFs if i can get more clues, or smaller CNF to reproduce the behaviour. I also test same thing with well-known 6x6.cnf which is perhaps easier and faster to reproduce...

[capiman]

I started the same with --bva=1. It has meanwhile found 4 solutions, all 4 solutions are the same. The found solutions are far away, e.g. one found, second one 10 minutes later, so no direct relation with time. Perhaps interesting with --bva=1: The number of variable of result is the original number of variables, without additional variables for bva. Is this correct? At least when doing --maxsol=x, the additional BVA variables are not filtered. Is it correct that BVA are only "output" (i hope you understand what i mean?) variables? But this does not explain, why it also happens when BVA is switched off...

[msoos]

Hmm... okay, gotta look into that!

[capiman]

Many thanks! Just got some timing for this CNF done:

CMS 2.9.9: 5248s CMS 3.x without BVA: 5809s CMS 3.x with BVA: 10208s

Perhaps still something wrong or space for improvement...

I have the 6x6 (one time with BVA, one time without BVA) running overnight. I will post result (correctness and times) tomorrow morning.

[msoos]

BVA variables should not be visible at all from outside. They are not to be worked with from the user's perspective. I don't yet know what to do with dumping the irredundant clause set yet. That dumping is currently WRONG in case you call the solver multiple times with solve() -- i.e. when --maxsol is active or you are using it as a library. As for time to solve, that will be a later issue. But BVA helps immensely with some instances that's for sure.

[capiman]

The 10x10, as well as the 6x6, contains a lot (100 vs. 36) one-at-most, naive implementation with lots of binaries, and some more binaries. I see that bva finds replaceable x. x is now multiple variables with/without '-'? Some days ago i switched on bva_verbosity (or so), I think the "YES" line is the important line? What other information is important? E.g. can I see which part is replaced by which new variable?

For the irred dumping: 1) Do you record, which parts (x in above paragraph) is replaced by which variable? Is it perhaps useful to dump this also to irred file? Could be a useful info also for debugging? 2) Other possibility is perhaps to reverse BVA, so only original variables are in irred file. Advantage if you just dump them is that irred file can be used with other SAT solver (or CMS 2.9.9), so it gets possibility to work with BVA. Disadvantage is that sometimes it is useful to concatenate CNFs and with additional variables, this is not so easy possible. One must check, if both CNF use common lower vars, but different BVA vars. Example: I have a CNF which calculates for 2000 variable but is only a part of a bigger CNF with 3000 or even 9000 variables. So when BVA add variables around 2001 and upper this collides with existing variables at 2001 and upper. But it would be possible to move them (by hand or tool) to 9001 or higher. (Command line for selecting one of both ways?)

[capiman]

--maxsol and --dumpirred (at the same time) is always a bit tricky, because in clauses the found results were already removed. But this was already in this way before BVA.

[capiman]

The fastest way I found so far is using the following command line (some options perhaps not needed due to default settings): cryptominisat64test1 --bva=1 --renumber=1 --maxsol=1000 --input=f:\6x6\6x6.cnf --dumpres=6x6_new_1_test1.res (It is using the well-known 6x6.cnf used also in other bug reports)

I have added the following code, directly after addClauseOuter (line 989, there is only one in main.cpp). It aborts after 14 solutions (of total 260), whereas solution 14 is same as solutions 13:

            // Start of Duplicate Check
            {
                static vector<vector<Lit>> solutions;

                solutions.push_back(lits);

                size_t j = solutions.size() - 1;

                for(size_t i = 0; i < j; i++)
                {
                    size_t k;
                    for(k = 0; k < solutions[i].size(); k++)
                    {
                        if(solutions[i][k] != solutions[j][k]) break;
                    }
                    if(k == solutions[i].size())
                    {
                        cout << "Duplicate solution!!! (i=" << i << ", j=" << j << ")" << endl;
                        exit(1);
                    }
                }
            }
            // End of Duplicate Check

c Outputting solution to console c CryptoMiniSat version MinGW64-compiled, without GIT c compiled with gcc version 4.7.3 c Executed with command line:cryptominisat64test1 --bva=1 --renumber=1 --maxsol=1000 --input=f:\6x6\6x6.cnf --dumpres=6x6_new_1_test1.res c Reading file 'f:\6x6\6x6.cnf' c WARNING: Empty line at line number 1 -- this is not part of the DIMACS specifications. Ignoring. c WARNING: Empty line at line number 8 -- this is not part of the DIMACS specifications. Ignoring. c WARNING: Empty line at line number 10 -- this is not part of the DIMACS specifications. Ignoring. c WARNING: Empty line at line number 156723 -- this is not part of the DIMACS specifications. Ignoring. c -- clauses added: 155432 irredundant c -- vars added 1280 c Parsing time: 0.16 s c clause size stats. size4: 4 size5: 0 larger: 32 c [clean] T: 0.0160 s c 0 0 1280 36 0 155K 35.6 0 0 0 -1.$ c Doing burst search for 300 conflicts c 300-long burst search learnt units:0 learnt bins: 14 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 1 302 1280 36 0 155K 35.6 268 20 14 69.0 c new bins since last SCC: 155412 free vars %:12141.56 c [clean] T: 0.0000 s c SCC new: 0 T: 0.00 s c new bins since last SCC: 27 free vars %:2.11 c [clean] T: 0.0000 s c SCC new: 0 T: 0.00 s c 18 2303 1280 36 0 155K 35.6 2094 135 50 101.5 c new bins since last SCC: 32 free vars %:2.50 c [clean] T: 0.0000 s c SCC new: 0 T: 0.00 s c new bins since last SCC: 26 free vars %:2.03 c [clean] T: 0.0150 s c SCC new: 0 T: 0.00 s c 27 4304 1280 36 0 155K 35.6 3898 240 108 108.2 c new bins since last SCC: 31 free vars %:2.43 c [clean] T: 0.0000 s c SCC new: 0 T: 0.00 s c 38 6305 1278 36 0 154K 35.5 5751 310 146 115.4 c new bins since last SCC: 26 free vars %:2.03 c [clean] T: 0.0000 s c SCC new: 0 T: 0.02 s c 53 8306 1278 36 0 154K 35.5 7656 352 169 122.0 c irred prop: 14K conf: 3K UIP used: 10K c red prop: 222K conf: 5K UIP used: 44K c sum lits visit: 0K cls visit: 0K prop: 236K conf: 8K UIP used: 54K c [clean] T: 0.0160 s c [DBclean] Hard long cls limit would be: 16K c [DBclean] Locked: 500 skipped: 0 c [DBclean] Pre-removed: 0 clean type will be propconfl c [DBclean] rem 0 avgGlue -1.#J avgSize -1.#J c [DBclean] remain 9272 avgGlue 19.15 avgSize 125.02 T 0.01 c Using var act-multip 11 instead of standard 11 and act-divider 10 instead of standard 10 c new bins since last SCC: 27 free vars %:2.11 c [clean] T: 0.0000 s c SCC new: 0 T: 0.00 s c 63 10307 1278 36 0 154K 35.5 9566 386 184 124.4 c 66 12308 1278 36 0 154K 35.5 11463 420 206 121.2 c new bins since last SCC: 27 free vars %:2.12 c [clean] T: 0.0160 s c SCC new: 0 T: 0.00 s c 78 14309 1276 36 0 154K 35.4 13365 450 223 127.3 c 93 16310 1275 36 0 154K 35.4 15283 476 233 130.6 c new bins since last SCC: 26 free vars %:2.04 c [clean] T: 0.0150 s c SCC new: 0 T: 0.00 s c 106 18311 1274 36 0 154K 35.4 17198 503 251 135.5 s SATISFIABLE v ... c Number of solutions found until now: 1 MM: solver->nVarsOutside()=1280 c clause size stats. size4: 4 size5: 0 larger: 33 c [clean] T: 0.0160 s c 107 18504 1274 37 0 153K 68.9 17383 505 252 135.9 c Doing burst search for 300 conflicts c 300-long burst search learnt units:0 learnt bins: 2 c percent of negative polarities set: 96.75 % (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 108 18806 1274 37 0 153K 68.9 17672 515 254 135.2 c new bins since last SCC: 28 free vars %:2.20 c [clean] T: 0.0150 s c SCC new: 0 T: 0.00 s c 118 20K 1273 37 0 153K 68.8 19604 536 268 139.4 c 127 22K 1271 37 0 153K 68.8 21K 546 284 142.1 c new bins since last SCC: 26 free vars %:2.05 c [clean] T: 0.0160 s c SCC new: 0 T: 0.00 s c 136 24K 1271 37 0 153K 68.7 23K 566 301 143.2 c 139 26K 1270 37 0 153K 68.7 25K 587 308 144.2 c new bins since last SCC: 29 free vars %:2.28 c [clean] T: 0.0150 s c SCC new: 0 T: 0.00 s c 144 28K 1270 37 0 152K 68.6 27K 592 313 144.5 c irred prop: 10K conf: 1K UIP used: 6K c red prop: 970K conf: 15K UIP used: 222K c sum lits visit: 0K cls visit: 0K prop: 981K conf: 17K UIP used: 229K c [clean] T: 0.0150 s c [DBclean] Hard long cls limit would be: 32K c [DBclean] Locked: 500 skipped: 292 c [DBclean] Pre-removed: 0 clean type will be propconfl c [DBclean] rem 14227 avgGlue 25.73 avgSize 169.52 c [DBclean] remain 14228 avgGlue 14.56 avgSize 120.98 T 0.05 c Using var act-multip 11 instead of standard 11 and act-divider 10 instead of standard 10 c 156 30K 1270 37 0 152K 68.6 15015 601 323 125.6 c 166 32K 1270 37 0 152K 68.6 16921 623 331 130.3 c new bins since last SCC: 26 free vars %:2.05 c [clean] T: 0.0000 s c SCC new: 0 T: 0.02 s c 172 34K 1270 37 0 152K 68.6 18851 636 340 135.4 c 183 36K 1270 37 0 152K 68.6 20K 641 343 139.2 s SATISFIABLE v ... c Number of solutions found until now: 2 MM: solver->nVarsOutside()=1280 c clause size stats. size4: 4 size5: 0 larger: 34 c [clean] T: 0.0160 s c 192 37K 1270 38 0 152K 100.3 21K 643 347 141.4 c Doing burst search for 300 conflicts c 300-long burst search learnt units:0 learnt bins: 2 c percent of negative polarities set: 96.52 % (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 193 37K 1270 38 0 152K 100.3 21K 647 349 141.2 c 200 39K 1270 38 0 152K 100.3 23K 656 354 147.1 c 213 41K 1270 38 0 152K 100.3 25K 667 356 151.1 c 230 43K 1270 38 0 152K 100.3 27K 674 360 156.0 c 244 45K 1270 38 0 152K 100.3 29K 681 363 160.1 c new bins since last SCC: 26 free vars %:2.05 c [clean] T: 0.0310 s c SCC new: 0 T: 0.00 s c 255 47K 1270 38 0 152K 100.3 31K 692 368 163.6 c 256 49K 1270 38 0 152K 100.3 33K 701 375 164.6 c irred prop: 5K conf: 0K UIP used: 3K c red prop: 1289K conf: 16K UIP used: 313K c sum lits visit: 0K cls visit: 0K prop: 1294K conf: 16K UIP used: 316K c [clean] T: 0.0150 s c [DBclean] Hard long cls limit would be: 48K c [DBclean] Locked: 500 skipped: 664 c [DBclean] Pre-removed: 0 clean type will be propconfl c [DBclean] rem 16786 avgGlue 24.98 avgSize 191.46 c [DBclean] remain 16786 avgGlue 20.42 avgSize 137.73 T 0.08 c Using var act-multip 11 instead of standard 11 and act-divider 10 instead of standard 10 c 267 51K 1270 38 0 152K 100.3 18715 709 379 147.9 c 283 53K 1270 38 0 152K 100.3 20K 719 383 155.2 s SATISFIABLE v ... c Number of solutions found until now: 3 MM: solver->nVarsOutside()=1280 c clause size stats. size4: 4 size5: 0 larger: 35 c [clean] T: 0.0150 s c 289 54K 1270 39 0 152K 130.3 21K 721 383 157.9 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.41 % (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 290 55K 1270 39 0 152K 130.3 21K 722 383 157.6 s SATISFIABLE v ... c Number of solutions found until now: 4 MM: solver->nVarsOutside()=1280 c clause size stats. size4: 4 size5: 0 larger: 36 c [clean] T: 0.0150 s c 291 55K 1270 40 0 152K 158.8 21K 722 383 157.6 c Doing burst search for 300 conflicts c 300-long burst search learnt units:0 learnt bins: 1 c percent of negative polarities set: 96.41 % (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 292 55K 1270 40 0 152K 158.8 22K 723 384 157.3 c 295 57K 1270 40 0 152K 158.8 24K 728 387 160.7 c new bins since last SCC: 28 free vars %:2.20 c [clean] T: 0.0150 s c SCC new: 0 T: 0.00 s c 302 59K 1270 40 0 152K 158.8 26K 739 394 163.1 c 308 61K 1270 40 0 152K 158.8 27K 749 397 166.6 c 317 63K 1270 40 0 152K 158.8 29K 753 401 169.1 c 330 65K 1270 40 0 152K 158.8 31K 756 406 172.8 c 344 67K 1269 40 0 152K 158.8 33K 763 411 177.4 s SATISFIABLE v ... c Number of solutions found until now: 5 MM: solver->nVarsOutside()=1280 c clause size stats. size4: 4 size5: 0 larger: 37 c [clean] T: 0.0310 s c 346 67K 1269 41 0 152K 185.7 34K 763 410 177.9 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.33 % (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 347 68K 1269 41 0 152K 185.7 34K 763 413 177.9 s SATISFIABLE v ... c Number of solutions found until now: 6 MM: solver->nVarsOutside()=1280 c clause size stats. size4: 4 size5: 0 larger: 38 c [clean] T: 0.0310 s c 348 68K 1269 42 0 152K 211.5 34K 763 413 177.9 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.33 % (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 349 68K 1269 42 0 152K 211.5 34K 767 413 177.6 c 356 70K 1269 42 0 152K 211.5 36K 778 417 179.3 c new bins since last SCC: 27 free vars %:2.13 c [clean] T: 0.0160 s c SCC new: 0 T: 0.02 s c 366 72K 1269 42 0 152K 211.5 38K 783 420 180.9 c 374 74K 1269 42 0 152K 211.5 40K 793 422 182.2 c 386 76K 1269 42 0 152K 211.5 42K 799 423 183.2 c 394 78K 1269 42 0 152K 211.5 44K 804 429 184.2 c 396 80K 1269 42 0 152K 211.5 46K 812 431 184.5 c new bins since last SCC: 110 free vars %:8.68 c [clean] T: 0.0320 s c SCC new: 0 T: 0.00 s c 407 82K 1268 42 0 152K 211.3 47K 819 432 185.7 c 415 84K 1268 42 0 152K 211.3 49K 828 433 186.6 c 421 86K 1268 42 0 152K 211.3 51K 837 436 188.0 c rest conf freevar IrrL IrrT IrrB l/c RedL RedT RedB l/c c 428 88K 1268 42 0 152K 211.3 53K 846 440 189.3 c 443 90K 1268 42 0 152K 211.3 55K 850 440 190.9 c 447 92K 1268 42 0 152K 211.3 57K 854 441 191.5 c 455 94K 1268 42 0 152K 211.3 59K 860 445 192.9 c 466 96K 1268 42 0 152K 211.3 61K 865 447 194.3 c 468 98K 1268 42 0 152K 211.3 63K 869 449 194.0 c irred prop: 7K conf: 0K UIP used: 3K c red prop: 3853K conf: 43K UIP used: 965K c sum lits visit: 0K cls visit: 0K prop: 3861K conf: 44K UIP used: 969K c [clean] T: 0.0620 s c [DBclean] Hard long cls limit would be: 64K c [DBclean] Locked: 500 skipped: 1019 c [DBclean] Pre-removed: 0 clean type will be propconfl c [DBclean] rem 32406 avgGlue 35.69 avgSize 256.15 c [DBclean] remain 32406 avgGlue 15.07 avgSize 135.23 T 0.14 c Using var act-multip 11 instead of standard 11 and act-divider 10 instead of standard 10 c 475 100K 1268 42 0 152K 211.3 32K 870 450 136.4 c 489 102K 1268 42 0 152K 211.3 34K 874 451 141.2 c 497 104K 1268 42 0 152K 211.3 36K 875 453 147.6 c 509 106K 1268 42 0 152K 211.3 38K 879 454 152.4 c rest conf freevar IrrL IrrT IrrB l/c RedL RedT RedB l/c c 518 108K 1268 42 0 152K 211.3 40K 883 456 154.3 s SATISFIABLE v ... c Number of solutions found until now: 7 MM: solver->nVarsOutside()=1280 c clause size stats. size4: 4 size5: 0 larger: 39 c [clean] T: 0.0150 s c 534 109K 1268 43 0 152K 235.9 42K 885 457 157.5 c Doing burst search for 300 conflicts c 300-long burst search learnt units:0 learnt bins: 1 c percent of negative polarities set: 96.19 % (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 535 110K 1268 43 0 152K 235.9 42K 886 458 157.7 c new bins since last SCC: 26 free vars %:2.05 c [clean] T: 0.0310 s c SCC new: 0 T: 0.00 s c 549 112K 1268 43 0 152K 235.9 44K 887 458 161.7 c 564 114K 1268 43 0 152K 235.9 46K 888 460 165.3 c 572 116K 1268 43 0 152K 235.9 48K 899 460 167.4 c 583 118K 1268 43 0 152K 235.9 50K 908 464 169.7 c irred prop: 2K conf: 0K UIP used: 1K c red prop: 1718K conf: 17K UIP used: 441K c sum lits visit: 0K cls visit: 0K prop: 1720K conf: 17K UIP used: 443K c [clean] T: 0.0310 s c [DBclean] Hard long cls limit would be: 81K c [DBclean] Locked: 500 skipped: 1355 c [DBclean] Pre-removed: 0 clean type will be propconfl c [DBclean] rem 25842 avgGlue 31.20 avgSize 220.28 c [DBclean] remain 25843 avgGlue 19.16 avgSize 126.23 T 0.11 c Using var act-multip 11 instead of standard 11 and act-divider 10 instead of standard 10 c 594 120K 1268 43 0 152K 235.9 26K 909 467 127.0 c 602 122K 1268 43 0 152K 235.9 28K 911 471 135.6 c 611 124K 1268 43 0 152K 235.9 29K 920 472 139.0 c 626 126K 1268 43 0 152K 235.9 31K 922 474 145.9 c 636 128K 1268 43 0 152K 235.9 33K 929 477 150.8 c irred prop: 1K conf: 0K UIP used: 0K c red prop: 892K conf: 8K UIP used: 234K c sum lits visit: 0K cls visit: 0K prop: 893K conf: 8K UIP used: 234K c [clean] T: 0.0160 s c [DBclean] Hard long cls limit would be: 97K c [DBclean] Locked: 500 skipped: 1638 c [DBclean] Pre-removed: 0 clean type will be propconfl c [DBclean] rem 17729 avgGlue 26.26 avgSize 169.09 c [DBclean] remain 17730 avgGlue 21.37 avgSize 141.15 T 0.08 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 644 130K 1268 43 0 152K 235.9 17993 936 477 143.0 c 656 132K 1268 43 0 152K 235.9 19931 938 479 149.7 c 668 134K 1268 43 0 152K 235.9 21K 940 480 157.4 s SATISFIABLE v ... c Number of solutions found until now: 8 MM: solver->nVarsOutside()=1280 c clause size stats. size4: 4 size5: 0 larger: 40 c [clean] T: 0.0160 s c 674 135K 1268 44 0 152K 259.4 22K 945 481 162.7 c Doing burst search for 300 conflicts c 300-long burst search learnt units:0 learnt bins: 1 c percent of negative polarities set: 96.15 % (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 675 135K 1268 44 0 152K 259.4 23K 946 482 163.0 c 683 137K 1268 44 0 152K 259.4 25K 952 483 168.8 c new bins since last SCC: 26 free vars %:2.05 c [clean] T: 0.0160 s c SCC new: 0 T: 0.00 s c 696 139K 1268 44 0 152K 259.4 27K 955 486 173.7 c 711 141K 1268 44 0 152K 259.4 29K 957 489 179.1 c 726 143K 1268 44 0 152K 259.4 30K 961 489 184.1 c 735 145K 1268 44 0 152K 259.4 32K 965 490 188.1 c 745 147K 1268 44 0 152K 259.4 34K 971 494 190.6 s SATISFIABLE v ... c Number of solutions found until now: 9 MM: solver->nVarsOutside()=1280 c clause size stats. size4: 4 size5: 0 larger: 41 c [clean] T: 0.0160 s c 749 148K 1268 45 0 152K 281.8 35K 972 497 193.1 c Doing burst search for 300 conflicts c 300-long burst search learnt units:0 learnt bins: 0 s SATISFIABLE v ... c Number of solutions found until now: 10 MM: solver->nVarsOutside()=1280 c clause size stats. size4: 4 size5: 0 larger: 42 c [clean] T: 0.0150 s c 750 148K 1268 46 0 152K 303.2 35K 972 497 193.1 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.14 % (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 751 148K 1268 46 0 152K 303.2 36K 972 497 192.8 s SATISFIABLE v ... c Number of solutions found until now: 11 MM: solver->nVarsOutside()=1280 c clause size stats. size4: 4 size5: 0 larger: 43 c [clean] T: 0.0310 s c 753 150K 1268 47 0 152K 323.7 37K 976 497 193.6 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.13 % (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 754 151K 1268 47 0 152K 323.7 38K 977 500 193.5 c 761 153K 1268 47 0 152K 323.7 40K 979 502 196.5 s SATISFIABLE v ... c Number of solutions found until now: 12 MM: solver->nVarsOutside()=1280 c clause size stats. size4: 4 size5: 0 larger: 44 c [clean] T: 0.0310 s c 763 153K 1268 48 0 152K 343.4 40K 979 502 196.7 c Doing burst search for 300 conflicts c 300-long burst search learnt units:0 learnt bins: 2 c percent of negative polarities set: 96.12 % (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 764 153K 1268 48 0 152K 343.4 40K 984 504 196.3 c 769 155K 1268 48 0 152K 343.4 42K 993 506 198.9 c 780 157K 1268 48 0 152K 343.4 44K 1002 508 200.5 c new bins since last SCC: 27 free vars %:2.13 c [clean] T: 0.0320 s c SCC new: 0 T: 0.00 s c 796 159K 1268 48 0 152K 343.4 46K 1005 511 202.9 c 807 161K 1268 48 0 152K 343.4 48K 1011 511 204.7 c 819 163K 1268 48 0 152K 343.4 50K 1015 512 205.9 c 827 165K 1268 48 0 152K 343.4 52K 1018 514 207.1 c 829 167K 1268 48 0 152K 343.4 54K 1020 515 207.3 c 834 169K 1268 48 0 152K 343.4 55K 1023 518 207.1 c 843 171K 1268 48 0 152K 343.4 57K 1025 520 207.2 c rest conf freevar IrrL IrrT IrrB l/c RedL RedT RedB l/c c 854 173K 1268 48 0 152K 343.4 59K 1026 521 209.1 c 858 175K 1268 48 0 152K 343.4 61K 1028 525 209.5 c 865 177K 1268 48 0 152K 343.4 63K 1030 526 209.8 c 873 179K 1268 48 0 152K 343.4 65K 1030 527 209.8 c 873 181K 1268 48 0 152K 343.4 67K 1031 528 209.6 c 892 183K 1268 48 0 152K 343.4 69K 1034 532 210.3 c 906 185K 1268 48 0 152K 343.4 71K 1039 532 211.6 c 922 187K 1268 48 0 152K 343.4 73K 1041 532 212.8 c 930 189K 1268 48 0 152K 343.4 75K 1041 533 213.4 c irred prop: 8K conf: 0K UIP used: 4K c red prop: 5334K conf: 53K UIP used: 1359K c sum lits visit: 0K cls visit: 0K prop: 5343K conf: 54K UIP used: 1363K c [clean] T: 0.0630 s c [DBclean] Hard long cls limit would be: 113K c [DBclean] Locked: 500 skipped: 2035 c [DBclean] Pre-removed: 0 clean type will be propconfl c [DBclean] rem 38270 avgGlue 42.98 avgSize 284.12 c [DBclean] remain 38271 avgGlue 22.62 avgSize 142.85 T 0.16 c Using var act-multip 11 instead of standard 11 and act-divider 10 instead of standard 10 c 939 191K 1268 48 0 152K 343.4 38K 1042 534 144.2 c rest conf freevar IrrL IrrT IrrB l/c RedL RedT RedB l/c c 948 193K 1268 48 0 152K 343.4 40K 1043 534 149.9 c 962 195K 1268 48 0 152K 343.4 42K 1043 534 155.9 c 969 197K 1268 48 0 152K 343.4 44K 1048 536 159.3 c new bins since last SCC: 27 free vars %:2.13 c [clean] T: 0.0310 s c SCC new: 0 T: 0.00 s c 977 199K 1268 48 0 152K 343.4 46K 1049 538 162.5 c irred prop: 1K conf: 0K UIP used: 0K c red prop: 885K conf: 8K UIP used: 229K c sum lits visit: 0K cls visit: 0K prop: 886K conf: 8K UIP used: 229K c [clean] T: 0.0310 s c [DBclean] Hard long cls limit would be: 130K c [DBclean] Locked: 500 skipped: 1962 c [DBclean] Pre-removed: 0 clean type will be propconfl c [DBclean] rem 23951 avgGlue 33.83 avgSize 201.78 c [DBclean] remain 23952 avgGlue 16.28 avgSize 129.40 T 0.09 c Using var act-multip 11 instead of standard 11 and act-divider 10 instead of standard 10 c 986 201K 1268 48 0 152K 343.4 24K 1050 538 131.3 c 999 203K 1268 48 0 152K 343.4 26K 1050 540 139.5 c 1004 205K 1268 48 0 152K 343.4 28K 1055 541 143.8 c 1011 207K 1268 48 0 152K 343.4 30K 1058 541 149.8 c 1016 209K 1268 48 0 152K 343.4 32K 1060 541 155.2 c 1030 211K 1268 48 0 152K 343.4 34K 1061 541 160.8 c recursive minimization cost OK: 4864Kcost/(% lits removed) c more minimization effectiveness good: 14.23 % --> increasing limit to 800 c irred prop: 1K conf: 0K UIP used: 0K c red prop: 986K conf: 9K UIP used: 258K c sum lits visit: 0K cls visit: 0K prop: 987K conf: 9K UIP used: 259K c [clean] T: 0.0160 s c [DBclean] Hard long cls limit would be: 146K c [DBclean] Locked: 500 skipped: 2169 c [DBclean] Pre-removed: 0 clean type will be propconfl c [DBclean] rem 17247 avgGlue 24.33 avgSize 179.71 c [DBclean] remain 17247 avgGlue 21.07 avgSize 144.70 T 0.08 c [clean] T: 0.0150 s c [clean] T: 0.0160 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 [comp] Found component(s): 1 BP: 0.47M time: 0.05 s c Cache cleaned. Updated: 0 K Cleaned: 0 K Freed: 1 K T: 0.00 c [bcache] 0-depth ass: 0 BXprop: 0 T: 0.00 c [impl sub] bin: 0 tri: 14 (stamp: 0, cache: 0) T: 0.05 T-out: N w-visit: 2560 c [probe] lits : 2.51M act vars: 1.27K BP+HP todo: 2280.00M c [clean] T: 0.0150 s c [probe] NumProps after perf multi: 2280.00M after numcall multi: 2280.00M (<- final) c [probe] time spent updating cache during probing: 0.6% c [clean] T: 0.0150 s c [probe] 0-depth assigns: 1 bsame: 0 Flit: 1 Visited: 2535/2536(100.0%) c [probe] probed: 2489(98.1%) hyperBin:40503 transR-Irred:0 transR-Red:182 c [probe] BP: 232.7M HP: 92.0M T: 1.70 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: 4 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: 10 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: 324 cl-sub: 0 c [cl-str] cache-based lit-rem: 9554 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: 31785 cl-sub: 33 c [cl-str] cache-based lit-rem: 564751 cl-sub: 0 c [asymm] longirred tried: 44/44 cl-rem:8 lits-rem:142 T: 0.06 T-out: N c [vivif] cache-based irred-- cl tried 44 cl-sh 8 cl-rem 0 lit-rem 9878 T-out N T: 0.00 c [vivif] cache-based red-- cl tried 17235 cl-sh 12260 cl-rem 33 lit-rem 596536 T-out N T: 0.84 c [vivif] asymm (tri+long) useful: 8/44/44 lits-rem: 142 0-depth-assigns: 0 T: 0.06 s T-out: N c [impl sub] bin: 4588 tri: 26 (stamp: 0, cache: 0) T: 0.06 T-out: N w-visit: 2560 c SCC new: 0 T: 0.00 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 0 MB c [simp] mem usage for occur of red 29 MB c [simp] Not linked in red 3578/17185 (20.82 %) c Mem for watch alloc : 13 MB (1.#J %) c Mem for watch array : 0 MB (1.#J %) c [sub] rem cl: 1978 tried: 25844/17229 (150.0%) T: 0.4 T-out: N c [str] sub: 133 str: 16452 tried: 32100/17229 (186.3%) T: 0.7 T-out: Y c Empty resolvent elimed: 0 T:0.0 T-out: N c #try to eliminate: 1267 c #var-elim: 36 c #T-out: N c #T: 0.7 c [impl sub] bin: 0 tri: 0 (stamp: 0, cache: 0) T: 0.05 T-out: N w-visit: 2560 c [bva] added: 568 simp: 101368 T: 6.68 T-out: Y c [gate] found irred:0 avg-s: -1.$ red: 0 T: 0.00 T-out: N c [gate] shorten cl: 0 l-rem: 0 T: 0.00 T-out: N c [gate] rem cl: 0 avg s: -1.#J T: 0.00 T-out: N c [gate] eqlit v-rep: 0 T: 0.00 c [clean] T: 0.0000 s c [occur] 0.0630 is overhead c [v-elim] elimed: 36 / 152 / 1267 T: 0.67 s T-out: N c [v-elim] cl-new: 4645 tried: 36 tested: 1267 (100.00 % agressive) c [v-elim] subs: 0 red-bin rem: 1090 red-tri rem: 245 red-long rem: 6202 v-fix: 0 c [simp] link-in T: 0.05 cleanup T: 0.02 c [implicit] str lit bin: 0 lit tri: 31 (by tri: 0) (by stamp: 1) set-var: 0 T: 0.02 T-out: N w-visit: 3696 c [impl sub] bin: 30 tri: 0 (stamp: 0, cache: 0) T: 0.02 T-out: N w-visit: 3696 c Cache cleaned. Updated: 0 K Cleaned: 7 K Freed: 10 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: 0 cl-sub: 231 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: 1 c [cl-str] cache-based lit-rem: 0 cl-sub: 0 c [cl-str] stamp-based lit-rem: 3 inv-lit-rem: 0 stamp-cl-rem: 0 c [cl-str] bintri-based lit-rem: 1922 cl-sub: 0 c [cl-str] cache-based lit-rem: 92238 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: 63 cl-sub: 0 c [cl-str] cache-based lit-rem: 0 cl-sub: 0 c [asymm] longirred tried: 2927/2927 cl-rem:354 lits-rem:3514 T: 0.56 T-out: N c [vivif] cache-based irred-- cl tried 2968 cl-sh 2719 cl-rem 0 lit-rem 94163 T-out N T: 0.06 c [vivif] cache-based red-- cl tried 5326 cl-sh 46 cl-rem 0 lit-rem 63 T-out N T: 0.05 c [vivif] asymm (tri+long) useful: 354/2927/2927 lits-rem: 3514 0-depth-assigns: 0 T: 0.56 s T-out: N c SCC new: 0 T: 0.02 s c Cache cleaned. Updated: 0 K Cleaned: 0 K Freed: 0 K T: 0.00 c [clean] T: 0.0160 s c calculated reachability. T: 0.000 c clause size stats. size4: 160 size5: 146 larger: 2621 c [clean] T: 0.0000 s c 1033 212K 1799 2927 208 46K 19.7 5326 593 35K 25.2 c Doing burst search for 300 conflicts c 300-long burst search learnt units:0 learnt bins: 4 c percent of negative polarities set: 96.04 % (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 1034 212K 1799 2927 208 46K 19.7 5612 603 35K 28.1 c 1038 214K 1799 2927 208 46K 19.7 7566 620 35K 54.1 c 1040 216K 1799 2927 208 46K 19.7 9526 625 35K 72.3 c 1042 218K 1799 2927 208 46K 19.7 11462 636 35K 78.8 c 1043 220K 1799 2927 208 46K 19.7 13440 639 35K 84.6 c 1048 222K 1799 2927 208 46K 19.7 15394 650 35K 92.5 c irred prop: 408K conf: 2K UIP used: 61K c red prop: 557K conf: 5K UIP used: 143K c sum lits visit: 0K cls visit: 0K prop: 966K conf: 8K UIP used: 205K c [clean] T: 0.0160 s c [DBclean] Hard long cls limit would be: 523K c [DBclean] Locked: 500 skipped: 1268 c [DBclean] Pre-removed: 0 clean type will be propconfl c [DBclean] rem 4162 avgGlue 16.60 avgSize 78.01 c [DBclean] remain 12998 avgGlue 14.60 avgSize 100.12 T 0.03 c Using var act-multip 11 instead of standard 11 and act-divider 10 instead of standard 10 c 1051 224K 1799 2927 208 46K 19.7 13204 656 35K 100.6 c 1054 226K 1799 2927 208 46K 19.7 15150 667 35K 107.9 c 1055 228K 1799 2927 208 46K 19.7 17104 670 35K 108.7 c 1061 230K 1799 2927 208 46K 19.7 19063 679 35K 110.6 c rest conf freevar IrrL IrrT IrrB l/c RedL RedT RedB l/c c 1063 232K 1799 2927 208 46K 19.7 21K 703 35K 112.9 c 1065 234K 1799 2927 208 46K 19.7 22K 710 35K 114.8 c 1065 236K 1799 2927 208 46K 19.7 24K 720 35K 114.4 c irred prop: 736K conf: 3K UIP used: 116K c red prop: 354K conf: 6K UIP used: 113K c sum lits visit: 0K cls visit: 0K prop: 1090K conf: 9K UIP used: 230K c [clean] T: 0.0160 s c [DBclean] Hard long cls limit would be: 575K c [DBclean] Locked: 500 skipped: 1310 c [DBclean] Pre-removed: 0 clean type will be propconfl c [DBclean] rem 12573 avgGlue 19.44 avgSize 134.36 c [DBclean] remain 13440 avgGlue 14.13 avgSize 98.44 T 0.05 c Using var act-multip 11 instead of standard 11 and act-divider 10 instead of standard 10 c 1068 238K 1799 2927 208 46K 19.7 14326 727 35K 98.9 c 1069 240K 1799 2927 208 46K 19.7 16274 733 35K 98.7 c 1069 242K 1799 2927 208 46K 19.7 18224 736 35K 99.6 c 1072 244K 1799 2927 208 46K 19.7 20K 748 35K 99.8 c 1073 246K 1799 2927 208 46K 19.7 22K 750 35K 101.9 c 1079 248K 1799 2927 208 46K 19.7 24K 756 35K 104.7 c 1081 250K 1799 2927 208 46K 19.7 26K 771 35K 105.6 c recursive minimization cost OK: 1490Kcost/(% lits removed) c more minimization effectiveness good: 25.51 % --> increasing limit to 800 c irred prop: 821K conf: 3K UIP used: 125K c red prop: 469K conf: 7K UIP used: 143K c sum lits visit: 0K cls visit: 0K prop: 1290K conf: 10K UIP used: 269K c [clean] T: 0.0160 s c [DBclean] Hard long cls limit would be: 628K c [DBclean] Locked: 500 skipped: 1787 c [DBclean] Pre-removed: 0 clean type will be propconfl c [DBclean] rem 13808 avgGlue 18.68 avgSize 122.51 c [DBclean] remain 13931 avgGlue 14.22 avgSize 88.19 T 0.05 c SCC new: 0 T: 0.00 s c Cache cleaned. Updated: 0 K Cleaned: 0 K Freed: 0 K T: 0.00 c [bcache] 0-depth ass: 0 BXprop: 0 T: 0.01 c [impl sub] bin: 0 tri: 6 (stamp: 0, cache: 0) T: 0.02 T-out: N w-visit: 3598 c [probe] lits : 1.29M act vars: 1.80K BP+HP todo: 2736.00M c [clean] T: 0.0150 s c [probe] NumProps after perf multi: 1368.00M after numcall multi: 1571.42M (<- final) c [probe] time spent updating cache during probing: 1.3% c [probe] 0-depth assigns: 0 bsame: 0 Flit: 0 Visited: 3598/3598(100.0%) c [probe] probed: 2620(72.8%) hyperBin:19149 transR-Irred:1008 transR-Red:2851 c [probe] BP: 110.2M HP: 25.9M T: 0.83 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: 300 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: 37 cl-sub: 0 c [cl-str] cache-based lit-rem: 101 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: 8212 cl-sub: 1 c [cl-str] cache-based lit-rem: 265589 cl-sub: 0 c [asymm] longirred tried: 1038/2924 cl-rem:5 lits-rem:6 T: 0.39 T-out: Y c [vivif] cache-based irred-- cl tried 2925 cl-sh 87 cl-rem 0 lit-rem 138 T-out N T: 0.06 c [vivif] cache-based red-- cl tried 13631 cl-sh 5797 cl-rem 1 lit-rem 273801 T-out N T: 0.42 c [vivif] asymm (tri+long) useful: 5/1038/2924 lits-rem: 6 0-depth-assigns: 0 T: 0.39 s T-out: Y c [impl sub] bin: 11826 tri: 2 (stamp: 0, cache: 1) T: 0.02 T-out: N w-visit: 3598 c SCC new: 0 T: 0.00 s c [clean] T: 0.0160 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.0000 s c [simp] mem usage for occur of irred 1 MB c [simp] mem usage for occur of red 14 MB c [simp] Not linked in red 937/13627 (6.88 %) c Mem for watch alloc : 10 MB (1.#J %) c Mem for watch array : 0 MB (1.#J %) c [sub] rem cl: 2511 tried: 24827/16551 (150.0%) T: 0.3 T-out: N c [str] sub: 152 str: 11645 tried: 40308/16551 (243.5%) T: 0.7 T-out: Y c Empty resolvent elimed: 0 T:0.0 T-out: N c #try to eliminate: 1799 c #var-elim: 0 c #T-out: N c #T: 0.2 c [impl sub] bin: 0 tri: 0 (stamp: 0, cache: 0) T: 0.03 T-out: N w-visit: 3598 c [bva] added: 1859 simp: 24418 T: 0.89 T-out: N c [gate] found irred:0 avg-s: -1.$ red: 0 T: 0.02 T-out: N c [gate] shorten cl: 0 l-rem: 0 T: 0.00 T-out: N c [gate] rem cl: 0 avg s: -1.#J T: 0.00 T-out: N c [gate] eqlit v-rep: 0 T: 0.00 c [clean] T: 0.0000 s c [occur] 0.0790 is overhead c [v-elim] elimed: 0 / 322 / 1799 T: 0.16 s T-out: N c [v-elim] cl-new: 0 tried: 0 tested: 1799 (100.00 % agressive) c [v-elim] subs: 0 red-bin rem: 0 red-tri rem: 0 red-long rem: 0 v-fix: 0 c [simp] link-in T: 0.06 cleanup T: 0.02 c [implicit] str lit bin: 0 lit tri: 9 (by tri: 0) (by stamp: 2) set-var: 0 T: 0.02 T-out: N w-visit: 7316 c [impl sub] bin: 9 tri: 0 (stamp: 0, cache: 0) T: 0.02 T-out: N w-visit: 7316 c Cache cleaned. Updated: 0 K Cleaned: 0 K Freed: 0 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: 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: 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: 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: 0 c [cl-str] cache-based lit-rem: 0 cl-sub: 0 c [asymm] longirred tried: 861/2750 cl-rem:3 lits-rem:3 T: 0.41 T-out: Y c [vivif] cache-based irred-- cl tried 2750 cl-sh 0 cl-rem 0 lit-rem 0 T-out N T: 0.03 c [vivif] cache-based red-- cl tried 10965 cl-sh 0 cl-rem 0 lit-rem 0 T-out N T: 0.28 c [vivif] asymm (tri+long) useful: 3/861/2750 lits-rem: 3 0-depth-assigns: 0 T: 0.41 s T-out: Y c SCC new: 0 T: 0.00 s c Cache cleaned. Updated: 0 K Cleaned: 0 K Freed: 0 K T: 0.01 c [clean] T: 0.0160 s c calculated reachability. T: 0.000 c clause size stats. size4: 145 size5: 121 larger: 2484 c [clean] T: 0.0160 s c 1083 252K 3658 2750 167 21K 19.4 10965 767 39K 77.3 c Doing burst search for 300 conflicts c 300-long burst search learnt units:0 learnt bins: 2 c percent of negative polarities set: 94.81 % (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 1084 252K 3658 2750 167 21K 19.4 11265 767 39K 78.5 c 1087 254K 3658 2750 167 21K 19.4 13207 775 39K 86.2 c 1091 256K 3658 2750 167 21K 19.4 15169 783 39K 92.5 c 1094 258K 3658 2750 167 21K 19.4 17102 792 39K 98.4 c 1095 260K 3658 2750 167 21K 19.4 19055 795 39K 102.6 c 1100 262K 3658 2750 167 21K 19.4 21K 800 39K 108.8 c 1100 264K 3658 2750 167 21K 19.4 22K 806 39K 109.6 c 1104 266K 3658 2750 167 21K 19.4 24K 808 39K 111.2 c irred prop: 1066K conf: 3K UIP used: 170K c red prop: 516K conf: 6K UIP used: 164K c sum lits visit: 0K cls visit: 0K prop: 1583K conf: 10K UIP used: 334K c [clean] T: 0.0150 s c [DBclean] Hard long cls limit would be: 893K c [DBclean] Locked: 500 skipped: 1741 c [DBclean] Pre-removed: 0 clean type will be propconfl c [DBclean] rem 13342 avgGlue 20.13 avgSize 116.78 c [DBclean] remain 13343 avgGlue 14.88 avgSize 106.74 T 0.05 c Using var act-multip 11 instead of standard 11 and act-divider 10 instead of standard 10 c 1106 268K 3658 2750 167 21K 19.4 13543 817 39K 107.5 c 1110 270K 3658 2750 167 21K 19.4 15495 824 39K 116.0 c rest conf freevar IrrL IrrT IrrB l/c RedL RedT RedB l/c c 1110 272K 3658 2750 167 21K 19.4 17447 834 39K 119.7 c 1114 274K 3658 2750 167 21K 19.4 19408 839 39K 123.2 c 1119 276K 3658 2750 167 21K 19.4 21K 841 39K 124.8 c 1126 278K 3658 2750 167 21K 19.4 23K 847 39K 129.9 c 1129 280K 3658 2750 167 21K 19.4 25K 852 39K 131.4 c 1133 282K 3658 2750 167 21K 19.4 27K 859 39K 131.6 c 1133 284K 3658 2750 167 21K 19.4 29K 862 39K 130.3 c irred prop: 1182K conf: 3K UIP used: 189K c red prop: 646K conf: 7K UIP used: 202K c sum lits visit: 0K cls visit: 0K prop: 1829K conf: 11K UIP used: 392K c [clean] T: 0.0150 s c [DBclean] Hard long cls limit would be: 962K c [DBclean] Locked: 500 skipped: 2019 c [DBclean] Pre-removed: 0 clean type will be propconfl c [DBclean] rem 15333 avgGlue 21.59 avgSize 155.39 c [DBclean] remain 15333 avgGlue 17.83 avgSize 109.76 T 0.06 c Using var act-multip 11 instead of standard 11 and act-divider 10 instead of standard 10 c 1137 286K 3658 2750 167 21K 19.4 15821 867 39K 112.9 c 1137 288K 3658 2750 167 21K 19.4 17774 872 39K 125.8 c 1142 290K 3658 2750 167 21K 19.4 19702 879 39K 128.5 c rest conf freevar IrrL IrrT IrrB l/c RedL RedT RedB l/c c 1144 292K 3658 2750 167 21K 19.4 21K 884 39K 132.1 c 1155 294K 3658 2750 167 21K 19.4 23K 888 39K 135.3 s SATISFIABLE v ... c Number of solutions found until now: 13 MM: solver->nVarsOutside()=1280 c clause size stats. size4: 155 size5: 121 larger: 2655 c [clean] T: 0.0160 s c 1155 296K 3693 2931 167 26K 20.5 25K 890 39K 135.8 c Doing burst search for 300 conflicts c 300-long burst search learnt units:0 learnt bins: 3 c percent of negative polarities set: 90.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 1156 296K 3693 2931 167 26K 20.5 25K 891 39K 136.4 s SATISFIABLE v ... c Number of solutions found until now: 14 MM: solver->nVarsOutside()=1280 Duplicate solution!!! (i=12, j=13)

When allowing only a few message:

c clause size stats. size4: 4 size5: 0 larger: 32 c clause size stats. size4: 4 size5: 0 larger: 33 c clause size stats. size4: 4 size5: 0 larger: 34 c clause size stats. size4: 4 size5: 0 larger: 35 c clause size stats. size4: 4 size5: 0 larger: 36 c clause size stats. size4: 4 size5: 0 larger: 37 c clause size stats. size4: 4 size5: 0 larger: 38 c clause size stats. size4: 4 size5: 0 larger: 39 c clause size stats. size4: 4 size5: 0 larger: 40 c clause size stats. size4: 4 size5: 0 larger: 41 c clause size stats. size4: 4 size5: 0 larger: 42 c clause size stats. size4: 4 size5: 0 larger: 43 c clause size stats. size4: 4 size5: 0 larger: 44 c [bva] added: 568 simp: 101368 T: 6.68 T-out: Y c clause size stats. size4: 160 size5: 146 larger: 2621 c [bva] added: 1859 simp: 24418 T: 0.89 T-out: N c clause size stats. size4: 145 size5: 121 larger: 2484 v ...solution which is later duplicate... c clause size stats. size4: 155 size5: 121 larger: 2655 v ...duplicate solution...

There the problem occurs after 2 times BVA is done, before all solutions were correct. But in above CNF problem occured also without BVA, so this hint seems to be wrong. I have checked all solver->nVarsOutside()=1280 when solutions were found and reverse clause is added, but they (the number of variables) seem to be correct all the time.

[msoos]

I'll fix this, but unfortunately this is not helping. I need time and I need to sit down. Sorry, let me get back to this when I have time.

[capiman]

Just a quick idea: I have tried two tests (renumber changed) 1) cryptominisat64 --bva=1 --renumber=1 --maxsol=1000 --input=f:\6x6\6x6.cnf --dumpres=6x6_new_1.res 2) cryptominisat64 --bva=1 --renumber=0 --maxsol=1000 --input=f:\6x6\6x6.cnf --dumpres=6x6_new_2.res

Test 1 aborted with wrong solution (as seen above), test 2 was ok, found all 260 unique solutions. When I compare the both logs, the first difference (beside times) is the following:

1) c [DBclean] Hard long cls limit would be: 523K 2) c [DBclean] Hard long cls limit would be: 528K

This changed number comes from:

In Solver::calc_how_many_to_remove() there is uint64_t maxToHave = (double)(longIrredCls.size() + binTri.irredTris + nVars() + 300ULL) * (double)solveStats.nbReduceDB * conf.maxNumRedsRatio;

Is nVars() there ok?

I see the same output again 2 times, again with changed numbers. Then i see a change in

1) c [impl sub] bin: 0 tri: 6 (stamp: 0, cache: 0) T: 0.02 T-out: N w-visit: 3598 2) c [impl sub] bin: 0 tri: 6 (stamp: 0, cache: 0) T: 0.02 T-out: N w-visit: 3696

(All this after 12 found solutions, during the calculation of 12 solutions no changes beside timestamps)

[msoos]

That limit has to be fixed. I'm putting it on the issues list.Thanks!

[capiman]

But could it be my problem of wrong (equal) result or is it only a side effect (cosmetical change)?

[capiman]

I found another difference between --renumber=0 and --renumber=1: *simplifier->limit_to_decrease seems to be decreasing different. Normal with/without renumber?

Difference seems to come from: SubsumeStrengthen::findStrengthened

There is following code (but whole function not yet checked..):

    if (newSize < bestSize) {
        minVar = cl[i].var();
        bestSize = newSize;
    }

Could there be something wrong? Perhaps not compatible with new Renumber & BVA var handling?

I don't know and stop for today...

[capiman]

I have just retested the above problem with and without BVA with sources from 17.01.2014:

D:\cryptominisat-17012014\cmsat>cryptominisat64 --bva=1 --maxsol=1000000 --input=solution_brendan_10x10_reduced_test.cnf --input=f:\10x10\10x10_new_dec2011.cnf --dumpres=10x10_0_to_24_with_bva.res

and

d:\cryptominisat-17012014\cmsat>cryptominisat64 --bva=0 --maxsol=1000000 --input=solution_brendan_10x10_reduced_test.cnf --input=f:\10x10\10x10_new_dec2011.cnf --dumpres=10x10_0_to_24_without_bva.res

as well as my well-known 6x6.cnf

It looks like the error was fixed in one of the commits since creation of this issue. The number of all found solutions were now correct. There were now no duplicates in the found solutions.

Therefore I think this issue can be closed!