Skip to content

Add minimal factoring Cube-and-Conquer workflow#54

Merged
isPANN merged 3 commits into
mainfrom
codex/issue-51-hard-regime
Jul 22, 2026
Merged

Add minimal factoring Cube-and-Conquer workflow#54
isPANN merged 3 commits into
mainfrom
codex/issue-51-hard-regime

Conversation

@isPANN

@isPANN isPANN commented Jul 19, 2026

Copy link
Copy Markdown
Collaborator

Summary

  • Reduce the benchmark surface to the factoring workflow: deterministic SAT/UNSAT instance generation in CircuitSAT JSON and DIMACS CNF.
  • Add direct Kissat solving and march-generated cube conquering from Python.
  • Add Rust cube export and streaming conquer modes with bounded parallel Kissat workers.
  • Terminate in-flight Kissat processes after an early SAT result and stream CNFs through stdin to avoid per-cube disk I/O.
  • Remove the superseded hard-regime calibration, matrix, HPC, verification, and reporting pipeline.

Why

The previous benchmark stack mixed several historical experiment paths. This change keeps the paper-facing factoring workflow small and makes the Rust solver responsible for structural cubing and optional online conquer, while Python remains focused on reproducible experiment orchestration and analysis.

User impact

The retained workflow can generate matching circuit/CNF factoring corpora, solve CNF directly with Kissat, generate and conquer march cubes, export all cubes from the structural Rust solver, or stream those cubes directly into a parallel Kissat pool. SAT streaming runs stop and terminate outstanding solver processes as soon as a model is found.

Validation

  • cargo test --all-targets — 109 passed.
  • PYTHONPATH=. uv run pytest — 30 passed.
  • Linux 26-bit UNSAT streaming benchmark, 72 Kissat workers, CnC threshold 1024 — UNSAT in 21.69 s; 248/248 cubes closed with zero errors.

Closes #51

@isPANN

isPANN commented Jul 19, 2026

Copy link
Copy Markdown
Collaborator Author

HPC2 debug smoke completed successfully.

  • Slurm job: 10006741
  • State / exit: COMPLETED (0:0)
  • Elapsed: 00:03:14
  • Allocation: debug, 1 task, 4 CPUs, 16 GiB; batch MaxRSS 1,314,732 KiB
  • Checks: frozen contract; 24 targeted Python tests; 3 Rust trace tests; release build; 39 deterministic prime targets; independent primality, width, and calibration/held-out split validation

No pilot or full-table job has been submitted yet.

@isPANN

isPANN commented Jul 19, 2026

Copy link
Copy Markdown
Collaborator Author

HPC2 materialization checkpoint

Slurm job 10006802 completed successfully on HPC2.

  • submission: debug, 00:30:00, 1 task × 4 CPUs, 16 GiB, no GPU
  • result: COMPLETED (0:0) in 49 s; batch peak RSS 96,692 KiB
  • build: pinned Kissat 8af8e56f174b778aef3aa45af9f739b2a5f492c2 and march_cu 705b60c6491ef2b61988b3ce6ac674be1b90571d
  • Kissat SHA-256: 07da6866c339de638458a7867f8d11a17162046878b552cadd22b265a8b5e7b1
  • march_cu SHA-256: a0236ad5634fb680fa84220ad6806e5def15bca4d9c8850f1abbc397cedec416
  • toolchain lock SHA-256: 9be804ff3e8bb99c6bbeb92e80ed1947919a4425857fe7ae7934414196e2800c
  • corpus: 39 manifest rows, 39 CircuitSAT files, 39 CNFs, 39 metadata files
  • validation: deterministic target generation, 64/32 + 72/36 + 80/40 width semantics, disjoint calibration/held-out splits, and independent SymPy/Miller–Rabin primality checks all passed

Logs remain under artifacts/cnc-hard-regime/hpc/logs/materialize_10006802.{out,err} on HPC2. This is setup evidence, not a scientific outcome run; subsequent calibration and measurement commands will be recorded through the H1 runscribe hypothesis.

@isPANN isPANN changed the title Build the hard-regime CnC work/span workflow Add minimal factoring Cube-and-Conquer workflow Jul 22, 2026
@isPANN
isPANN marked this pull request as ready for review July 22, 2026 08:40
@isPANN
isPANN merged commit 88ad71f into main Jul 22, 2026
1 check passed
@isPANN
isPANN deleted the codex/issue-51-hard-regime branch July 22, 2026 08:41
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Build the hard-regime CnC work/span table on 64–80-bit UNSAT factoring

1 participant