Biclause optimization

[shnarazk]

changelog

• simplifyDB is called only after restart. Since this means decision level is zero, locked is removed from it. Note: In some problems, the number of propagations increases by calling simplifyDB. Is it possible!? 😲

objective

• Binary clause, or biclause, has a specific representation.
• biclause should be handled as a kind of problem clause.
• learning a binary clause should be a trigger to simplify or subsumpiton.

related branch

• investigate the probability of biclause
• comparison to the previous code: #51

This is a week project. 👨‍⚕️ cf #19, #28

[shnarazk]

# sat-benchmark 0.13.3, j=1, t=1260, p='' on xingu @ 2017-10-24T18:02:46+09:00
# 2017-10-24T18:02 mios-48; mios-1.5.0WIP #48
"mios-48", 1, 175,       4.83
"mios-48", 2, 200,       13.75
"mios-48", 3, 225,       40.79
"mios-48", 4, 250,       94.78
"mios-48", 5, "itox",    21.08
"mios-48", 6, "m283",    35.14
"mios-48", 7, "38b",     18.61
"mios-48", 8, "48b",     221.15
# 2017-10-21T10:46 mios-1.5.0; mios-1.5.0 https://github.com/shnarazk/mios/
"mios-1.5.0", 1, 175,    3.85
"mios-1.5.0", 2, 200,    11.78
"mios-1.5.0", 3, 225,    33.13
"mios-1.5.0", 4, 250,    80.74
"mios-1.5.0", 5, "itox",         13.51
"mios-1.5.0", 6, "m283",         43.28
"mios-1.5.0", 7, "38b",  46.35
"mios-1.5.0", 8, "48b",  60.05

[shnarazk]

# 2017-10-24T19:27 mios-48; mios-1.5.0WIP #48
# sat-benchmark 0.13.3, j=1, t=1260, p='' on xingu @ 2017-10-24T19:35:30+09:00
"mios-48", 1, 175,       4.60
"mios-48", 2, 200,       13.61
"mios-48", 3, 225,       36.46
"mios-48", 4, 250,       82.98
"mios-48", 5, "itox",    20.88
"mios-48", 6, "m283",    38.76
"mios-48", 7, "38b",     19.17
"mios-48", 8, "48b",     223.81

[shnarazk]

# 2017-10-25T09:32 mios-48; mios-1.5.0WIP #48, inplaceSubsume on learnts
# sat-benchmark 0.13.3, j=1, t=1260, p='' on xingu @ 2017-10-25T09:33:15+09:00
"mios-48", 1, 175,       3.77
"mios-48", 2, 200,       11.54
"mios-48", 3, 225,       33.38
"mios-48", 4, 250,       79.62
"mios-48", 5, "itox",    22.30
"mios-48", 6, "m283",    82.48
"mios-48", 7, "38b",     23.86
"mios-48", 8, "48b",     644.31   
# sat-benchmark 0.13.3, j=1, t=1260, p='' on xingu @ 2017-10-25T09:49:14+09:00, inplaceSubsume on clauses
"mios-48", 1, 175,       3.83
"mios-48", 2, 200,       11.63
"mios-48", 3, 225,       33.52
"mios-48", 4, 250,       80.00
"mios-48", 5, "itox",    24.90
"mios-48", 6, "m283",    76.95
"mios-48", 7, "38b",     23.94
"mios-48", 8, "48b",     636.22
# sat-benchmark 0.13.3, j=1, t=1260, p='' on xingu @ 2017-10-25T10:05:58+09:00, subsumeAll on both
"mios-48", 1, 175,       4.25
"mios-48", 2, 200,       11.99
"mios-48", 3, 225,       33.72
"mios-48", 4, 250,       81.66
"mios-48", 5, "itox",    117.57
"mios-48", 6, "m283",    99.59
"mios-48", 7, "38b",     32.53
"mios-48", 8, "48b",     392.78

[shnarazk]

A very interesting behavior: difference between 3-SATs and industrials on 9800e1d

solver, num, target, time
# 2017-10-25T21:15 mios-48; mios-1.5.0WIP #48, pushTo learnts 
# sat-benchmark 0.13.3, j=1, t=1260, p='' on xingu @ 2017-10-25T21:16:34+09:00
"mios-48", 2, 200,       11.79
"mios-48", 3, 225,       33.63
"mios-48", 4, 250,       81.71
"mios-48", 5, "itox",    22.16
"mios-48", 6, "m283",    38.49
"mios-48", 7, "38b",     15.71
"mios-48", 8, "48b",     80.84

# 2017-10-25T21:22 mios-48; mios-1.5.0WIP #48, pushTo clauses
# sat-benchmark 0.13.3, j=1, t=1260, p='' on xingu @ 2017-10-25T21:22:22+09:00
"mios-48", 2, 200,       11.53    -- good
"mios-48", 3, 225,       33.31.   -- good
"mios-48", 4, 250,       79.66    -- good
"mios-48", 5, "itox",    21.46
"mios-48", 6, "m283",    73.83    -- doubled
"mios-48", 7, "38b",     23.38
"mios-48", 8, "48b",     619.84  !!!

[shnarazk]

[shnarazk]

# 2017-11-12T07:54 mios-52; mios-1.5.0WIP #52
"mios-52", 1, 175,       3.83
"mios-52", 2, 200,       11.87
"mios-52", 3, 225,       33.57
"mios-52", 4, 250,       82.40
"mios-52", 5, "itox",    12.83
"mios-52", 6, "m283",    39.92
"mios-52", 7, "38b",     47.47
"mios-52", 8, "44b",     58.80
# 2017-11-12T12:40 mios-48; mios-1.5.0WIP #52 #48
"mios-48", 1, 175,       3.94
"mios-48", 2, 200,       12.01
"mios-48", 3, 225,       34.56
"mios-48", 4, 250,       83.22
"mios-48", 5, "itox",    70.79
"mios-48", 6, "m283",    37.50
"mios-48", 7, "38b",     57.45
"mios-48", 8, "44b",     450.05

[shnarazk]

# sat-benchmark 0.13.3, j=1, t=1260, p='' on xingu @ 2017-11-12T15:09:38+09:00
"mios-48", 1, 175,       3.98
"mios-48", 2, 200,       12.08
"mios-48", 3, 225,       34.28
"mios-48", 4, 250,       84.04
"mios-48", 5, "itox",    62.81
"mios-48", 6, "m283",    37.28
"mios-48", 7, "38b",     74.19
"mios-48", 8, "44b",     121.93

[shnarazk]

moved to #55