Compare with 8232f99

[shnarazk]

fix the regression in #42

• [ ] Day 1: re-evaluate 8232f99
• [ ] Day 2: the same reduction sequence
• [x] Day 3: the same restart sequence
• [x] Bug hunt
• [x] Fix the regression

[shnarazk]

baseline

# 2017-09-21T14:09 /mios-lbd-8232f99 ; mios lbd:PR#36
"mios-lbd-8232f99", 1, 200,      17.64
"mios-lbd-8232f99", 2, 225,      42.62
"mios-lbd-8232f99", 3, 250,      129.45
"mios-lbd-8232f99", 4, "een",    4.34
"mios-lbd-8232f99", 5, "bmc",    2.81
"mios-lbd-8232f99", 6, "38b",    16.55
# 2017-09-21T14:23 #44comapare-with-8232f99 4493b8a
"mios-sla-44", 1, 200,   21.23
"mios-sla-44", 2, 225,   78.39
"mios-sla-44", 3, 250,   204.94
"mios-sla-44", 4, "een",         5.25
"mios-sla-44", 5, "bmc",         3.84
"mios-sla-44", 6, "38b",         17.07

[shnarazk]

001f965

# p='', t=1260 on xingu @ 2017-09-21T14:44:59+09:00
"mios-sla-44", 1, 200,   12.85
"mios-sla-44", 2, 225,   35.71
"mios-sla-44", 3, 250,   124.88
"mios-sla-44", 4, "een",         5.18
"mios-sla-44", 5, "bmc",         3.75
"mios-sla-44", 6, "38b",         65.00

Gedankenexperimentre

I mean they have no corresponding commits.

restartScale = 1.5 (instead of 1.4)

# p='', t=1260 on xingu @ 2017-09-21T14:52:41+09:00
"mios-sla-44", 1, 200,   13.65
"mios-sla-44", 2, 225,   37.50
"mios-sla-44", 3, 250,   113.43
"mios-sla-44", 4, "een",         4.63
"mios-sla-44", 5, "bmc",         3.26
"mios-sla-44", 6, "38b",         81.43

DB expansion rate is fixed to 500

# p='', t=1260 on xingu @ 2017-09-21T14:58:43+09:00
"mios-sla-44", 1, 200,   15.47
"mios-sla-44", 2, 225,   40.09
"mios-sla-44", 3, 250,   106.18
"mios-sla-44", 4, "een",         4.61
"mios-sla-44", 5, "bmc",         3.74
"mios-sla-44", 6, "38b",         61.63

[shnarazk]

# p='', t=1260 on xingu @ 2017-09-21T15:32:12+09:00
"mios-sla-44", 1, 200,   14.14
"mios-sla-44", 2, 225,   38.92
"mios-sla-44", 3, 250,   113.53
"mios-sla-44", 4, "een",         4.68
"mios-sla-44", 5, "bmc",         3.67
"mios-sla-44", 6, "38b",         29.70

seems a promising way :+1:

[shnarazk]

The regression was fixed. Luby works!

[shnarazk]

d8166e3

5aa343e

[shnarazk]

[shnarazk]

Cllosing note

1. The graph is against the 'Luby and/or quick restart is better' claim. One solid reason of this deviation is clauses weren't sorted by LBD :-1 were by size (SSA-ordering). So I need exam again in the upper branch.

2. Problem selection affects much! It's the time to switch a less biased benchmark suit. The following is the result of experimentation on small problems in SAT-Competition 2017 Main track.