dev-0.19.0

[shnarazk]

• O(1) Luby iterator #207 (https://github.com/shnarazk/LubySequence)
• Clause reduction may remove clauses that are stored in Var:saved_reason! Ouch! #310
• revise orchestration of clause elimination/reduction/vivification based on the new LubySequence-dviven restart policy An orchestration of Luby restart, re-phasing selection and decision literal selection 20250507 #328
  • set FlagClause::ASSIGN_REASON at/around propagate_by_implication
• Implement focused search mode like Kissat #314 -> Hotspot seeker 20260331 #315
• Reconsider LBD at The last day of The Late Show with Stephan Colbert #330
• Fix correctness of clause vivification 20260526 #332
• polarity at best assignments as rephrase target base #335

The target line defined by Kissat

solver,       num,                       target,     time
"kissat",       1,"0a8a4c28d27228e954354ea0a6e7f16c-sum_of_three_cubes_42_known_representation.cnf",  126.650
"kissat",       2,"1a936d41e3439d602c3ddcf96458a38c-arles_thres10_p10_r8185.cnf",    0.007
"kissat",       3,"2b4467a5ac4ac41b36d4c3432b07f767-oddball_69_5_tto_zp.normalised.cnf", 1065.746
"kissat",       4,"3a1f1b4b9a521737cc760017fe9d8b43-MVRoundRobin_n16_d10_v3.cnf",  TIMEOUT
"kissat",       5,"4ba2c1aa580b6497df6baf5e7e2c87be-at-least-two-vmpc_28.cnf", 1120.135
"kissat",       6,"5aed29ce52192a55ffbd2a6f340017e7-oisc-subrv-and-nested-12.cnf",  TIMEOUT
"kissat",       7,"6cb995b1c550beb579c53e27f6ca881a-RoundRobin_n16_d13.cnf", 1116.055
"kissat",       8,"7a044c997ede14d00002f1db39d45170-sum_of_3_cubes_37_bits_87.cnf",  650.169
"kissat",       9,"8a05f9b6bf49285e40d0a197967ea5d3-arles_thres10_p10_r7466.cnf",    0.696
"kissat",      10,"9a839badecb20dcf505ec79eedd3753a-anbul-dated-5-15-u.cnf",   15.028
"kissat",      11,"a0bcdaffb0ea36b678899fd86bdc7f18-arles_thres10_p10_r8186.cnf",    0.018
"kissat",      12,"b1c8eaa002ac2fa1c8bfd1002738e78e-cliquecolouring_n15_k7_c6.sanitized.cnf",  TIMEOUT
"kissat",      13,"c0bd86bd7ca2c65e44311de374168150-goldcrest-and-14.cnf",  528.235
"kissat",      14,"d0298807e51730261ef65db827dcd70f-Break_triple_16_70.xml.cnf",   23.596
"kissat",      15,"e2d2b011b0805782df6adba648db92e8-59-129706.cnf",  405.921
"kissat",      16,"f0bafebdcce23ccfbaf6c27a7522069b-div-mitern172.cnf",   26.040
"kissat",      17,              "sc2025(13/16)", 4378.523
# med:   126.650, max:  1120.135,total except 3 timeouts: 5078.296

The old target

# ~/.cargo/bin/splr (0.19.0-rc2) @ 2026-03-19T19:34:20
solver,       num,                       target,     time
"splr",         1,"0a8a4c28d27228e954354ea0a6e7f16c-sum_of_three_cubes_42_known_representation.cnf",  TIMEOUT
"splr",         2,"1a936d41e3439d602c3ddcf96458a38c-arles_thres10_p10_r8185.cnf",    0.678
"splr",         3,"2b4467a5ac4ac41b36d4c3432b07f767-oddball_69_5_tto_zp.normalised.cnf",  TIMEOUT
"splr",         4,"3a1f1b4b9a521737cc760017fe9d8b43-MVRoundRobin_n16_d10_v3.cnf",  TIMEOUT
"splr",         5,"4ba2c1aa580b6497df6baf5e7e2c87be-at-least-two-vmpc_28.cnf",  239.209
"splr",         6,"5aed29ce52192a55ffbd2a6f340017e7-oisc-subrv-and-nested-12.cnf",  TIMEOUT
"splr",         7,"6cb995b1c550beb579c53e27f6ca881a-RoundRobin_n16_d13.cnf",  TIMEOUT
"splr",         8,"7a044c997ede14d00002f1db39d45170-sum_of_3_cubes_37_bits_87.cnf", 1445.579
"splr",         9,"8a05f9b6bf49285e40d0a197967ea5d3-arles_thres10_p10_r7466.cnf",    0.680
"splr",        10,"9a839badecb20dcf505ec79eedd3753a-anbul-dated-5-15-u.cnf",   44.637
"splr",        11,"a0bcdaffb0ea36b678899fd86bdc7f18-arles_thres10_p10_r8186.cnf",    0.011
"splr",        12,"b1c8eaa002ac2fa1c8bfd1002738e78e-cliquecolouring_n15_k7_c6.sanitized.cnf",  TIMEOUT
"splr",        13,"c0bd86bd7ca2c65e44311de374168150-goldcrest-and-14.cnf",  TIMEOUT
"splr",        14,"d0298807e51730261ef65db827dcd70f-Break_triple_16_70.xml.cnf", 1255.024
"splr",        15,"e2d2b011b0805782df6adba648db92e8-59-129706.cnf",  TIMEOUT
"splr",        16,"f0bafebdcce23ccfbaf6c27a7522069b-div-mitern172.cnf",  183.734
"splr",        17,               "sc2025(8/16)",19169.793
med:       114.186, max:  1445.579, total except 8 timeouts: 3169.552
[I] ~/Reposi/splr (dev-0.19.0|)

The best in this branch so far

36ff02c

"splr"    ,  1,"0a8a4c28d27228e954354ea0a6e7f16c-sum_of_three_cubes_42_kno",  TIMEOUT
"splr"    ,  2,"1a936d41e3439d602c3ddcf96458a38c-arles_thres10_p10_r8185.c",    0.688
"splr"    ,  3,"2b4467a5ac4ac41b36d4c3432b07f767-oddball_69_5_tto_zp.norma",   72.704
"splr"    ,  4,"3a1f1b4b9a521737cc760017fe9d8b43-MVRoundRobin_n16_d10_v3.c",  TIMEOUT
"splr"    ,  5, "4ba2c1aa580b6497df6baf5e7e2c87be-at-least-two-vmpc_28.cnf",  142.824
"splr"    ,  6,"5aed29ce52192a55ffbd2a6f340017e7-oisc-subrv-and-nested-12.",  TIMEOUT
"splr"    ,  7,"6cb995b1c550beb579c53e27f6ca881a-RoundRobin_n16_d13.cnf"   ,  TIMEOUT
"splr"    ,  8,"7a044c997ede14d00002f1db39d45170-sum_of_3_cubes_37_bits_87", 1614.967
"splr"    ,  9,"8a05f9b6bf49285e40d0a197967ea5d3-arles_thres10_p10_r7466.c",    0.012
"splr"    , 10,   "9a839badecb20dcf505ec79eedd3753a-anbul-dated-5-15-u.cnf",  243.219
"splr"    , 11,"a0bcdaffb0ea36b678899fd86bdc7f18-arles_thres10_p10_r8186.c",    0.013
"splr"    , 12,"b1c8eaa002ac2fa1c8bfd1002738e78e-cliquecolouring_n15_k7_c6",  TIMEOUT
"splr"    , 13,"c0bd86bd7ca2c65e44311de374168150-goldcrest-and-14.cnf"     ,  TIMEOUT
"splr"    , 14,"d0298807e51730261ef65db827dcd70f-Break_triple_16_70.xml.cn", 1303.459
"splr"    , 15,            "e2d2b011b0805782df6adba648db92e8-59-129706.cnf", 1135.450
"splr"    , 16,        "f0bafebdcce23ccfbaf6c27a7522069b-div-mitern172.cnf",  370.608
med:   193.022, max:  1614.967,total except 6 timeouts: 4883.944