CnC comparison environment: region-branching cuber + kissat conquer + baseline Makefile

[isPANN]

What

Builds the Cube-and-Conquer (CnC) comparison environment so our region-branching
cuber can be measured head-to-head against the standard cuber baselines on the
same CNF, with the same conquer solver — the fair-comparison setup the paper
reviewers asked for.

Purely additive: src/solver.rs is byte-identical to main (the core
bbsat search is untouched). New module + tooling only.

Changes

• src/cube.rs — generate_cubes: uses the region-branching rule as a CnC
  cuber. Descends the branch tree and emits the decision-literal path as a cube
  once |σ_dec|·|σ_all| > θ (the paper's cutoff). No component decomposition (a
  cube is a whole-formula partial assignment), every branch explored to a leaf;
  reuses the existing node primitives (findbest / propagation / reductions). Two
  unit tests.
• benchmarks/conquer_cubes.py — one harness that conquers a cube file
  (march_cu's a <lits> 0 iCNF, which our cuber also emits over the same
  variable numbering) with kissat and reports the per-cube difficulty
  distribution (CV / P95 / P99 = the uniformity metric) plus the cutoff-proxy vs
  realized-difficulty Spearman.
• cnc-tools/{Makefile,README.md,.gitignore} — one-command setup
  (cd cnc-tools && make) that builds cadical, kissat, and march_cu from
  upstream source and clones Proofix (the SAT 2025 proof-prefix cuber the
  reviewers named). Idempotent, self-cleaning; only the recipe is tracked, the
  built binaries are git-ignored.

Not included (by design)

• examples/gen_cubes.rs — the CLI that drives generate_cubes, kept local per
  the repo's examples/ gitignore convention.
• The γ-share search-tree instrumentation lives on a separate branch
  (gamma-share-only), out of this PR to keep the core solver untouched here.

Test

cargo test green (93 existing + 2 new cube tests); pipeline validated
end-to-end (bi / march_cu / Proofix cubes → kissat conquer) locally.