dev-0.19.0 by shnarazk · Pull Request #307 · shnarazk/splr

shnarazk · 2026-03-14T12:21:03Z

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

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

- Switch to the O(1) Luby iterator. Now Luby sequence is used for - trigger for restarts, clause elimination, and clause vivification - clause DB size after clause reduction - `ClauseDBIF::reduce` can run at any decision level, and runs every 40,000 conflicts

* feat: pass cdb to all relevant functions * feat(reduce): switch to FlagClause-based implementation

…r non unsafe_access feature

…h fewer stages

shnarazk · 2026-05-26T09:48:22Z

invalid [`6645b4c`] with a wrong vivifier

num,target                                                      ,    time
  1,"0a8a4c28d27228e954354ea0a6e7f16c-sum_of_three_cubes_42_kno",4431.811
  2,"1a936d41e3439d602c3ddcf96458a38c-arles_thres10_p10_r8185.c",   0.016
  3,"2b4467a5ac4ac41b36d4c3432b07f767-oddball_69_5_tto_zp.norma",2101.005
  4,"3a1f1b4b9a521737cc760017fe9d8b43-MVRoundRobin_n16_d10_v3.c", TIMEOUT
  5,"4ba2c1aa580b6497df6baf5e7e2c87be-at-least-two-vmpc_28.cnf" , 332.773
  6,"5aed29ce52192a55ffbd2a6f340017e7-oisc-subrv-and-nested-12.",1870.920
  7,"6cb995b1c550beb579c53e27f6ca881a-RoundRobin_n16_d13.cnf"   , TIMEOUT
  8,"7a044c997ede14d00002f1db39d45170-sum_of_3_cubes_37_bits_87",3525.610
  9,"8a05f9b6bf49285e40d0a197967ea5d3-arles_thres10_p10_r7466.c",   0.680
 10,"9a839badecb20dcf505ec79eedd3753a-anbul-dated-5-15-u.cnf"   ,  35.784
 11,"a0bcdaffb0ea36b678899fd86bdc7f18-arles_thres10_p10_r8186.c",   0.058
 12,"b1c8eaa002ac2fa1c8bfd1002738e78e-cliquecolouring_n15_k7_c6", TIMEOUT
 13,"c0bd86bd7ca2c65e44311de374168150-goldcrest-and-14.cnf"     , 322.588
 14,"d0298807e51730261ef65db827dcd70f-Break_triple_16_70.xml.cn",1197.987
 15,"e2d2b011b0805782df6adba648db92e8-59-129706.cnf"            ,1010.550
 16,"f0bafebdcce23ccfbaf6c27a7522069b-div-mitern172.cnf"        , 327.236
"splr"    , med:   332.773, max:  4431.811,total except 3 timeouts:15157.018

chore: open PR

644a0a8

shnarazk self-assigned this Mar 14, 2026

shnarazk linked an issue Mar 14, 2026 that may be closed by this pull request

O(1) Luby iterator #207

Open

shnarazk added 3 commits March 14, 2026 21:55

feat(Luby): implement LubySequence

266408b

fix: bump version to 0.19.0-rc1

6939364

fix: add LubySegment::as_n

89e5afe

shnarazk force-pushed the dev-0.19.0 branch from acf4393 to 89e5afe Compare March 14, 2026 13:04

shnarazk linked an issue Mar 14, 2026 that may be closed by this pull request

ROADMAP #299

Open

3 tasks

shnarazk added 19 commits March 15, 2026 08:48

refactor(luby): update stage and search (WIP)

9e2481d

Restart NG 20260317 (#308)

6a5e21b

* feat: pass cdb to all relevant functions * feat(reduce): switch to FlagClause-based implementation

refactor(luby): remove the old Luby implementation

773f324

bump version to 0.19.0-rc2

04f0542

chore(flake): add drat-trim

7fe2ce0

chore(flake): add kissat

b2035c8

chore: update flake.lock

a778070

chore: ignore *.cnf*

3b3adda

chore(direnv): add .envrc

2aa4ee9

chore: add proof.drat to .gitignore

c50f100

refactor: simplify RuductionType

9c19858

refactor: define local vars

e08063d

doc: wording

6418663

optimize(reduce): add a variation as comment

ca81944

refactor: remove feature 'two_mode_reduction'

4d83d4a

refactor: remove ReductionType

71c4973

docs: mention BT_deepen at features

1207b8f

refactor: rename reverse_activity_sum to inactivity_sum

20564d2

shnarazk linked an issue Mar 20, 2026 that may be closed by this pull request

Clause reduction may remove clauses that are stored in Var:saved_reason! Ouch! #310

Closed

shnarazk added 2 commits March 20, 2026 16:05

fix(trail_saving): clear saved_trail if an implication clause is reduced

43aab98

chore: delete obsolete comment

3323fd9

shnarazk added 15 commits May 25, 2026 19:43

fix: use valid stats entries in result file and use valid fields unde…

fc340ee

…r non unsafe_access feature

ext(reduce): a tiny tweak

3b72b92

feat: a tiny tweak

8422725

fix: check the number of unasserted vars before and after RESTART.

d17b77c

feat: remove FlagClause::YOUNG

9ef6c23

fix(core): another fix after inconsistent assertion

8d7ef2e

feat(reduce): check ASSIGN_REASON after tier1 and tier2

534afb9

chore: cargo clippy

cb99eb8

feat: add AssignStack::literal_block_distance_current

f6daab3

exp: save lbd2 in the current assignment and use rephase rotation wit…

464b47a

…h fewer stages

chore: clean up

9882cf3

chore: update flake

46fec66

chore: bump to version 0.19.0-rc6

a70ae7f

chore(doc): update algorithm.typst

a5953d3

chore(doc): add placeholder for correctness of 0.19.0 to README.md

ce38bb0

shnarazk force-pushed the dev-0.19.0 branch from 56884cc to ce38bb0 Compare May 25, 2026 12:03

shnarazk added 6 commits May 25, 2026 21:04

ditto

fcf8c59

chore(doc): update correctness

336a5a3

chore(doc): trim long filenames

c381b70

chore(doc): use tt font

6cc5742

chore(doc): add the number of vars

e55a7d1

chore(doc): failed to verify

a5b50b4

shnarazk added 7 commits May 29, 2026 13:39

feat: add the target cnf

3f941f1

chore(doc): update README.md

f17979d

fix(vivify): shrinked clauses were just killed!

2e038ac

fix(bestphase): count only !FlagVar::ELIMINATED

44f5444

chore: update flake

9eaed95

chore: update flake

831d398

chore: bump to version 0.19.0-rc7

9aaba38

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

dev-0.19.0#307

dev-0.19.0#307
shnarazk wants to merge 178 commits into
mainfrom
dev-0.19.0

shnarazk commented Mar 14, 2026 •

edited

Loading

Uh oh!

shnarazk commented May 26, 2026 •

edited

Loading

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Conversation

shnarazk commented Mar 14, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

The target line defined by Kissat

The old target

The best in this branch so far

Uh oh!

shnarazk commented May 26, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

invalid [6645b4c] with a wrong vivifier

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

shnarazk commented Mar 14, 2026 •

edited

Loading

shnarazk commented May 26, 2026 •

edited

Loading

invalid [`6645b4c`] with a wrong vivifier