Bounded-width VE canonicalizer (representation preprocessing)#39
Merged
Conversation
Static, width-aware constraint-network preprocessing. `bounded_ve_canonicalize` (src/preprocessing/canonicalize.jl) generalizes `precontract_degree2!` from "eliminate any degree-2 variable" to "eliminate any variable whose elimination width stays <= budget_B, in weighted-min-fill order". `budget_B` is the single fine<->coarse knob; unlike degree-2-greedy (which raised treewidth), min-fill ordering with a per-step width cap cuts the treewidth proxy 50-70%, shrinking the branch set and giving a several-fold end-to-end speedup on factoring. Protected read-out variables (e.g. factor bits) are never eliminated, so they survive into the reduced network and are read directly off the solution via `orig_to_new` -- no variable-elimination back-substitution. Supporting changes: - DiffLookaheadSelector (branch_table/selector.jl): difficulty-guided lookahead selector that cuts the search tree vs MostOccurrenceSelector. - TensorData config indices widened UInt16 -> UInt32 (core/static.jl, branching/propagate.jl, branch_table/contraction.jl), lifting the per-tensor arity cap from 16 to 32 so the canonicalizer can use larger budgets. - test/canonicalize.jl: canonicalizing a factoring instance preserves satisfiability, keeps protected factor-bit vars alive, shrinks the branch set, and reads correct factors off the solution (a*b==N). Runs early in runtests.jl so the suite reaches it before the cadical-dependent test. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
isPANN
force-pushed
the
representation-preprocessing
branch
from
June 24, 2026 19:41
5d2f732 to
eb47a15
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.
Summary
Adds a static, width-aware constraint-network canonicalizer — bounded-width variable elimination — as a preprocessing step, plus the supporting selector and representation widening. Eliminating structurally-cheap variables before search shrinks the branch set and gives a several-fold end-to-end speedup on factoring (4.5–9.2× median at 16–20 bit), with answers read straight off the reduced network.
What's in
src/preprocessing/canonicalize.jl—bounded_ve_canonicalize(cn; budget_B, protected, order=:weighted_min_fill). Generalizesprecontract_degree2!from "eliminate any degree-2 variable" to "eliminate any variable whose elimination width stays≤ budget_B, in weighted-min-fill order".budget_Bis the single fine↔coarse knob. Unlike degree-2-greedy (which raised treewidth), min-fill ordering with a per-step width cap cuts the treewidth proxy 50–70%.protectedvariables (e.g. factor bits) are never eliminated, so they survive into the reduced network and their values are read directly viaresult.orig_to_new— no variable-elimination back-substitution.DiffLookaheadSelector(branch_table/selector.jl): difficulty-guided lookahead selector that cuts the search tree vsMostOccurrenceSelector.TensorDataconfig indices widenedUInt16 → UInt32(core/static.jl,branching/propagate.jl,branch_table/contraction.jl): lifts the per-tensor arity cap from 16 to 32 so the canonicalizer can use larger budgets.budget_Bis a plain hyperparameter.Tests
test/canonicalize.jl: canonicalizing a factoring instance preserves satisfiability, keeps the protected factor-bit variables alive, shrinks the branch set, and the factors are read off the solution (a*b == N). 16/16 pass. Runs early inruntests.jlso the suite reaches it before the cadical-dependentsolve_factoringtest.solve_factoringcadical path (missinglibcadical_mine.dylib), unrelated to this branch.🤖 Generated with Claude Code