dev-0.18.0 (2026 version)#300
Merged
Merged
Conversation
* 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
Owner
Author
shnarazk
force-pushed
the
dev-0.18.0-trial2026
branch
from
1dc89df to
5b0144e
Compare
shnarazk
force-pushed
the
dev-0.18.0-trial2026
branch
from
a0649b5 to
fc3ef27
Compare
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
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.
$O(1)$ Luby implementationThe best so far
the best of this branch
22f8937
without BT_drift
So
BT_driftis effective!