Recurring Conflict Complexity

[shnarazk]

Objective

Restart if the present 'path' is a part of a too complex network. It's a derivation of #7.

Branches

• https://github.com/shnarazk/splr/tree/20200102-RCC
• https://github.com/shnarazk/splr/tree/20191231-FOC

I've learned so far

• It's not an alternative to the LBD threshold.
• Rather a kind of var reward.

Tried

• adaptive threshold on the frequency of being conflict
  • reset by a new level 0 assignment
• Ema based threshold on the recent average of the frequency of recurring conflict
• used as a restart condition on conflict paths.
• used as a coefficient for LBD threshold in order to be tolerant of 'bad' learnt on a 'hard' path.
  Since the development of path expansion isn't a Markov process, we can't estimate ... well, what?
• used as a reward for variables; reward should be given to variables that emit or have emitted conflicts. So RCC should be such a weighted criterion.

[shnarazk]

Multiply LBD with RCC

1: origin

T56.2.0.cnf                                3145220,10854665 |time:   422.32
 #conflict:     285954, #decision:      1139695, #propagate:      809410366 
  Assignment|#rem:   693206, #fix:    36609, #elm:  2415405, prg%:  77.9600 
 Clause Kind|Remv:    72866, LBD2:    29178, Binc:    14621, Perm:  4992586 
     Restart|#BLK:     1852, #RST:     1209, eASG:   0.5452, eLBD:   0.6881 
    Conflict|aLBD:     5.56, cnfl:    69.26, bjmp:    66.33, rpc%:   0.4228 
   Clause DB|#rdc:       13, #sce:      197 |blkR:   1.4000, frcK:   0.8032 

10-3-13.cnf                                    29772,922204 |time:  1001.97
 #conflict:    2890000, #decision:      6260488, #propagate:     1331423143 
  Assignment|#rem:    25425, #fix:     2948, #elm:     1399, prg%:  14.6010 
 Clause Kind|Remv:   224907, LBD2:     7193, Binc:     1750, Perm:   895383 
     Restart|#BLK:     3079, #RST:    22938, eASG:   1.0406, eLBD:   1.5704 
    Conflict|aLBD:    52.17, cnfl:    75.80, bjmp:    74.72, rpc%:   0.7937 
   Clause DB|#rdc:       49, #sce:      306 |blkR:   1.4000, frcK:   0.9496 

2 generous guard: threshold * RCC.trend() < LBD.trend()

T56.2.0.cnf                                3145220,10854665 |time:   459.30
 #conflict:     305284, #decision:      1294943, #propagate:      823134138 
  Assignment|#rem:   748302, #fix:     7267, #elm:  2389651, prg%:  76.2083 
 Clause Kind|Remv:   103271, LBD2:    28351, Binc:    14078, Perm:  5467068 
     Restart|#BLK:     2157, #RST:     1343, eASG:   0.1312, eLBD:   1.0176 
    Conflict|aLBD:     9.41, cnfl:    65.28, bjmp:    62.96, rpc%:   0.4399 
   Clause DB|#rdc:       12, #sce:      200 |blkR:   1.4000, frcK:   0.8814 

10-3-13.cnf                                    29772,922204 |time:  1002.56
 #conflict:    4250000, #decision:      9760765, #propagate:     1666401649 
  Assignment|#rem:    25201, #fix:     3172, #elm:     1399, prg%:  15.3534 
 Clause Kind|Remv:   329709, LBD2:    11859, Binc:     2623, Perm:   890640 
     Restart|#BLK:     7804, #RST:    15113, eASG:   0.8011, eLBD:   1.7488 
    Conflict|aLBD:    50.88, cnfl:   514.50, bjmp:   512.44, rpc%:   0.3556 
   Clause DB|#rdc:       56, #sce:      452 |blkR:   1.4000, frcK:   0.9797 
    Strategy|mode: ERROR

3 evacuater: threshold < LBD.trend() * RCC.trend()

T56.2.0.cnf                                3145220,10854665 |time:   535.49
 #conflict:     301611, #decision:      1292338, #propagate:      998491152 
  Assignment|#rem:   717175, #fix:    38633, #elm:  2389412, prg%:  77.1979 
 Clause Kind|Remv:    63449, LBD2:    29231, Binc:    15331, Perm:  5212232 
     Restart|#BLK:     2045, #RST:     1502, eASG:   0.5945, eLBD:   0.6225 
    Conflict|aLBD:     4.56, cnfl:    80.86, bjmp:    78.28, rpc%:   0.4980 
   Clause DB|#rdc:       12, #sce:      160 |blkR:   1.4000, frcK:   0.7837 ```

[shnarazk]

RCC as var reward