feature 'reward_annealing' #187

shnarazk · 2022-10-02T14:35:07Z

reward annealing, activity annealing

shnarazk · 2022-10-06T01:23:24Z

# 0.14.1, timeout:2000 on demorgan @ 2022-10-06T09:07:01
# ~/.cargo/bin/splr (0.17.0-alpha) @ 2022-10-06T09:07:01
solver,       num,                       target,     time
"splr",         1,                 "UF250(100)",   74.552
"splr",         2,                "UUF250(100)",  220.842
"splr",         3,   "3SAT/360  S722433227-030",  256.248
"splr",         4,   "3SAT/360 S2032263657-035",    0.893
"splr",         5,   "3SAT/360  S368632549-051",   19.017
"splr",         6,   "3SAT/360 S1684547485-073",    3.284
"splr",         7,   "3SAT/360 S1711406314-093",   13.497
"splr",         8,   "3UNS/360 S1369720750-015",  168.562
"splr",         9,   "3UNS/360  S367138237-029",  360.240
"splr",        10,   "3UNS/360  S680239195-053",  166.212
"splr",        11,   "3UNS/360  S253750560-086",  132.746
"splr",        12,   "3UNS/360 S1028159446-096",  193.549
"splr",        13,   "[SAT] SR2015/m283,  3553",   17.481
"splr",        14,   "[SAT] SR2015/38b,    448",   48.943
"splr",        15,   "[SAT] SR2015/44b,    609",  240.093
"splr",        16,   "[SAT] SC21/b04_s_unknown",  171.057
"splr",        17,   "[SAT] SC21/quad_r21_m22 ",   22.084
"splr",        18,   "[SAT] SC21/toughsat_895s",  339.265
"splr",        19,   "[UNS] SC21/assoc_mult_e3",  154.019
"splr",        20,   "[UNS] SC21/dist4.c      ",  195.261
"splr",        21,   "[UNS] SC21/p01_lb_05    ",  255.376
"splr",        22,   "[UNS] SC21/shift1add    ",   25.396
med:   160.115, max:   360.240,           total: 3078.617
# ~/Repositories/splr@10-06T09:25:17 8d5e8a5d@20221002-vdr*

shnarazk · 2022-10-06T18:27:34Z

# 0.14.1, timeout:2000 on demorgan @ 2022-10-07T02:11:43
# ~/.cargo/bin/splr (0.17.0-alpha) @ 2022-10-07T02:11:43
solver,       num,                       target,     time
"splr",         1,                 "UF250(100)",   73.925
"splr",         2,                "UUF250(100)",  217.685
"splr",         3,   "3SAT/360  S722433227-030",  225.273
"splr",         4,   "3SAT/360 S2032263657-035",    0.821
"splr",         5,   "3SAT/360  S368632549-051",   17.109
"splr",         6,   "3SAT/360 S1684547485-073",    2.961
"splr",         7,   "3SAT/360 S1711406314-093",   12.262
"splr",         8,   "3UNS/360 S1369720750-015",  150.390
"splr",         9,   "3UNS/360  S367138237-029",  331.267
"splr",        10,   "3UNS/360  S680239195-053",  151.182
"splr",        11,   "3UNS/360  S253750560-086",  123.484
"splr",        12,   "3UNS/360 S1028159446-096",  188.553
"splr",        13,   "[SAT] SR2015/m283,  3553",   15.830
"splr",        14,   "[SAT] SR2015/38b,    448",   50.106
"splr",        15,   "[SAT] SR2015/44b,    609",  251.571
"splr",        16,   "[SAT] SC21/b04_s_unknown",  180.438
"splr",        17,   "[SAT] SC21/quad_r21_m22 ",   23.901
"splr",        18,   "[SAT] SC21/toughsat_895s",  343.403
"splr",        19,   "[UNS] SC21/assoc_mult_e3",  158.155
"splr",        20,   "[UNS] SC21/dist4.c      ",  196.131
"splr",        21,   "[UNS] SC21/p01_lb_05    ",  257.615
"splr",        22,   "[UNS] SC21/shift1add    ",   25.688
med:   150.786, max:   343.403,           total: 2997.750
# ~/Repositories/splr@10-07T02:29:39 e4c8c95f@20221002-vdr*
$ cargo install --path . && splr cnfs/a_rphp035_05.cnf
  Installing splr v0.17.0-alpha (/Users/nash/Repositories/splr)
    Updating crates.io index
   Compiling splr v0.17.0-alpha (/Users/nash/Repositories/splr)
    Finished release [optimized] target(s) in 15.77s
   Replacing /Users/nash/.cargo/bin/dmcr
   Replacing /Users/nash/.cargo/bin/splr
    Replaced package `splr v0.17.0-alpha (/Users/nash/Repositories/splr)` with `splr v0.17.0-alpha (/Users/nash/Repositories/splr)` (executables `dmcr`, `splr`)
a_rphp035_05.cnf                                   367,4118 |time:  3349.00
 #conflict:   42464042, #decision:    393169424, #propagate:     1663458479
  Assignment|#rem:      211, #fix:      118, #elm:       38, prg%:  42.5068
      Clause|Remv:    21871, LBD2:     5571, BinC:      398, Perm:     1127
    Conflict|entg:   6.2452, cLvl:  12.3120, bLvl:  10.2429, /cpr:   125.16
    Learning|avrg:   1.8750, trnd:   0.2433, #RST:  2880406, /dpc:     1.06
        misc|vivC:   172551, subC:        0, core:        4, /ppc:    16.39
      Result|file: ./ans_a_rphp035_05.cnf
s UNSATISFIABLE: cnfs/a_rphp035_05.cnf
# ~/Repositories/splr@10-07T03:26:21 e4c8c95f@20221002-vdr*

shnarazk · 2022-10-07T08:28:42Z

a_rphp035_05.cnf                                   367,4118 |time:  3159.27
 #conflict:   36536320, #decision:    341417051, #propagate:     1431463346
  Assignment|#rem:      225, #fix:      104, #elm:       38, prg%:  38.6921
      Clause|Remv:    16846, LBD2:     4154, BinC:      505, Perm:     1423
    Conflict|entg:   6.3123, cLvl:  12.5211, bLvl:  10.6435, /cpr:    99.46
    Learning|avrg:   1.8750, trnd:   0.2201, #RST:  2550483, /dpc:     1.11
        misc|vivC:   166264, subC:        0, core:        3, /ppc:    12.37
      Result|file: ./ans_a_rphp035_05.cnf
s UNSATISFIABLE: cnfs/a_rphp035_05.cnf

# 0.14.1, timeout:2000 on demorgan @ 2022-10-07T16:27:44
# ~/.cargo/bin/splr (0.17.0-alpha) @ 2022-10-07T15:34:56
solver,       num,                       target,     time
"splr",         1,                 "UF250(100)",   74.470
"splr",         2,                "UUF250(100)",  213.637
"splr",         3,   "3SAT/360  S722433227-030",   45.051
"splr",         4,   "3SAT/360 S2032263657-035",    2.751
"splr",         5,   "3SAT/360  S368632549-051",    5.950
"splr",         6,   "3SAT/360 S1684547485-073",   19.577
"splr",         7,   "3SAT/360 S1711406314-093",   13.587
"splr",         8,   "3UNS/360 S1369720750-015",  165.990
"splr",         9,   "3UNS/360  S367138237-029",  356.747
"splr",        10,   "3UNS/360  S680239195-053",  221.738
"splr",        11,   "3UNS/360  S253750560-086",  166.815
"splr",        12,   "3UNS/360 S1028159446-096",  202.110
"splr",        13,   "[SAT] SR2015/m283,  3553",   43.787
"splr",        14,   "[SAT] SR2015/38b,    448",   45.477
"splr",        15,   "[SAT] SR2015/44b,    609",  255.057
"splr",        16,   "[SAT] SC21/b04_s_unknown",  179.384
"splr",        17,   "[SAT] SC21/quad_r21_m22 ",   22.155
"splr",        18,   "[SAT] SC21/toughsat_895s",   39.916
"splr",        19,   "[UNS] SC21/assoc_mult_e3",  143.246
"splr",        20,   "[UNS] SC21/dist4.c      ",  170.202
"splr",        21,   "[UNS] SC21/p01_lb_05    ",  278.085
"splr",        22,   "[UNS] SC21/shift1add    ",   25.523
med:   108.858, max:   356.747,           total: 2691.255
#[2] ~/Repositories/splr@10-07T16:44:56 71409eaf@20221002-vdr*

- fix #188 - feature 'reward_annealing' #187 - `Certificate` handles empty clauses correctly #191 - fix stage calculations #194 - a better clause reduction #195 - SolverError::OutOfRange -> SolverError::InvalidLiteral #198 - SLS #159 #192 #199 - fix a build error without feature 'trail_saving' #202 - fix a build error without feature 'rephase' #205 - two-mode reduction (#208)

shnarazk self-assigned this Oct 2, 2022

shnarazk changed the title ~~intensive vdr adjusting~~ intensive vdr adjusting: a completely different stabilization approach Oct 3, 2022

shnarazk added parameter tuning combinational optimization based on benchmark suits idea My original idea labels Oct 7, 2022

shnarazk linked an issue Oct 8, 2022 that may be closed by this pull request

Stochastic Local Search in Splr #159

Closed

7 tasks

shnarazk force-pushed the 20221002-vdr branch from 3c980d5 to 13ef51e Compare October 8, 2022 14:56

shnarazk linked an issue Oct 9, 2022 that may be closed by this pull request

Add builder pattern to structs #186

Closed

3 tasks

shnarazk mentioned this pull request Oct 10, 2022

Splr-0.17.0 #185

Merged

14 tasks

shnarazk force-pushed the 20221002-vdr branch from f69d0c3 to a434ad7 Compare October 10, 2022 23:20

shnarazk changed the title ~~intensive vdr adjusting: a completely different stabilization approach~~ feature 'reward_annealing' Oct 10, 2022

shnarazk marked this pull request as ready for review October 10, 2022 23:21

shnarazk added 12 commits October 11, 2022 08:31

intensive vdr adjusting

df20e1e

modified: src/solver/search.rs

c590059

modified: src/solver/search.rs

eb792d3

revise the idea and its implementation

de64133

Rework through observation

b24c644

The best so far

7d909fa

(clause vivification) revise selection criteria

ee992f6

(vivify) revise parameters and conditions

3ef31db

vivify.rs: revise vivification parameters

bc48efa

a snapshot of changes on vivification

d3c995c

vivify.rs: revert

117a5c2

add feature 'reward_annealing'

24505f2

shnarazk force-pushed the 20221002-vdr branch from 6a05669 to 24505f2 Compare October 10, 2022 23:32

shnarazk merged commit 04fadb3 into dev-0.17.00 Oct 10, 2022

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feature 'reward_annealing' #187

feature 'reward_annealing' #187

shnarazk commented Oct 2, 2022 •

edited

Loading

shnarazk commented Oct 6, 2022

shnarazk commented Oct 6, 2022

shnarazk commented Oct 7, 2022

feature 'reward_annealing' #187

feature 'reward_annealing' #187

Conversation

shnarazk commented Oct 2, 2022 • edited Loading

reward annealing, activity annealing

shnarazk commented Oct 6, 2022

shnarazk commented Oct 6, 2022

shnarazk commented Oct 7, 2022

shnarazk commented Oct 2, 2022 •

edited

Loading