45 lines
1.6 KiB
Text
45 lines
1.6 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...
|
|
62 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 2549 rows, 2106 columns, and 9349 non-zeros
|
|
575 covering inequalities
|
|
1924 partitioning equalities
|
|
Solving CNF-SAT problem...
|
|
Instance has 3356 variables, 10874 clauses, and 34549 literals
|
|
==================================[MINISAT]===================================
|
|
| Conflicts | ORIGINAL | LEARNT | Progress |
|
|
| | Clauses Literals | Limit Clauses Literals Lit/Cl | |
|
|
==============================================================================
|
|
| 0 | 9000 32675 | 3000 0 0 0.0 | 0.000 % |
|
|
| 101 | 6025 21551 | 3300 93 1620 17.4 | 57.688 % |
|
|
| 251 | 6025 21551 | 3630 243 4961 20.4 | 57.688 % |
|
|
==============================================================================
|
|
SATISFIABLE
|
|
Objective value = 0.000000000e+000
|
|
Time used: 0.0 secs
|
|
Memory used: 6.5 Mb (6775701 bytes)
|
|
1 12 7 18 3
|
|
6 19 2 13 8
|
|
11 22 15 4 17
|
|
20 5 24 9 14
|
|
23 10 21 16 25
|
|
Model has been successfully processed
|