Open
Conversation
…lysis Port CaDiCaL's bump_clause technique: when a redundant clause is encountered as a reason during conflict analysis, recompute its LBD using current variable levels and update if improved. This allows clauses to be promoted to higher tiers (lower LBD = more protected from deletion) as the search progresses. Previously this was attempted but disabled (commented-out update_lbd calls). The change also marks ALL redundant reason clauses as "used" (not just high-LBD ones), matching CaDiCaL's approach where every reason clause gets bumped regardless of current tier. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Port CaDiCaL's bumpreason technique: after learning a conflict clause, bump the activity of literals in the reason clauses of the learned clause's literals (depth 1). This helps the VSADS variable activity heuristic focus on the broader conflict neighborhood, not just the variables directly in the learned clause. For each non-UIP literal in the learned clause, look at its antecedent (reason clause) and bump all other literals in that reason. This is CaDiCaL's proven technique for improving decision quality. Controlled by --bumpreason (default: on). Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Port CaDiCaL's EVSIDS scoring: instead of halving all variable activities every N decisions (old VSADS approach), grow the activity increment by factor 1/0.95 after each conflict. This gives exponentially more weight to variables involved in recent conflicts, which is the standard approach in modern SAT solvers since MiniSat 2. When the increment exceeds 1e100, all activities are rescaled by dividing by the increment. This prevents floating-point overflow while maintaining relative ordering. The old periodic halving was a coarser approximation of the same effect. EVSIDS provides smoother, conflict-aligned decay that better tracks the current "frontier" of the search. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
msoos
force-pushed
the
synth-better-cubes-lbd-vsids-change
branch
from
4a2a953 to
6192398
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
2 participants
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.
Check how this would affect Ganak. Maybe it's not as good in a counting scenario.