And revise vivification 20260304#302
Merged
Merged
Conversation
shnarazk
added a commit
that referenced
this pull request
Mar 6, 2026
* Bump version to 0.18.0-dev0 * Remove feature 'incremental_solver' * modified: Cargo.toml * Fix f64 ordering (401fa3c) * Fix `Ord::cmp` for `OrderedProxy<T>` (see #277) * Fix bugs in an unused function * 20250202 refactor primitive types (#288) * Bump version to 0.18.0-dev1 * Reorganize types/* * modified: Cargo.lock * cargo cllipy: replace args().last() with args().next_back() * Activate "chrono_BT" * modified: Cargo.toml * Fix accesing level - modified: src/assign/propagate.rs - modified: src/assign/stack.rs - modified: src/solver/conflict.rs * Comment out debug_assert! calls * Lower CBT threshold to force chrono backtracking Change default c_cbt_thr from 100 to 4 Force chronobt to true when chrono_BT feature is enabled by removing original conditional check * WIP(debug) Simplify chrono_BT conflict handling with if let * Add debug assertion for decision level consistency * tiny changes * Simplify assign_by_implication signature and logic * Better message for assertion errors. * Support BinaryLink in conflict resolution Match on AssignReason to handle BinaryLink and Implication cases separately. Introduce a `chbt` flag to track chrono_BT cancellation logic and enhance debug assertions for the l0 assignment. * Add debug logging for propagation and conflicts * Simplify conflict logic Comment out conflicting_level assignment and cancel_until call in handle_conflict, using a direct assert for level equality. In conflict_analyze, filter out assigned literals when inspecting clauses, simplify the validate_vi! invocation, and clarify the panic println message. * Allow dead code for is_empty and ignore cid * Compute conflicting_level from correct literal Remove redundant conflicting_level reset and adjust its assignment in BinaryLink and Implication to use the higher decision level. Comment out stale debug asserts in conflict_analyze, add doc comments for macros, and simplify literal mapping by dropping unused fields. * Correct spelling errors in comments * Apply implication logic in BinaryLink case Comment out the assert_eq! comparing decision levels and add a note to align with the Implication case logic * cargo clippy (1.87) * WIP: (conflict_analyze) handle cases on biclause. Add debug logs and ANSI color constants * Push negated literal for chrono-BT Ensure that during conflict analysis for chronological backtracking, the negated literal (!l) is pushed to the learnt clause rather than l * Disable hardcoded debug prints and add debug panic Clear magic var-index filters to suppress conditional debug prints in propagation. Comment out leftover printlns in handle_conflict and add panic with debug output on unexpected assignment. * Remove commented code in conflict handler * Inline chrono_BT checks and remove chronobt Remove chronobt definitions and the assert in handle_conflict, using compile-time cfg!(feature = "chrono_BT") checks instead. * Simplify cancel_until logic and remove chbt Inline conditional in cancel_until call to choose the rollback level and remove the chbt flag and its associated debug assertion. * Inline cancel_until logic and remove chbt flag * Track and report chronological backtrack rate * Raise CBT threshold and use exp backtrack check * Add chronological backtrack percentage to status Replace the exploration rate metric with chronological backtrack percentage (cbt%) in the status output. Compute cbt% as 100 * num_chrono_bt / num_conflicts and add a new LogF64Id::ChronologicalBacktrackPercentage variant. * Use tb_lits_ema to control chrono backtracking Add a tb_lits_ema field to State and initialize it in Default. In handle_conflict compute num_bt_lits as the difference in assigned literals, update the EMA, and replace the old chrono_BT threshold check with a condition comparing num_bt_lits against 3×tb_lits_ema. * Use a new counter for STM stage checks Compute stage_counter as the difference between total learnt and chronological backtracks, and use it for stage_ended and prepare_new_stage calls to ensure correct stage management. * (Exp) Refine conflict backtracking and stage counter Import cdb and compute cfl_lvl_lits via asg.stack_len(). Update chrono_BT backtracking to use CDB entanglement EMA and c_lvl, and enforce assign_level+8 < conflicting_level. Simplify stage_counter by removing subtraction of num_chrono_bt. * parameter tuning * cargo clippy * Add Zed debug task for building and running splr * add an alternative chronoBT threshold as comment * clean up debug code * chore: add `.cargo` to .gitignore * a new implementation of chronoBT threshold * optimize (chronoBT): set threshold to 1.6 * optimize (chronoBT): set threshold to 1.65 * optimize(chronoBT): set to 1.6 back * chore: cargo update * feat(chronoBT): revise implementation * a snapshot * feat(chronoBT): implement valid propgation after (current - 1) jump and implement (assign - 1) jump * chore(trail_saving): fix compile errors * chore: cargo clippy * optimize(chrono_BT): tune bt_drift condition * ditto * ditto * optimize(chronoBT): use the number of vars instead of the level gap * optimize(chronoBT): got 1270.409 * optimize(bt_drift): use code in bt-drift-20260301 * optimize(chronoBT): remove idling time * fix: cargo test * And revise vivification 20260304 (#302) * exp: use vivification to reduce redundant *small* clauses * feat(clause): substitute rank_old and DERIVE20 with a counter * fix(trail_saving): give a valid livel to assign_by_implication * refactor(BT_drift): add as feature * chore: use trail_saving feature
shnarazk
added a commit
that referenced
this pull request
Mar 14, 2026
* Chrono_BT 2025 (#296) * Remove feature 'incremental_solver' * Fix f64 ordering (401fa3c) * Fix `Ord::cmp` for `OrderedProxy<T>` (see #277) * 20250202 refactor primitive types (#288) * Simplify assign_by_implication signature and logic * Support BinaryLink in conflict resolution * Push negated literal for chrono-BT * Inline cancel_until logic and remove chbt flag * Use tb_lits_ema to control chrono backtracking * Use a new counter for STM stage checks * Add Zed debug task for building and running splr * feat(chronoBT): implement valid propgation after (current - 1) jump and implement (assign - 1) jump * And revise vivification 20260304 (#302) * feat(clause): substitute rank_old and DERIVE20 with a counter * fix(trail_saving): give a valid level to assign_by_implication * chore: switch to edition 2024; cargo check * feat(log): remove Glucose-style log option * feat(debug): add ClauseDBIF::clause_heatmap * Rename feature `BT_drift` to `BT_deepen` * feat(UI): Show bt_drift rate instead of chrono_BT rate * feat(UI): better coloring for changes of float values * feat(cdb_heatmap): add option `--hide-heatmap`; merge it into `progress` * feat(UI): replace `--hide-heatmap` with `--heatmap` * chore: clean up based on AI previews; add option `--rst-lbd-thr` * fix(CLI): emit an error if '--long-option=value' style is used
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
rank_oldwhich definition is unclear andDERIVE20flag with a new usage counterused. It works!trail_savingon M1chrono_BTon M12922d3c on M3