Chrono_BT 2025 #296
Draft
Chrono_BT 2025 #296
Conversation
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
- modified: src/assign/propagate.rs - modified: src/assign/stack.rs - modified: src/solver/conflict.rs
Change default c_cbt_thr from 100 to 4 Force chronobt to true when chrono_BT feature is enabled by removing original conditional check
There was a problem hiding this comment.
Pull Request Overview
This PR updates the conflict handling logic, configuration thresholds, and refactors field access patterns while removing several debug assertions. Key changes include:
- Changing the conflict condition in the chrono_BT block by hardcoding the 'chronobt' flag.
- Refactoring field access in conflict resolution, assignment stack, and propagation modules.
- Adjusting configuration parameters (e.g., reducing c_cbt_thr) and commenting out debug assertions.
Reviewed Changes
Copilot reviewed 5 out of 5 changed files in this pull request and generated 2 comments.
Show a summary per file
| File | Description |
|---|---|
| src/solver/conflict.rs | Updated chrono_BT logic, removed match panic branch, and changed conflict handling. |
| src/config.rs | Lowered the c_cbt_thr configuration value. |
| src/cdb/vivify.rs | Commented out several debug assertions. |
| src/assign/stack.rs | Refactored field access from separate arrays to the Var struct. |
| src/assign/propagate.rs | Updated field access and commented out additional debug assertions. |
Comments suppressed due to low confidence (4)
src/solver/conflict.rs:45
- Hardcoding 'chronobt' to true bypasses the intended conflict threshold condition; consider restoring the original logic or documenting why this change is necessary.
let chronobt = true;
src/solver/conflict.rs:70
- Changing the return value from Ok(()) to Ok(c.rank) alters the function's output and may impact downstream logic; please confirm that this change aligns with the overall API design.
return Ok(c.rank);
src/config.rs:95
- Reducing the configuration value for 'c_cbt_thr' from 100 to 4 significantly alters conflict handling thresholds; ensure that this change is intentional and supported by test cases.
c_cbt_thr: 4, // 100,
src/assign/propagate.rs:644
- [nitpick] Ensure that removing this debug assertion does not let invariant violations go unnoticed during propagation; consider implementing alternative safeguards if necessary.
// debug_assert!(!self.var[cached.vi()].is(FlagVar::ELIMINATED));
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.
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.
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.
Comment out the assert_eq! comparing decision levels and add a note to align with the Implication case logic
handle cases on biclause. Add debug logs and ANSI color constants
Ensure that during conflict analysis for chronological backtracking, the negated literal (!l) is pushed to the learnt clause rather than l
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 chronobt definitions and the assert in handle_conflict, using compile-time cfg!(feature = "chrono_BT") checks instead.
Inline conditional in cancel_until call to choose the rollback level and remove the chbt flag and its associated debug assertion.
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.
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.
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.
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.
Owner
Author
|
Owner
Author
|
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.
No description provided.