Evaluate CnC generalization across circuit topologies, CNF encodings, and structured SAT families

[isPANN]

Background

The hard-regime table in #51 tests one circuit topology and one CNF representation. Even a positive result there would not establish whether structure-aware cubing generalizes across circuit implementations, survives changes in CNF encoding, or extends beyond factoring.

These are three distinct external-validity questions. They must be evaluated in stages rather than as an uncontrolled Cartesian product.

Objective

Determine the scope of the structure-aware cubing claim along three axes:

1. Circuit topology: same arithmetic semantics and targets, different circuit architectures.
2. CNF representation: same native instance and architecture, different fixed CNF encodings.
3. Problem family: different structured SAT semantics with a preregistered native region interpretation.

Every stage must report null, reversed, timeout, and encoding-sensitive results. The final paper claim must be no broader than the stages that pass their registered gates.

Shared protocol

• Use held-out factoring instances in the monolithic-hardness regime established by Build the hard-regime CnC work/span table on 64–80-bit UNSAT factoring #51.
• Keep calibration and test instances disjoint.
• Freeze method parameters before evaluating a stage's held-out instances.
• Use the factoring instance, miter, or structured SAT instance as the statistical unit; cubes are nested observations.
• Record encoding, cubing, conquer, and end-to-end costs separately.
• Use the same pinned Kissat binary and hardware class within every paired comparison.
• Preserve every declared method/instance/resource cell, including timeouts and failures.
• Prohibit per-instance and per-cube encoding selection on held-out data.

G1: circuit-topology generalization

Scope

Use identical hard targets and held-out seeds at two product widths selected from #51, initially 72 and 80 bits. Evaluate at least three substantively different multiplier topologies:

• array-ripple;
• one tree-based design: Wallace or Dadda;
• Karatsuba.

Booth-radix-4 and the second tree design are optional extensions after the required three complete.

For every target, verify that each circuit computes the same product and pins the same target. Keep the CNF encoding fixed for this stage.

Analysis

Report method × architecture interactions for:

• frontier size;
• cubing time;
• conquer work and maximum-cube span;
• p99 time and maximum conflicts;
• finite-worker and end-to-end makespan;
• structural residual measures from Explain the CnC span reduction with a verified residual-structure audit #52.

Gate

Topology generalization passes when the registered span effect has the same direction on at least two of the three required architectures without an unacceptable work increase. Do not redefine the gate after observing held-out results.

G2: CNF-encoding robustness

Valid method/encoding cells

Evaluate the following fixed pipelines on a preregistered subset of G1 containing two architectures, two hard widths, and five held-out seeds per cell:

Cubing interface	Direct CNF conquer	Tseitin CNF conquer
Native region cubing	required	required
march_cu on the corresponding CNF	required	required

The exact encoding definitions must be canonical, versioned, and verified equivalent on the native instance.

march_cu(Tseitin) → Direct and other cross-encoding cube transfers are prohibited unless an explicit verified auxiliary-variable mapping is added in a future issue. March may branch on encoding-specific auxiliary variables, so its cubing and conquer CNF must match.

Fixed residual-compilation modes

If region cubes can be converted to CNF in more than one way, register each as a separate whole-arm policy, for example:

• global encoded CNF plus cube assumptions;
• fresh residual CNF encoded after native propagation.

The policy is fixed for an experimental arm. It may not be selected separately for each cube.

Representation controls

For a smaller preregistered subset, generate five deterministic variable-number permutations per CNF. Verify logical equivalence and report sensitivity separately from encoding-family effects.

Measurements

In addition to the shared metrics, record:

• encoding variables and clauses;
• auxiliary-variable count;
• encoding and residual-compilation time;
• variable ordering/permutation seed;
• branch assignments to primary versus auxiliary variables;
• frontier bytes and minimal-basis bytes from Explain the CnC span reduction with a verified residual-structure audit #52.

Gate

Encoding robustness passes when the principal work/span conclusion does not reverse across both required encodings. If an interaction is present, report an explicitly encoding-conditional claim instead of averaging it away.

G3: structured-SAT family generalization

Proceed in increasing semantic distance from factoring:

1. Arithmetic equivalence checking: UNSAT miters between multiplier or adder implementations.
2. Sequential or grid-structured verification: bounded model checking, local transition systems, or cellular-automata reachability with a native time × state region definition.
3. Structured CSP/SAT: grid/torus coloring or another preregistered relation-tensor family.

The required paper extension is one arithmetic-miter family and one genuinely non-factoring structured family. A new family must provide:

• a versioned native structure and region definition that does not use solver outcomes;
• independent SAT/UNSAT validation on smoke instances;
• a monolithic-hardness screen;
• at least ten held-out instances if it enters the main generalization table;
• the same structure-aware, structure-blind, CNF-only, and monolithic baselines whenever interfaces permit.

Do not redesign the region rule after inspecting a new family's held-out performance. Any family-specific rule is a new registered method arm, not evidence for the unchanged general method.

Gate

Problem-family generalization passes when at least one non-factoring family preserves the registered work-neutral/span-lower pattern. If only arithmetic miters pass, restrict the claim to arithmetic circuits.

Execution order and scale

Avoid the full cross-product:

1. G1 required: 3 architectures × 2 widths × 5 held-out seeds = 30 paired instances.
2. G2 required: 2 selected architectures × 2 widths × 5 seeds × 2 encodings, with the valid pipeline cells above.
3. G3 required: 10 held-out arithmetic-miter instances plus 10 held-out instances from one non-factoring structured family.

Complete and review each stage before launching the next. Architecture or family selection for a later stage may use calibration evidence but not held-out performance cherry-picking.

Statistical analysis

For every stage report:

• raw per-instance paired ratios;
• geometric-mean ratios and win rates;
• instance-level bootstrap 95% confidence intervals;
• frontier-budget-adjusted results where actual task counts differ;
• method × architecture, method × encoding, or method × family interactions;
• censored-run and timeout counts.

Do not pool cubes across architectures, encodings, permutations, or families as independent paper-level samples.

Deliverables

• A frozen generalization contract listing every topology, encoding, family, instance, seed, method, cutoff, and resource cell.
• Complete machine-readable result matrices for G1, G2, and G3.
• Encoding-equivalence and circuit-equivalence verification records.
• One topology table, one encoding-interaction table, and one problem-family table.
• A claim-scope report that selects exactly one supported conclusion:
  • array-ripple only;
  • arithmetic-topology generalization;
  • arithmetic plus encoding robustness;
  • structured-SAT generalization beyond arithmetic.

Verification

Provide an executable verifier that rejects:

• product/factor width confusion;
• non-equivalent circuit or CNF instances in a paired cell;
• march cubes applied across incompatible encodings;
• per-cube or held-out per-instance encoding selection;
• calibration/test overlap;
• missing failures or timeouts;
• unregistered architecture/family exclusions;
• cube-level pseudoreplication;
• aggregate claims that hide a reversing method × encoding or method × family interaction.

Dependencies

• Run a fair cross-family comparison against modern partitioning baselines #46 for complete cross-family result matrices and failure accounting
• Build the hard-regime CnC work/span table on 64–80-bit UNSAT factoring #51 for hard-regime instances, methods, and budget protocol
• Explain the CnC span reduction with a verified residual-structure audit #52 for residual-structure instrumentation and mechanism interpretation

Out of scope

• Running every architecture × encoding × family combination.
• Claiming universal SAT generalization from arithmetic-only evidence.
• Adaptive per-cube encoding selection.
• Adding a new family solely because the existing held-out families were unfavorable.