Add minimal factoring Cube-and-Conquer workflow

.gitignore

@@ -13,6 +13,7 @@
 # Local research and experiment state.
 /.knowledge/
 /experiments/
+/artifacts/
 
 # Python caches.
 __pycache__/

benchmarks/cnc/README.md

@@ -1,44 +1,76 @@
-# Auditable Cube-and-Conquer measurements
+# Factoring Cube-and-Conquer
 
-## Current CnC comparison
+This directory contains only the operations needed for factoring runs:
 
-The primary comparison uses online stopping rules on both sides:
+1. generate paired SAT/UNSAT `n×n` factoring instances in CircuitSAT and CNF;
+2. solve a CNF directly with Kissat;
+3. cube a CNF with `march_cu`, then solve the cubes in parallel with Kissat;
+4. use the Rust solver either to export a complete frontier or to stream cubes
+   directly into a bounded parallel Kissat pool;
+5. solve a frozen frontier in Python for reproducible paper measurements.
 
-- Region cubing reads structured CircuitSAT and stops at classical CC
-  difficulty `D^2(D+I)/N > threshold`. Calibrate the threshold by frontier
-  count only with `calibrate_cc_difficulty.py`.
-- `march_cu` reads a globally encoded CNF and uses its upstream default dynamic
-  cutoff unchanged. Do not pass `-d`, `-n`, `-e`, or `-f` in the primary arm.
-- Both frontiers are conquered by the same solver and resource policy. Report
-  preprocessing, cubing, and conquer work/span separately and end to end.
+## Generate instances
 
-Machine-specific Slurm wrappers are intentionally not versioned. Build the
-frontiers with `cnc_cuber`, `calibrate_cc_difficulty.py`, and upstream
-`march_cu`, then run both arms through `conquer_parallel.py`. Rejected
-static/product cutoff workflows are not maintained.
+```sh
+PYTHONPATH=. python3 -m benchmarks.cnc.factoring \
+  --width 26 --width 28 --count 10 \
+  --out-dir artifacts/factoring
+```
+
+Each manifest row points to `instance.circuitsat.json` and `instance.cnf` with
+matching SAT/UNSAT metadata and hashes.
+
+## Direct Kissat
+
+```sh
+PYTHONPATH=. python3 -m benchmarks.cnc.solve INSTANCE.cnf \
+  --kissat cnc-tools/bin/kissat \
+  --timeout-s 600 --out-dir artifacts/direct
+```
+
+## march_cu then parallel Kissat
+
+```sh
+PYTHONPATH=. python3 -m benchmarks.cnc.cubing march INSTANCE.cnf \
+  --march-cu cnc-tools/bin/march_cu \
+  --kissat cnc-tools/bin/kissat --workers 32 \
+  --out-dir artifacts/march
+```
+
+Pass `--remaining-vars N` to override `march_cu`'s dynamic cutoff.
 
-Each measurement bundle is a directory containing a hash-linked `bundle.json`,
-the input DIMACS file, a frontier JSONL, a monotonic event JSONL, per-cube raw
-result JSONL, and a SAT witness when applicable. The verifier treats those raw
-records as authoritative and independently reconstructs:
+## Rust solver: export all cubes
+
+```sh
+cargo build --release --bin cnc_cuber
+target/release/cnc_cuber INSTANCE.circuitsat.json \
+  --cc-threshold 65536 -o artifacts/project/frontier.icnf
+```
 
-- complete, non-overlapping frontier coverage;
-- every cube's solved, cancelled, timed-out, or never-started lifecycle;
-- cubing wall/CPU time, conquer CPU work and scheduled makespan;
-- orchestration and end-to-end wall time;
-- maximum worker concurrency and the aggregate verdict;
-- input, tool, and executable provenance plus SAT witness validity.
+This mode finishes the whole cubing traversal and never starts Kissat.
+
+## Rust solver: streaming Cube-and-Conquer
+
+```sh
+target/release/cnc_cuber INSTANCE.circuitsat.json \
+  --cc-threshold 65536 \
+  --solve-cnf INSTANCE.cnf \
+  --kissat cnc-tools/bin/kissat --workers 32
+```
 
-Run the positive fixture and the generated negative controls from the
-repository root:
+The Rust cuber submits each open leaf immediately to a bounded worker pool.
+Exit codes follow SAT conventions: `10` for SAT and `20` for UNSAT.
 
-```bash
-python3 benchmarks/cnc/verify_measurements.py \
-  --bundle tests/fixtures/cnc/measurement-valid
+## Analyze a frozen frontier
 
-python3 -m unittest tests/test_cnc_measurements.py
+```sh
+PYTHONPATH=. python3 -m benchmarks.cnc.cubing frontier \
+  INSTANCE.cnf artifacts/project/frontier.icnf \
+  --kissat cnc-tools/bin/kissat --workers 32 \
+  --out-dir artifacts/project-analysis
 ```
 
-The exhaustive frontier representation is intended for small audit fixtures.
-Large production runs should add a branching-tree certificate before using
-this format beyond a tractable number of frontier variables.
+The Python path never invokes the project cuber. It consumes a complete,
+frozen frontier and records per-cube timing, decisions, conflicts, and aggregate
+statistics. March and project frontiers can therefore use the same analysis
+backend.