Variance of polarity

[shnarazk]

Objective

Import and try the idea prioritizing decision vars based on their variance of polarity EMA in the context of CDCL SAT solvers;

• Prioritized Unit Propagation with Periodic Resetting is (Almost) All You Need for Random SAT Solving, avXiv

• PR: a new branch about variance of var polarity #8

So far

• The EMA length should be short.
• Shouldn't substitute 'phase' with 'polarity'.
• It's another deep swamp eating time endlessly. Managing and reflecting the best assignment set needs some idea.
• Should reconsider Luby restart again in the context of my deep search usability.
• Combining heuristics is another way to enable multi-dimension investigation like restarts. So it should be good.
• There is a very similar idea: confliction heat map, or frequency of conflicts, requires update operations only on conflicting vars. ➡️ Recurring Conflict Complexity #11
• Suspended.
• Another idea: frequency of conflict and its EMA.

tried

• mixed and conditional combination of activity and VoP.
• use VoP as the increment of CHB. Fixing an important or difficult conflict eagerly seems rational.
• 20191231-vop-restart: Instead of var ordering, how about as a restart trigger? Escaping from "a too difficult conflicting situation" might be good.
• New series from 2020-01-22: update only when getting the most assigns ever.

[shnarazk]

base: dev-0.2.2

# sat-bench 0.6.1, timeout:510 on demorgan @ 2019-12-24T17:57:22
# ~/.cargo/bin/splr (splr 0.2.2-dev.0) @ 2019-12-24T17:57:10
solver,       num,                 target,    time
"splr",         1,           "UF250(100)", 125.528
"splr",         2,          "UUF250(100)", 391.485
"splr",         3, "3/SAT/v360-c1530/002",  93.333
"splr",         4, "3/SAT/v360-c1530/030", 279.968
"splr",         5, "3/SAT/v360-c1530/033",  11.974
"splr",         6, "3/SAT/v360-c1530/035",  14.960
"splr",         7, "3/SAT/v360-c1530/039",   ABORT
"splr",         8, "3/SAT/v360-c1530/051",   ABORT
"splr",         9, "3/SAT/v360-c1530/060",   ABORT
"splr",        10, "3/SAT/v360-c1530/073", 108.163
"splr",        11, "3/SAT/v360-c1530/087", 100.646
"splr",        12, "3/SAT/v360-c1530/093", 138.353
"splr",        13, "3/UNS/v360-c1530/001",   ABORT
"splr",        14, "3/UNS/v360-c1530/015", 325.093
"splr",        15, "3/UNS/v360-c1530/028", 489.470
"splr",        16, "3/UNS/v360-c1530/029",   ABORT
"splr",        17, "3/UNS/v360-c1530/031",   ABORT
"splr",        18, "3/UNS/v360-c1530/053", 379.220
"splr",        19, "3/UNS/v360-c1530/061",   ABORT
"splr",        20, "3/UNS/v360-c1530/086", 296.291
"splr",        21, "3/UNS/v360-c1530/089", 367.831
"splr",        22, "3/UNS/v360-c1530/096", 203.396
"splr",        23,          "SR2015/itox",   1.691
"splr",        24,          "SR2015/m283",  59.258
"splr",        25,           "SR2015/38b",  34.372
"splr",        26,           "SR2015/44b", 117.917

commit 73a5699

"splr",         1,           "UF250(100)", 132.203
"splr",         2,          "UUF250(100)", 368.384
"splr",         3, "3/SAT/v360-c1530/002", 314.685
"splr",         4, "3/SAT/v360-c1530/030", 344.352
"splr",         5, "3/SAT/v360-c1530/033",  40.731
"splr",         6, "3/SAT/v360-c1530/035",  73.324
"splr",         7, "3/SAT/v360-c1530/039",   ABORT
"splr",         8, "3/SAT/v360-c1530/051", 465.758
"splr",         9, "3/SAT/v360-c1530/060",   ABORT
"splr",        10, "3/SAT/v360-c1530/073",  23.994
"splr",        11, "3/SAT/v360-c1530/087",  16.906
"splr",        12, "3/SAT/v360-c1530/093",  17.496
"splr",        13, "3/UNS/v360-c1530/001", 492.342
"splr",        14, "3/UNS/v360-c1530/015", 325.968
"splr",        15, "3/UNS/v360-c1530/028", 476.926
"splr",        16, "3/UNS/v360-c1530/029",   ABORT
"splr",        17, "3/UNS/v360-c1530/031", 492.500
"splr",        18, "3/UNS/v360-c1530/053", 355.292
"splr",        19, "3/UNS/v360-c1530/061",   ABORT
"splr",        20, "3/UNS/v360-c1530/086", 240.469
"splr",        21, "3/UNS/v360-c1530/089", 352.583
"splr",        22, "3/UNS/v360-c1530/096", 253.425
"splr",        23,          "SR2015/itox",   1.663
"splr",        24,          "SR2015/m283",  54.409
"splr",        25,           "SR2015/38b",  19.469
"splr",        26,           "SR2015/44b", 152.407