Freeze the 26–30-bit factoring CnC result with a matched-frontier control

[isPANN]

Background

This issue freezes the complete factoring result for the paper's 26–30-bit Cube-and-Conquer (CnC) study. CnC first partitions a SAT instance into cubes (partial assignments), then solves those cubes with Kissat. The structure-aware cuber reads the original multiplication circuit and branches by circuit region; march_cu reads the expanded CNF and uses generic look-ahead search.

The original version of this issue compared structure-aware CnC only with upstream-default march_cu. That is a valid system comparison, but default march emits 35–219 times as many cubes, so it cannot isolate whether the gain comes from structural cube quality or simply avoiding over-partitioning. This revision adds the completed matched-frontier march control, calibrated without observing the main-table instances.

Related baseline record: #55.

Objective

Publish one reviewer-auditable record containing:

1. the direct Kissat and upstream-default march system baselines;
2. the frozen structure-aware result;
3. a held-out-calibrated march control with approximately the same frontier scale;
4. SAT/UNSAT and cubing/conquer decompositions;
5. the uncensored UNSAT balance/work evidence needed for the mechanism claim;
6. explicit limitations and a verifier with a negative control.

Frozen protocol

• Corpus: factoring-w{26,28,30}-{sat,unsat}-00..09, giving 10 SAT and 10 UNSAT instances per width and 60 instances total.
• Encoding: one frozen array-tseitin-v1 CNF contract. Every method sees the same canonical SAT formula; the structural cuber additionally consumes the corresponding original circuit.
• Region policy: difficulty cutoff 1,024, frozen on a disjoint calibration corpus before the 60 main instances were observed.
• Default march: upstream dynamic march_cu, with no static stopping override.
• Matched march: one static march_cu -n value per width, selected on 18 held-out calibration instances by minimizing paired RMS log2 cube-count error against region-1,024. No main-table instance was used for tuning, and no final frontier used -l truncation.
• Conquer: one instance at a time, 72 Kissat workers, identical input-order multijob scheduler.
• SAT: stop at the first satisfying cube. UNSAT: drain every cube.
• End-to-end wall: cubing wall plus observed conquer wall for the same instance. Batch makespan is never used.
• Direct Kissat: one core, 3,600-second timeout. Timed-out values are right-censored lower bounds.
• Tool hashes: march_cu a0236ad5634fb680fa84220ad6806e5def15bca4d9c8850f1abbc397cedec416; Kissat 07da6866c339de638458a7867f8d11a17162046878b552cadd22b265a8b5e7b1.

Result 1: primary system comparison

This table compares the methods as they would normally be run. Geometric means (GM) are paired by instance ID. Direct rows containing timeouts use the 3,600-second cap only to state a lower bound.

Width	Direct capped GM	Direct timeouts	Default march GM	Region-1,024 GM	Default march / region	Region wins vs march	Direct / region
26	254.075 s	0/20	65.260 s	12.264 s	5.321x	19/20	20.717x
28	≥1,255.854 s	4/20	123.446 s	36.033 s	3.426x	19/20	≥34.852x
30	≥2,669.726 s	15/20	561.985 s	89.636 s	6.270x	19/20	≥29.784x

Region-1,024 was faster than default march on 57/60 instances and provably faster than direct Kissat on all 60. The default-march result is nevertheless strongly confounded by frontier scale:

Width	Default march cubes GM	Region cubes GM	Frontier reduction	Default march cubing	Region cubing
26	19,457	563	34.6x	33.021 s	2.542 s
28	25,122	469	53.5x	48.182 s	2.104 s
30	121,961	556	219.5x	311.739 s	2.815 s

Result 2: held-out matched-frontier control

Calibration

march_cu -n stops when the formula has the requested number of remaining variables. One value was frozen per width from six held-out calibration instances (three SAT/UNSAT pairs), then applied unchanged to all 20 main instances at that width.

Width	DIMACS variables	Frozen -n	Held-out march/region cube GM	Main march/region cube GM	Main per-instance range
26	4,108	3,084	1.068x	0.986x	0.290–4.291x
28	4,760	3,688	1.015x	0.940x	0.049–6.149x
30	5,460	4,272	0.986x	1.153x	0.317–4.591x

This is a matched-scale, not per-instance exact-match, control. Per-instance retuning would leak evaluation data and give march a tuning privilege that region does not receive.

End-to-end crossover

Region/matched above one favors matched march; below one favors region.

Width	Outcome	Matched march GM	Region-1,024 GM	Region/matched	Matched wins
26	all	10.366 s	12.264 s	1.183x	13/20
26	SAT	4.530 s	6.361 s	1.404x	7/10
26	UNSAT	23.722 s	23.646 s	0.997x	6/10
28	all	34.424 s	36.033 s	1.047x	9/20
28	SAT	15.055 s	18.712 s	1.243x	7/10
28	UNSAT	78.712 s	69.391 s	0.882x	2/10
30	all	99.878 s	89.636 s	0.898x	7/20
30	SAT	37.906 s	37.746 s	0.996x	5/10
30	UNSAT	263.168 s	212.857 s	0.809x	2/10

The aggregate crossover is therefore:

• 26-bit: matched march is 1.183x faster;
• 28-bit: matched march is 1.047x faster, effectively close;
• 30-bit: region is 1.114x faster;
• full-drain UNSAT: region is tied at 26 bits, 1.134x faster at 28 bits, and 1.236x faster at 30 bits;
• first-solution SAT: march leads at 26/28 bits and the methods tie at 30 bits. SAT has high variance because solution placement and scheduling order affect when the first satisfying cube appears.

Stage decomposition

Width	Matched cubes GM	Region cubes GM	Matched cubing	Region cubing	Matched conquer	Region conquer	Region conquer speedup
26	555	563	0.541 s	2.542 s	9.264 s	8.218 s	1.127x
28	441	469	0.502 s	2.104 s	33.579 s	32.298 s	1.040x
30	641	556	0.834 s	2.815 s	97.483 s	82.908 s	1.176x

Matched march always cubes faster. Region's more expensive B&B-like structural reasoning is recovered in conquer as width grows: its conquer advantage reaches 17.6% at 30 bits and produces the 30-bit end-to-end win.

Matched march is still 6.295x, 3.586x, and 5.627x faster than upstream-default march at 26/28/30 bits. This shows that default march loses much of its time through over-partitioning; it does not remove the 30-bit region advantage at comparable frontier scale.

Result 3: uncensored UNSAT mechanism evidence

Only UNSAT gives a complete cube distribution because every cube is solved. Every entry below is the geometric mean over the ten UNSAT instances at that width. Runtime CV is standard deviation divided by mean; the utilization proxy is total per-cube solver wall divided by 72 × observed conquer wall.

Width	Cubes, march/region	Runtime CV, march/region	p95, march/region	Max, march/region	Solver work, march/region	Utilization, march/region	Region end-to-end speedup
26	598 / 627	1.157 / 0.819	5.562 / 4.510 s	17.296 / 13.869 s	1,085 / 1,199 solver-s	65.2% / 81.1%	1.003x
28	426 / 585	1.143 / 0.953	18.255 / 12.919 s	62.944 / 54.640 s	2,743 / 3,454 solver-s	48.7% / 72.9%	1.134x
30	618 / 622	1.513 / 1.003	52.258 / 36.631 s	218.475 / 169.951 s	9,141 / 10,165 solver-s	48.4% / 67.4%	1.236x

This matched-scale table is the mechanism result that the default-march comparison could not provide:

• region has lower normalized dispersion, shorter absolute p95 and maximum tails, and higher 72-worker utilization at every width;
• matched march actually uses less aggregate solver work (about 9%, 21%, and 10% less), so region's 28/30-bit wall-time advantage is not explained by doing less CDCL work;
• at 30-bit UNSAT the cube counts are essentially identical (618 versus 622 GM), yet region is 1.236x faster end to end and 1.252x faster in conquer.

The observation is consistent with the structural cuber spending more time up front to produce a frontier that schedules more evenly. It does not prove that uniformity is the only cause.

Result 4: 30-bit cutoff sensitivity

Cutoff 4,096 was retained as a sensitivity row, not selected post hoc. The ratio is paired time(1,024) / time(4,096); intervals crossing one do not resolve a winner.

Outcome	n	GM at 1,024	GM at 4,096	Paired ratio	Bootstrap 95% interval	Wins, 1,024–4,096
all	20	89.636 s	86.951 s	1.031x	0.906–1.163	9–11
SAT	10	37.746 s	39.125 s	0.965x	0.787–1.174	6–4
UNSAT	10	212.857 s	193.237 s	1.102x	0.961–1.266	3–7

The sensitivity experiment does not justify replacing the preregistered 1,024 primary row.

Integrity audit

• 60/60 direct records, 60/60 default-march frontiers and conquer records, 60/60 region-1,024 cells, 20/20 retained region-4,096 sensitivity cells, and 60/60 matched-march frontiers and conquer records are present.
• All matched-frontier calls returned complete partitions without -l; none timed out or solved the instance during cubing.
• All 60 matched conquer results have the expected SAT/UNSAT outcome, 72 workers, zero solver errors, and zero cube timeouts.
• All SAT cells contain one satisfying cube and stop further scheduling. All UNSAT cells have completed == terminal_records == cubes, with zero cancelled and zero not-started cubes.
• Every audited canonical-CNF, frontier, Kissat, and march SHA-256 agrees with its source record.
• End-to-end times equal cubing elapsed plus observed conquer wall.

Claim supported by the complete evidence

Upstream-default generic look-ahead cubing severely over-partitions these factoring instances. After controlling frontier scale with a held-out, width-frozen march policy, structure-aware cubing exhibits a size-dependent tradeoff: it pays a larger cubing cost but produces more balanced full-drain frontiers, reaching parity around 28 bits and lower end-to-end wall time at 30 bits under 72-way conquer.

The evidence does not support claiming that region wins at every width, that SAT prefix distributions describe complete frontiers, that 4,096 is the best cutoff, or that uniformity alone causes the result.

Interface (Input → Output)

Input artifacts

• Contract: benchmarks/cnc/contracts/factoring-array-tseitin-v1.json
• Direct: artifacts/factoring-direct-array-tseitin-v1/results/
• Default march cubes: artifacts/factoring-march-default-v1/
• Default march conquer: artifacts/factoring-conquer-kissat-w72-v1/
• Region 26/28 cubes: artifacts/factoring-region-main-t1024-w26-w28-cubes-v1/
• Region 26/28 conquer: artifacts/factoring-region-main-t1024-w26-w28-full-v1/
• Region 30 cubes: artifacts/factoring-region-main-w30-cutoff-sensitivity-cubes-v1/
• Region 30 conquer: artifacts/factoring-region-main-w30-cutoff-sensitivity-full-v1/
• Matched-march calibration: artifacts/factoring-march-matched-region1024-calibration-v1/
• Matched-march cubes: artifacts/factoring-march-matched-region1024-main-cubes-v1/
• Matched-march conquer: artifacts/factoring-march-matched-region1024-main-conquer-v1/

The detached artifact root is /home/xiweipan/Codes/boolean-inference-crossover/ on 6xA800.

Required output

• one versioned joined machine-readable table keyed by the 60 instance IDs;
• Markdown/CSV tables reproducing all rounded values above;
• one reviewer-facing verifier covering completeness, provenance, stopping semantics, censoring, timing identities, and aggregates.

Verification

Provide a single reviewer-facing command:

PYTHONPATH=. python -m benchmarks.cnc.verify_region_main_factoring \
  --contract benchmarks/cnc/contracts/factoring-array-tseitin-v1.json \
  --direct artifacts/factoring-direct-array-tseitin-v1/results \
  --default-march-cubes artifacts/factoring-march-default-v1 \
  --default-march-full artifacts/factoring-conquer-kissat-w72-v1 \
  --region-26-28-cubes artifacts/factoring-region-main-t1024-w26-w28-cubes-v1 \
  --region-26-28-full artifacts/factoring-region-main-t1024-w26-w28-full-v1 \
  --region-30-cubes artifacts/factoring-region-main-w30-cutoff-sensitivity-cubes-v1 \
  --region-30-full artifacts/factoring-region-main-w30-cutoff-sensitivity-full-v1 \
  --matched-calibration artifacts/factoring-march-matched-region1024-calibration-v1 \
  --matched-cubes artifacts/factoring-march-matched-region1024-main-cubes-v1 \
  --matched-full artifacts/factoring-march-matched-region1024-main-conquer-v1 \
  --workers 72 --direct-timeout-s 3600

It must exit 0 and print PASS while independently recomputing, rather than trusting stored aggregate tables:

• exact artifact counts and unique IDs listed in the integrity audit;
• frozen matched-march settings 26=3084, 28=3688, 30=4272, with no final cube limit;
• input/tool/frontier hashes and SAT/UNSAT stopping semantics;
• default-march/region speedups 5.321x, 3.426x, 6.270x;
• matched-march/region end-to-end values 10.366/12.264, 34.424/36.033, and 99.878/89.636 seconds;
• full-drain UNSAT region speedups 1.003x, 1.134x, and 1.236x;
• 30-bit UNSAT cube-count GM 618/622, runtime-CV GM 1.513/1.003, and utilization 48.4%/67.4% for matched march/region;
• direct timeout counts 0/4/15 and correct right-censoring labels;
• 30-bit cutoff-sensitivity ratio 1.031x with both rows retained.

Negative control: copy one instance bundle into a temporary fixture and perform one of these corruptions: change its frontier SHA-256, delete one UNSAT terminal record, change the frozen -n, or mark a first-SAT prefix as a complete distribution. The verifier must exit nonzero, print FAIL, and name both the affected instance_id and violated invariant. A file-existence check or comparison against trusted precomputed aggregates does not satisfy this issue.

Limitations / follow-up

• Methods ran on the same server but in different epochs and were not replicated or interleaved; close timing differences can still contain shared-server noise.
• The matched policy controls width-level frontier scale, not every instance's exact cube count. The verifier must report residual paired count ratios beside timing ratios.
• A paired count-adjusted analysis of the saved UNSAT records should test whether the 30-bit advantage remains after residual mismatch.
• A frozen larger-width validation panel is needed before claiming a general asymptotic crossover.
• Generalization to other structured families belongs to Evaluate CnC generalization across circuit topologies, CNF encodings, and structured SAT families #53.