Fix bugs in simplifyDB and analyze in 1.5.0

[shnarazk]

objective

• fix (or optimeze) about UPDATEVARACTIVITY trick used in Glucose 3.0
• simplifyDB failed to remove satisfied clauses from learnts
• a speculation on the meaning of LBD

related

• glucose-3.0: https://github.com/shnarazk/glucose/pull/2
• glucose-3.0: https://github.com/shnarazk/glucose/pull/3
• glucose-3.0: https://github.com/shnarazk/glucose/pull/4

---

Gilles Audemard, Laurent Simon, GLUCOSE : a solver that predicts learnt clauses quality, In SAT 2009 competitive events booklet: preliminary version, 2009.

The state-of-the-art VSIDS [Moskewicz et al., 2001] heuristic bumps all variables which participated to the resolution steps conducting to the assertive clause. This heuristic favors variables that are often and recently used in conflict analysis. Since we want to help the solver to generate clauses with
small LBD values, we propose to reward a second time variables that help to obtain such clauses.

We bump once again all variables from the last decision level, which were used in conflict analysis, but which were propagated by a clause of small LBD (smaller than the new learnt clause).

the criterion based on 1.5.0

# sat-benchmark 0.13.2, j=1, t=1260, p='' on smithi @ 2017-11-01T01:32:12+09:00
"mios-1.5.0", 1, 175,    3.61
"mios-1.5.0", 2, 200,    9.72
"mios-1.5.0", 3, 225,    26.56
"mios-1.5.0", 4, 250,    64.66
"mios-1.5.0", 5, "itox",         10.86
"mios-1.5.0", 6, "m283",         24.14
"mios-1.5.0", 7, "38b",  30.03
"mios-1.5.0", 8, "48b",  38.83

[shnarazk]

experimentation on variants

# sat-benchmark 0.13.2, j=1, t=1260, p='' on smithi @ 2017-11-01T00:46:11+09:00, r < r'
"mios-52", 1, 175,       3.55
"mios-52", 2, 200,       9.68
"mios-52", 3, 225,       26.41
"mios-52", 4, 250,       64.37
"mios-52", 5, "itox",    12.13
"mios-52", 6, "m283",    23.62
"mios-52", 7, "38b",     29.42
"mios-52", 8, "48b",     37.56

# sat-benchmark 0.13.2, j=1, t=1260, p='' on smithi @ 2017-11-01T00:50:12+09:00, r* < r
"mios-52", 1, 175,       4.28
"mios-52", 2, 200,       11.28
"mios-52", 3, 225,       23.23
"mios-52", 4, 250,       76.76
"mios-52", 5, "itox",    15.49
"mios-52", 6, "m283",    55.90
"mios-52", 7, "38b",     46.49
"mios-52", 8, "48b",     44.93

# sat-benchmark 0.13.2, j=1, t=1260, p='' on smithi @ 2017-11-01T01:02:54+09:00, no check
"mios-52", 1, 175,       4.25
"mios-52", 2, 200,       9.14
"mios-52", 3, 225,       24.57
"mios-52", 4, 250,       71.57
"mios-52", 5, "itox",    24.03
"mios-52", 6, "m283",    41.55
"mios-52", 7, "38b",     47.27
"mios-52", 8, "48b",     613.07

# sat-benchmark 0.13.2, j=1, t=1260, p='' on smithi @ 2017-11-01T01:19:15+09:00, rank r* < rank r
"mios-52", 1, 175,       4.34
"mios-52", 2, 200,       10.24
"mios-52", 3, 225,       26.07
"mios-52", 4, 250,       69.96
"mios-52", 5, "itox",    17.67
"mios-52", 6, "m283",    64.29
"mios-52", 7, "38b",     47.28
"mios-52", 8, "48b",     48.59

# sat-benchmark 0.13.2, j=1, t=1260, p='' on smithi @ 2017-11-01T01:25:26+09:00, rank r < rank r*
"mios-52", 1, 175,       4.14
"mios-52", 2, 200,       9.75
"mios-52", 3, 225,       22.14
"mios-52", 4, 250,       67.89
"mios-52", 5, "itox",    24.06
"mios-52", 6, "m283",    71.16
"mios-52", 7, "38b",     29.34
"mios-52", 8, "48b",     56.21

[shnarazk]

[shnarazk]

an effect of definition of LBD

## LBD after cancel (the level of the 1st literal is the level that back jump to)
"mios-52", 3, 225,       33.06
"mios-52", 4, 250,       108.68
"mios-52", 5, "itox",    24.01
"mios-52", 6, "m283",    107.46
"mios-52", 7, "38b",     14.63
"mios-52", 8, "44b",     81.26
# original definition: the level of the 1st literal is the conflicting level
"mios-52", 3, 225,       36.54
"mios-52", 4, 250,       97.22
"mios-52", 5, "itox",    28.45
"mios-52", 6, "m283",    75.81
"mios-52", 7, "38b",     54.10
"mios-52", 8, "44b",     259.33     -- What a big difference that needs an explanation!

Note: the value of LBD can become one even in Glucose.

[shnarazk]

[shnarazk]