jwaldmann
commented
1 year ago When I set verbosity to 2 in Ersatz.Solver.Minisat.API, for the 8x8-knight's tour (cabal test) I get this trace
Test suite knight: RUNNING...
CNF 24321 vars 111104 clauses
| Garbage collection: 2060300 bytes => 613860 bytes |
| Garbage collection: 808276 bytes => 404108 bytes |
| Eliminated clauses: 0.18 Mb |
============================[ Search Statistics ]==============================
| Conflicts | ORIGINAL | LEARNT | Progress |
| | Vars Clauses Literals | Limit Clauses Lit/Cl | |
===============================================================================
| 100 | 2771 20003 56690 | 7334 99 49 | 61.042 % |
| 250 | 2769 20003 56690 | 8067 247 58 | 61.050 % |
| 475 | 2765 20003 56690 | 8874 468 62 | 61.067 % |
| 812 | 2763 20003 56690 | 9762 803 62 | 61.075 % |
| 1318 | 2762 20003 56690 | 10738 1308 78 | 61.079 % |
| 2077 | 2758 20003 56690 | 11812 2063 89 | 61.095 % |
| 3216 | 2757 20003 56690 | 12993 3201 101 | 61.099 % |
| 4924 | 2743 20003 56690 | 14292 4895 94 | 61.157 % |
| 7486 | 2731 20003 56690 | 15722 7444 110 | 61.206 % |
| 11330 | 2713 20003 56690 | 17294 11266 108 | 61.280 % |
| 17096 | 2699 20003 56690 | 19023 17017 116 | 61.338 % |
===============================================================================
0 25 38 47 62 3 30 33
39 46 63 2 29 32 61 4
26 1 24 37 48 59 34 31
45 40 49 28 23 36 5 60
50 27 52 41 6 11 58 35
53 44 15 22 13 20 7 10
16 51 42 55 18 9 12 57
43 54 17 14 21 56 19 8
real 0m8.156s
When I write the CNF to file, and solve with minisat from the command line, I get
============================[ Problem Statistics ]==================real 0m8.156s
===========
| |
| Number of variables: 24321 |
| Number of clauses: 111104 |
| Parse time: 0.03 s |
| Garbage collection: 2060300 bytes => 613860 bytes |
| Garbage collection: 808276 bytes => 404108 bytes |
| Garbage collection: 447788 bytes => 306772 bytes |
| Eliminated clauses: 0.18 Mb |
| Simplification time: 0.05 s |
| |
============================[ Search Statistics ]==============================
| Conflicts | ORIGINAL | LEARNT | Progress |
| | Vars Clauses Literals | Limit Clauses Lit/Cl | |
===============================================================================
| 100 | 2790 20003 56690 | 7334 99 52 | 60.964 % |
| 250 | 2790 20003 56690 | 8067 249 59 | 60.964 % |
| 475 | 2787 20003 56690 | 8874 471 66 | 60.976 % |
| 812 | 2787 20003 56690 | 9762 808 88 | 60.976 % |
| 1318 | 2787 20003 56690 | 10738 1314 96 | 60.976 % |
| 2077 | 2779 19891 56434 | 11812 2064 90 | 61.009 % |
| 3216 | 2778 19891 56434 | 12993 3202 113 | 61.013 % |
| 4924 | 2742 19840 56320 | 14292 4893 100 | 61.161 % |
| 7486 | 2734 19413 55299 | 15722 7444 106 | 61.194 % |
| 11330 | 2712 19213 54832 | 17294 11257 100 | 61.284 % |
| 17096 | 2689 18919 54130 | 19023 16988 106 | 61.379 % |
===============================================================================
restarts : 78
conflicts : 22217 (26181 /sec)
decisions : 138774 (0.00 % random) (163532 /sec)
propagations : 3688453 (4346495 /sec)
conflict literals : 2527356 (10.45 % deleted)
Memory used : 33.00 MB
CPU time : 0.848604 s
SATISFIABLEOne difference is that the number of clauses and literals is constant with the API call but reduces with the process call.
I was comparing runtimes for solving one and the same CNF (built via http://hackage.haskell.org/package/ersatz) when calling minisat via:
and to my surprise, solver-via-API is definitely slower, namely, it behaves exactly as command-line solver with
-no-pre.Is this intended? How can I get the API to behave as the default command-line solver (with
-pre)?This seems to be relevant: https://github.com/niklasso/minisat-haskell-bindings/blob/master/MiniSat.hsc#L31 , what does it mean?
I can comment out the line
eliminate s Trueand it is indeed running faster.