Add persistent CDCL-assisted cube generation

[isPANN]

What changed

• add a persistent CaDiCaL companion for cube generation, using only explicit cube decisions as assumptions
• support full-CDCL candidate propagation and the production hybrid mode where region/candidate work stays on native CT while committed branches use CDCL
• retain learned clauses across branches and invoke CaDiCaL's native scheduled learned-clause reduction after assumption conflicts
• submit decision-only cubes to streaming Kissat workers at the cutoff, with first-answer SAT termination and RAII worker/child cleanup
• disjointize overlapping optimizer covers before traversal so the submitted CnC frontier does not duplicate residual assignments
• separate optimizer cover evidence from the actual CnC partition in the current trace format
• consolidate cube-generation policy into a configuration object and clean up statistics, naming, tests, and documentation

Why

Region branching evaluates many propagation candidates, while the emitted cubes are ultimately solved by CDCL. Previous integration attempts either performed redundant propagation, treated native implications as artificial assumptions, or allowed solver search to blur the CnC boundary. This change keeps the architecture explicit: native structure chooses branches, the cuber-side CDCL solver performs one learned propagation per committed branch, and unrestricted solving remains in conquer workers.

The CaDiCaL assumption-propagation path performs conflict analysis outside its normal search loop, so its learned database would otherwise never run the usual reduction schedule. RustSAT and rustsat-cadical are pinned to isPANN/rustsat@24c202c, a five-file wrapper patch that removes an upstream debug print and exposes a narrow maintenance hook calling CaDiCaL's own reduction policy. No upstream solver sources are vendored in this repository.

Impact

• hybrid mode now performs one root CDCL query plus one query per committed branch
• SAT can terminate the streaming CnC run immediately without converting the cuber into a full solver
• abnormal CLI exits no longer detach worker threads or leave Kissat children running
• trace consumers use only the latest cover/partition layout; no schema-version compatibility layer is retained

Validation

• cargo test --all-targets
• PYTHONPATH=. uv run pytest -q — 42 passed
• cargo clippy --all-targets -- -A clippy::int-plus-one -A clippy::needless-range-loop -A clippy::manual-div-ceil -A clippy::manual-contains -A clippy::manual-is-multiple-of -D warnings
• cargo fmt --all -- --check
• cargo test --test cnc_cuber_trace — 12 passed after the final trace-format cleanup
• PYTHONPATH=. uv run pytest -q tests/test_cnc_trace_mechanism.py — 11 passed after the final trace-format cleanup