Paper revision: reviewer response tracker

[isPANN]

Revision plan in response to PC review feedback.

Paper

P1. Upgrade from empirical to mechanistic

• Engage existing literature on multiplier SAT hardness (Beame & Pitassi, Cook/Haken, Biere).
• Formalize ripple-carry multiplier structure: carry chain length, pathwidth, narrow-channel property along critical path.
• Define a measurable structural indicator (candidates: average implication count per single-variable assumption; effective cut size around focus variable; carry-chain segment depth). Prefer general-purpose metrics over multiplier-specific ones so they can later serve as transformation cost functions.
• Show the indicator correlates with HB's per-node γ behavior.
• Replace observation-level claims with mechanism-level claims (e.g., "k-bit boundary around a k+1-adder region forces internal state when k boundary bits are decided").

P2. Define method scope explicitly

• Use the structural indicator from P1 to predict, before running experiments, whether HB should work on a given circuit class.
• Validate predictions empirically on contrasting circuits (Wallace-tree / Dadda multipliers; AES/SHA preimage as negative example).
• Uncomment and reframe the random 3-CNF limitation experiment (main.tex L695-719) as a positive Scope and Applicability section.

P3. Discussion: structure-preserving compilation as future direction

• Add a Discussion paragraph: rather than running HB on arbitrary circuit representations, transform problems into the structural form HB exploits, using P1's metric as a cost function in existing logic synthesis tools (ABC, Yosys).

Code

C1. Remove the tensor wrapping layer

• Replace GenericTensorNetworks-based region enumeration with direct bitset enumeration on the branching path.
• Keep tensor contraction available as an optional backend for reproducibility, but not the default.
• Expose a RegionEnumerator interface; tensor and bitset are two implementations.
• Update src/branch_table/contraction.jl and related code.

C2. Migrate core to C++/Rust

• C++ for orchestration / SAT solver integration (CaDiCaL/Kissat); Rust for OB rule-synthesis components.
• Scope: CNF parsing, region enumeration (bitset), GreedyMerge, HB driver, CaDiCaL/Kissat integration. No tensor library.

Reviewer source quotes (for reference)

R1 weaknesses

• "results look very specific to the chosen example"
• "tuned their approach on this particular example while they did not try to optimize March"
• "In the introduction I did not understand what the tensor approach does"
• "I do not get what the update Q part does in that algorithm"
• "Heule's early work also considered double-lookahead which looks very similar to the tensor approach"
• "running times of the cubing are not compared"
• Reproducibility: "paper does not discuss cubing times"; "supplementary part does not include the considered CNFs"

R2 weaknesses

• "evaluation only uses factoring with ripple-carry adders, only 52- and 56-bit instances, and only 10 instances per bit-length"
• "tensor network formulation is non-essential ... tensor language adds no algorithmic advantage at the region sizes used (6-8 variables, 4-12 configurations)"
• "gamma=1 contribution is conflated with the branching contribution"
• "Multiplier circuits are well understood. The paper should try to explain why 90% of steps are reductions in terms of carry-chain propagation and output constraints"
• "cutoff condition |σ_dec| × |σ_all| > θ is ad hoc"
• "comparison against the recently proposed cubing algorithm by Battleman, Reeves, and Heule based on proof prefixes is missing"