Freeze the 26–30-bit factoring crossover and cube-uniformity evidence

[isPANN]

Background

This issue records the first fixed-corpus factoring crossover result for the paper's main-table campaign. The corpus uses the frozen array-tseitin-v1 CNF encoding at 26, 28, and 30 factor bits, with 10 SAT and 10 UNSAT instances per scale (60 instances total). Within each scale, all instances share the same variable map and non-unit clauses; only target-product unit literals differ.

The direct baseline is single-threaded Kissat with a 3,600 s cutoff. The Cube-and-Conquer (CnC) path uses upstream-default dynamic march_cu cubing followed by an instance-serial, 72-worker Kissat multijob conquer phase. SAT stops at the first satisfying cube; UNSAT requires every cube to be refuted. End-to-end CnC wall time is cubing wall + conquer wall, so the comparison does not hide partitioning cost.

Related: #51, #52, and the cross-family campaign in #53.

Objective

Freeze and publish a reviewer-auditable evidence package for this 60-instance factoring cell, including the direct-vs-CnC crossover table, every per-instance result, and the per-cube runtime/conflict distributions needed to assess load balance and mechanism claims.

Recorded observation

Direct Kissat versus end-to-end CnC

Timeouts are displayed at the 3,600 s cutoff but are not treated as completed runs. "Paired median speedup" uses only instances completed by direct Kissat; timeout cases contribute only lower bounds.

Scale/outcome	Direct solved	Direct capped median	CnC end-to-end median	Paired median speedup	CnC faster
26-bit SAT	10/10	121.752 s	66.618 s	2.683x	7/10
26-bit UNSAT	10/10	530.894 s	80.799 s	5.911x	10/10
28-bit SAT	9/10	851.527 s	79.225 s	5.711x	10/10
28-bit UNSAT	7/10	3357.414 s	143.855 s	13.872x	10/10
30-bit SAT	4/10	3600 s	438.323 s	1.301x	9/10
30-bit UNSAT	1/10	3600 s	851.455 s	5.603x	10/10

Across all 60 instances:

• Direct Kissat completed 41 and timed out on 19.
• End-to-end CnC completed all 60 within 3,600 s.
• CnC had lower wall time on 56/60 instances.
• On the 41 jointly solved instances, the paired median wall-time speedup was 5.005x.
• For the 19 direct timeouts, the median CnC speedup lower bound was 6.131x.
• The four direct-solved cases where CnC was slower were w26-sat-02, w26-sat-03, w26-sat-08, and w30-sat-03.
• On jointly solved instances, CnC used 4.387x as much total CPU time at the median. The current observation is therefore a wall-time/resource trade rather than a total-work reduction.

Cubing and cube uniformity

march_cu generated 5,241,649 cubes across the corpus. Per-instance cubing time ranged from 2.269 s to 2160.812 s, and frontier size ranged from 1,581 to 652,797 cubes.

For UNSAT instances, all cubes were solved and the distribution is complete. CV is runtime standard deviation divided by mean; p99/p50 and max/p50 expose the long tail. Worker efficiency is sum(per-cube wall) / (72 * conquer wall).

Scale	Runtime CV median	p99/p50 median	max/p50 median	72-worker efficiency median
26-bit UNSAT	1.324	11.5x	59x	92.8%
28-bit UNSAT	2.065	12.3x	200x	95.3%
30-bit UNSAT	1.851	17.2x	230x	97.5%

The most uneven complete frontiers were:

Instance	Cubes	p50	p99	Max	CV	Efficiency
w30-unsat-03	293,905	0.062 s	1.084 s	134.1 s	6.40	97.8%
w30-unsat-00	114,435	0.061 s	2.860 s	111.5 s	5.06	97.2%
w28-unsat-06	100,307	0.055 s	0.547 s	36.7 s	4.19	81.5%
w28-unsat-04	20,381	0.102 s	1.488 s	44.2 s	4.01	66.3%
w26-unsat-00	23,241	0.051 s	0.888 s	20.0 s	3.92	94.7%

The lowest worker efficiency was w26-unsat-01: 1,950 cubes, 0.291 s p50, 20.93 s maximum, and 55.2% efficiency. Large frontiers can retain high utilization despite severe per-cube skew, while smaller frontiers expose stragglers directly.

Runtime CV and conflicts CV have Pearson correlation 0.968 across the 30 complete UNSAT frontiers. This supports an algorithmic difficulty-skew explanation rather than pure host timing noise. The mechanism candidate to scrutinize is therefore: CnC creates many usually easy cubes, dynamic multijob scheduling absorbs most of the long tail, and a small set of hard cubes controls the remaining span.

SAT uniformity is necessarily partial because first-solution stopping visited only 35%--47% of the frontier at the group median. These prefix distributions must not be reported as full-frontier uniformity.

Interface (Input → Output)

Input

• Corpus contract: benchmarks/cnc/contracts/factoring-array-tseitin-v1.json
• Canonical CNFs: benchmarks/data/factoring-array-tseitin-v1/
• Direct result records: artifacts/factoring-direct-array-tseitin-v1/results/
• Cubing records/frontiers: artifacts/factoring-march-default-v1/{results,cubes}/
• Conquer summaries and per-cube JSONL: artifacts/factoring-conquer-kissat-w72-v1/instances/

The current detached records are on 6xA800 under /home/xiweipan/Codes/boolean-inference-crossover/. Each run also has a detached runscribe record under runscribe/runs/*__{direct,cubes,conquer}-factoring-*.

Output

• A versioned machine-readable summary containing one joined row per instance.
• A CSV/Markdown table reproducing the direct-vs-CnC and uniformity values above.
• A verifier that checks record completeness, hashes, outcome semantics, timing identities, and cutoff handling.

Technical recommendations

• Aggregate by instance_id; require exactly 60 records in each stage.
• Recompute all reported statistics from raw JSON/JSONL rather than copying the numbers in this issue.
• For SAT, exclude cancelled-by-peer-sat cubes from difficulty-distribution statistics and report visited-frontier coverage.
• Preserve both conquer-only wall and end-to-end wall.
• Keep CPU-work and wall-time comparisons separate.

Verification

Provide a reviewer-facing command such as:

PYTHONPATH=. python -m benchmarks.cnc.verify_factoring_crossover \
  --contract benchmarks/cnc/contracts/factoring-array-tseitin-v1.json \
  --direct artifacts/factoring-direct-array-tseitin-v1/results \
  --cubing artifacts/factoring-march-default-v1 \
  --conquer artifacts/factoring-conquer-kissat-w72-v1 \
  --cutoff-s 3600 \
  --workers 72

It must exit 0 with a compact PASS report asserting all of the following:

• 60 contract instances, 60 direct records, 60 cubing records/frontiers, and 60 conquer summaries.
• Every CNF, frontier, Kissat, and march_cu SHA-256 matches its recorded value.
• Direct results are 41 solved / 19 timeout; CnC results are 60 solved within the end-to-end cutoff.
• SAT summaries contain exactly one SAT cube, stop further scheduling, and account for completed/cancelled/not-started cubes.
• UNSAT summaries contain one UNSAT terminal record for every frontier cube.
• end_to_end_wall_s == cubing.elapsed_s + conquer.observed_parallel_wall_s within 1 ms.
• Rounded recomputation matches 56/60 CnC wall-time wins, 5.005x paired median speedup, 4.387x median CPU-work ratio, and 0.968 runtime-CV/conflicts-CV correlation.

Negative control: copy one joined fixture to a temporary directory, change one frontier SHA-256 or delete one per-instance summary, and rerun the verifier. It must exit nonzero, print FAIL, and name the affected instance_id; an existence-only or precomputed-table check does not satisfy this issue.

Assumes

• The direct baseline was collected with 60 single-core Kissat processes running concurrently, whereas CnC instances were run serially with 72 workers. Shared-cache and memory-bandwidth contention remains a plausible direct-baseline confound. Before promoting wall-time differences to a paper finding, rerun direct Kissat under controlled per-instance or low-concurrency load.
• Each method currently has one timing sample per instance. Repeat policy and uncertainty reporting remain to be fixed for the final paper table.

Out of scope

• Changing array-tseitin-v1 or regenerating the frozen corpus.
• Region-based CnC, alternative cubers, or other benchmark families.
• Treating SAT prefix statistics as complete-frontier uniformity.