単位伝播と矛盾解析

[shnarazk]

どっちでもいいくらいだが、ふーむ、どちらかといえば矛盾解析に使われた節に報酬を与えようかな。

実は節を削減する方が探索空間を絞ることになるのでは。古い節を捨てるなら、直近の制約によってのみドライブされるのでそうなのでは。しかし古いものが残るなら遷移先はむしろ大きくなるような。

単位伝播を起こした節に報酬

# ~/.cargo/target/release/splr (0.18.0-dev5) @ 2024-08-16T21:00:53
solver,       num,                       target,     time
".cargo/target/release/splr",  1,                 "UF250(100)",   57.717
".cargo/target/release/splr",  2,                "UUF250(100)",  132.247
".cargo/target/release/splr",  3,   "3SAT/360  S722433227-030", 1175.447
”.cargo/target/release/splr",  4,   "3SAT/360 S2032263657-035",   13.877
".cargo/target/release/splr",  5,   "3SAT/360  S368632549-051",   10.777
".cargo/target/release/splr",  6,   "3SAT/360 S1684547485-073",   16.491
".cargo/target/release/splr",  7,   "3SAT/360 S1711406314-093",   58.351
".cargo/target/release/splr",  8,   "3UNS/360 S1369720750-015",  270.696
".cargo/target/release/splr",  9,   "3UNS/360  S367138237-029",  648.134
".cargo/target/release/splr", 10,   "3UNS/360  S680239195-053",  448.037
".cargo/target/release/splr", 11,   "3UNS/360  S253750560-086",  270.027
".cargo/target/release/splr", 12,   "3UNS/360 S1028159446-096",  248.208
".cargo/target/release/splr", 13,   "[SAT] SR2015/m283,  3553",   33.378
".cargo/target/release/splr", 14,   "[SAT] SR2015/38b,    448",    7.480
".cargo/target/release/splr", 15,   "[SAT] SR2015/44b,    609",   67.772
".cargo/target/release/splr", 16,   "[SAT] SC21/b04_s_unknown",  207.962
".cargo/target/release/splr", 17,   "[SAT] SC21/quad_r21_m22 ",  116.288
".cargo/target/release/splr", 18,   "[SAT] SC21/toughsat_895s",  119.816
".cargo/target/release/splr", 19,   "[UNS] SC21/assoc_mult_e3",  277.147
".cargo/target/release/splr", 20,   "[UNS] SC21/dist4.c      ",  380.545
".cargo/target/release/splr", 21,   "[UNS] SC21/p01_lb_05    ",  522.197
".cargo/target/release/splr", 22,   "[UNS] SC21/shift1add    ",  183.347
med:   157.797, max:  1175.447,           total: 5265.941

矛盾解析に使われた節に報酬

# ~/.cargo/target/release/splr (0.18.0-dev5) @ 2024-08-16T23:38:48
solver,       num,                       target,     time
".cargo/target/release/splr",  1,                 "UF250(100)",   48.544
".cargo/target/release/splr",  2,                "UUF250(100)",  130.968
".cargo/target/release/splr",  3,   "3SAT/360  S722433227-030",  778.429
".cargo/target/release/splr",  4,   "3SAT/360 S2032263657-035",   17.508
".cargo/target/release/splr",  5,   "3SAT/360  S368632549-051",  209.554
".cargo/target/release/splr",  6,   "3SAT/360 S1684547485-073",    0.790
".cargo/target/release/splr",  7,   "3SAT/360 S1711406314-093",   30.985
".cargo/target/release/splr",  8,   "3UNS/360 S1369720750-015",  195.595
".cargo/target/release/splr",  9,   "3UNS/360  S367138237-029",  697.246
".cargo/target/release/splr", 10,   "3UNS/360  S680239195-053",  451.823
".cargo/target/release/splr", 11,   "3UNS/360  S253750560-086",  269.028
".cargo/target/release/splr", 12,   "3UNS/360 S1028159446-096",  348.813
".cargo/target/release/splr", 13,   "[SAT] SR2015/m283,  3553",   36.156
".cargo/target/release/splr", 14,   "[SAT] SR2015/38b,    448",   13.074
".cargo/target/release/splr", 15,   "[SAT] SR2015/44b,    609",  273.015
".cargo/target/release/splr", 16,   "[SAT] SC21/b04_s_unknown",  110.060
".cargo/target/release/splr", 17,   "[SAT] SC21/quad_r21_m22 ",  512.045
".cargo/target/release/splr", 18,   "[SAT] SC21/toughsat_895s",  125.333
".cargo/target/release/splr", 19,   "[UNS] SC21/assoc_mult_e3",  360.004
".cargo/target/release/splr", 20,   "[UNS] SC21/dist4.c      ",  450.491
".cargo/target/release/splr", 21,   "[UNS] SC21/p01_lb_05    ",  697.139
".cargo/target/release/splr", 22,   "[UNS] SC21/shift1add    ",   76.536
med:   202.575, max:   778.429,           total: 5833.136