Experiment plan

[isPANN]

1. Technical Claims (Critical)

1.1 "Provably minimizing" Claim ✅ Fixed

• Issue: Abstract claims "provably minimizing γ" but uses greedy heuristic for NP-hard problem
• Status: Removed "provably", changed to "low-γ"

1.2 Measure Choice Lacks Theoretical Justification

• Issue: Δρ(c) = "number of newly fixed variables" not justified as good measure for SAT
• Issue: Table 3 shows NumUnfixedTensors (worse Knuth variance) outperforms NumUnfixedVars, undercutting "principled γ
  minimization" narrative
• Suggestion: Honestly acknowledge γ is a heuristic guide, not a theoretical guarantee
• Suggestion: Show correlation between γ and actual subtree sizes on small instances

1.3 Completeness/Soundness Argument Incomplete

• Issue: How is completeness ensured when branches overlap or local configs are globally inconsistent?
• Issue: Do you ensure disjointness or rely on propagation to eliminate redundancy?
• Suggestion: Add proof sketch or more explicit discussion

---

2. HOB/CnC Integration

2.1 Cutoff Condition is Ad Hoc

• Issue: |σ_dec| × |σ_all| > θ has no rationale—why use product vs sum?
• Issue: No experiments varying θ
• Issue: No analysis of how OB-specific features (γ plateaus, region sizes) interact with cutoff
• Suggestion: Add θ sensitivity experiment, or acknowledge borrowed heuristic from CnC

2.2 Cube Difficulty Shift Not Analyzed

• Issue: Table 6 shows difficulty shifts from cubing to conquering (Avg. Dec. per cube rises)
• Issue: No systematic analysis of this trade-off or optimization for end-to-end time
• Suggestion: Analyze trade-off or acknowledge as limitation

---

3. Experimental Evaluation

3.1 Narrow Benchmark Scope

• Issue: Only factorization circuits (single domain) and tiny random 3-CNF (150 vars)
• Missing: SAT competition benchmarks, graph-coloring, verification, cryptographic circuits
• Suggestion: Add more benchmark types OR explicitly scope the contribution

3.2 Weak/Missing Baselines

• Issue: DPLL is a straw man in 2025; NaiveBranch is custom weak baseline
• Missing: AlphaMapleSAT, other advanced cubers, SAT+CAS pipelines, strong lookahead solvers
• Suggestion: Add AlphaMapleSAT comparison or explain why not included

3.3 Wall-clock Performance ✅ Partially Addressed

• Issue: OB often slower than CDCL (Table 5: 32-bit 0.61s vs 0.28s; 40-bit 11.37s vs 1.97s)
• Status: Reframed to focus on conflicts; added amortization example (191350169: 8.5× speedup)
• Remaining: Could add more analysis of when overhead is/isn't amortized

3.4 Single-Machine Evaluation

• Issue: Only MacBook Air, no parallel CnC execution
• Suggestion: Acknowledge as proof-of-concept OR add parallel experiments

---

4. Algorithmic Details Insufficient for Reproduction

4.1 Region Selection Unclear

• Issue: "Region" definition (graph neighborhood, max depth, max_tensors) buried in details
• Issue: Algorithm 1 OBSolve has caption but no pseudocode
• Suggestion: Add complete pseudocode; clarify region construction rules, tie-breaking

4.2 Tensor Construction Vague

• Issue: How CNF/Tseitin gates map to tensors not clearly specified
• Issue: Contraction order selection not explained
• Suggestion: Add detailed specification

4.3 Greedy Merge Details Missing

• Issue: Stopping condition, tie-breaking, branch weight reuse not spelled out
• Suggestion: Add details in main text (Appendix Example 3 is too toy)

---

5. Scalability Analysis Insufficient

5.1 Runtime Breakdown Missing

• Issue: No quantitative analysis of time spent in contraction vs greedy merge vs propagation
• Suggestion: Add profiling data for 40-bit and 44-bit instances

5.2 Region Size Behavior at Scale

• Issue: No evidence that typical region sizes remain small on larger/denser instances
• Issue: Real formulas can have large local treewidth
• Suggestion: Analyze or acknowledge limitation

5.3 Memory Usage

• Issue: No discussion of memory overhead from caching branch tables per region
• Suggestion: Add memory analysis

---

6. Missing Related Work

6.1 Citations/Discussions to Add
Work: AlphaMapleSAT (2401.13770)
Relevance: MCTS-based cubing; head-to-head comparison needed

Work: ImitSAT (2509.25411)
Relevance: ML-guided CDCL branching; potentially complementary

Work: Exact SAT algorithms (2101.08637, 2507.14504)
Relevance: Branching via nonstandard measures

Work: Shati et al. 2021
Relevance: SAT-based optimal decision trees

Work: Smirnov et al. 2021
Relevance: PB optimization via implicit hitting sets (related to set-cover view)

Work: Torralba 2018
Relevance: Dominance techniques for search pruning

---

7. Presentation Issues

7.1 Table Formatting

• Issue: Some tables have extraction artifacts (Table 1 headers/bit-length alignment)
• Suggestion: Review and fix formatting

7.2 Figure 2(b)

• Issue: "Pareto-optimal frontier" not rigorously defined; only one instance shown
• Suggestion: Add aggregate plot across all instances of same bit-length

7.3 Solver Configuration

• Issue: Not stated whether single-threaded, whether inprocessing disabled for fair comparison
• Suggestion: Add solver configuration table for reproducibility

7.4 Eq. (3) Clarity

• Issue: |σ_dec| × |σ_all| notation is opaque
• Suggestion: Add sentence explaining why product (vs sum or just |σ_dec|)