1.4.2: Catch up MiniSat 2 mostly (41)

[shnarazk]

Objective: True Implementation of the MiniSat 2.2

• restart policy: start = 100, scaling = 1.5
• learnts reduction: start at (nc / 3), scaling = 1.5
• about clause reduction policy, use the result on #42 and #45. LBD finnaly
• switch to the ultimate evaluation criterion
• add some utilities

That's it.

[shnarazk]

another results

$ sat-benchmark -3 250 -s mios-1.4.0 mios-1.4.1 mios-1.4.2
solver, num, target, time
# sat-benchmark 0.13.2, j=1, t=1260, p='' on xingu @ 2017-10-17T15:37:39+09:00
# 2017-08-28T18:25 mios-1.4.0; mios 1.4.0 on regression15 branch
"mios-1.4.0", 1, 175,    5.72
"mios-1.4.0", 2, 200,    13.71
"mios-1.4.0", 3, 225,    45.42
"mios-1.4.0", 4, 250,    94.21
"mios-1.4.0", 5, "itox",     17.85
"mios-1.4.0", 6, "m283",     147.07
"mios-1.4.0", 7, "38b",  19.76
"mios-1.4.0", 8, "48b",  666.31
# 2017-08-31T16:03 mios-1.4.1; mios 1.4.1
"mios-1.4.1", 1, 175,    5.25
"mios-1.4.1", 2, 200,    12.58
"mios-1.4.1", 3, 225,    41.68
"mios-1.4.1", 4, 250,    87.55
"mios-1.4.1", 5, "itox",     17.31
"mios-1.4.1", 6, "m283",     134.83
"mios-1.4.1", 7, "38b",  20.30
"mios-1.4.1", 8, "48b",  629.51
# 2017-10-17T10:06 mios-1.4.2; mios-1.4.2 https://github.com/shnarazk/mios/
"mios-1.4.2", 1, 175,    3.82
"mios-1.4.2", 2, 200,    11.90
"mios-1.4.2", 3, 225,    33.14
"mios-1.4.2", 4, 250,    80.84
"mios-1.4.2", 5, "itox",     13.55
"mios-1.4.2", 6, "m283",     42.46
"mios-1.4.2", 7, "38b",  46.71
"mios-1.4.2", 8, "48b",  58.14

[shnarazk]

[shnarazk]

[shnarazk]