64 lines
3 KiB
Text
64 lines
3 KiB
Text
GLPSOL: GLPK LP/MIP Solver, v4.47
|
|
Parameter(s) specified in the command line:
|
|
--minisat --math Knights.mathprog
|
|
Reading model section from Knights.mathprog...
|
|
Reading data section from Knights.mathprog...
|
|
65 lines were read
|
|
Generating void0...
|
|
Generating void1...
|
|
Generating void2...
|
|
Generating void3...
|
|
Generating void4...
|
|
Generating void5...
|
|
Generating void6...
|
|
Generating void7...
|
|
Generating Izfree...
|
|
Generating Iz1...
|
|
Generating rule1...
|
|
Generating rule2...
|
|
Generating rule3...
|
|
Model has been successfully generated
|
|
Will search for ANY feasible solution
|
|
Translating to CNF-SAT...
|
|
Original problem has 10466 rows, 9360 columns, and 55330 non-zeros
|
|
3968 covering inequalities
|
|
6370 partitioning equalities
|
|
Solving CNF-SAT problem...
|
|
Instance has 15056 variables, 46754 clauses, and 149794 literals
|
|
==================================[MINISAT]===================================
|
|
| Conflicts | ORIGINAL | LEARNT | Progress |
|
|
| | Clauses Literals | Limit Clauses Literals Lit/Cl | |
|
|
==============================================================================
|
|
| 0 | 40512 143552 | 13504 0 0 0.0 | 0.000 % |
|
|
| 100 | 32458 114610 | 14854 89 5138 57.7 | 46.633 % |
|
|
| 250 | 32458 114610 | 16340 239 18544 77.6 | 46.633 % |
|
|
| 475 | 27499 102956 | 17974 424 42212 99.6 | 46.892 % |
|
|
| 813 | 27366 102490 | 19771 757 73184 96.7 | 51.541 % |
|
|
| 1322 | 27366 102490 | 21748 1264 137991 109.2 | 52.245 % |
|
|
| 2083 | 23226 92730 | 23923 2010 250286 124.5 | 53.620 % |
|
|
| 3227 | 22239 90284 | 26315 3138 460582 146.8 | 53.620 % |
|
|
| 4937 | 22239 90284 | 28947 4848 769486 158.7 | 53.620 % |
|
|
| 7499 | 22206 90168 | 31842 7404 1258240 169.9 | 55.167 % |
|
|
| 11346 | 21067 87284 | 35026 11248 2085553 185.4 | 55.167 % |
|
|
| 17113 | 21067 87284 | 38528 17015 3625910 213.1 | 55.167 % |
|
|
| 25763 | 21067 87284 | 42381 25665 5906283 230.1 | 55.167 % |
|
|
| 38738 | 21051 87252 | 46619 38638 9316878 241.1 | 55.679 % |
|
|
| 58199 | 21051 87252 | 51281 16434 3967196 241.4 | 55.685 % |
|
|
| 87393 | 20707 86474 | 56410 45624 13013357 285.2 | 56.277 % |
|
|
| 131184 | 20180 84834 | 62051 37252 8996727 241.5 | 56.542 % |
|
|
| 196871 | 20180 84834 | 68256 49392 13807861 279.6 | 56.542 % |
|
|
| 295399 | 20180 84834 | 75081 22688 5827696 256.9 | 56.542 % |
|
|
==============================================================================
|
|
SATISFIABLE
|
|
Objective value = 0.000000000e+000
|
|
Time used: 333.0 secs
|
|
Memory used: 28.2 Mb (29609617 bytes)
|
|
51 24 31 6 49 26 33 64
|
|
30 5 50 25 32 63 48 43
|
|
23 52 7 4 27 44 15 34
|
|
8 29 60 45 62 47 42 17
|
|
59 22 53 28 3 16 35 14
|
|
54 9 56 61 46 39 18 41
|
|
21 58 11 38 19 2 13 36
|
|
10 55 20 57 12 37 40 1
|
|
Model has been successfully processed
|