Remove cuber-side CDCL learning

[isPANN]

Summary

• remove the cuber-side RustSAT/CaDiCaL dependency and learned-clause propagation path
• keep cube generation on the native Compact-Table propagation engine; the flattened CNF is used only by Kissat conquer workers
• remove the obsolete propagation CLI/state, compatibility wrappers, trace fields, documentation, and CDCL-specific tests

Why

The cuber-side CDCL companion was an experimental mechanism that let a SAT solver learn clauses before conquer. It is no longer part of the intended solver design. Keeping it left two propagation systems, extra dependencies, and a broad configuration surface in the production cuber.

Impact

cnc_cuber no longer accepts --propagation or --propagate-cnf. Cube generation now has one propagation implementation and reports native-only trace provenance. The public cubing API retains the direct cutoff/configured entry points and removes compatibility-only forwarding functions.

Validation

• cargo test --all-targets
• PYTHONPATH=. uv run pytest tests/test_benchmark_pipeline.py tests/test_benchmark_scope.py tests/test_cnc_trace_mechanism.py tests/test_conquer_parallel.py tests/test_cubing.py tests/test_factoring_corpus.py tests/test_solve.py — 41 passed
• cargo fmt -- --check
• git diff --check
• cargo clippy --all-targets — completed with existing warnings in unchanged files