CQ-SAT/GCC v0.24.0
CQ-SAT/GCC v0.24.0 adds an exact closest-method experiment for causal counterexample analysis.
The release compares ordered deletion and QuickXplain over the same temporal waveform-intervention vocabulary. Every fresh-CDCL discovery and validation query is recorded and replayed through persistent CDCL and, when statically admitted, a continuation quotient. Publication fails on disagreement, overwrite, or invalid minimality evidence.
The result is deliberately mixed:
- QuickXplain reduces discovery queries on the sparse 2-of-16 control.
- Deletion wins on the dense control, infusion-pump example, and SPI fixture.
- Persistent CDCL beats rebuilding a fresh solver on all eight rows.
- CQ accelerates query replay when admitted but does not amortise preparation on this cohort.
This negative result is part of the release: v0.24.0 does not claim a new minimisation algorithm or a production performance advantage. Deletion, QuickXplain, incremental SAT, causal counterexample explanation, and compiled Boolean explanations are established work. The maximal-constant waveform vocabulary, identical cross-backend transcript replay, and digest-bound evidence integration remain potentially distinctive but scholarly novelty is unproven.
Validation includes exhaustive monotone-oracle checks through four choices, deterministic regeneration of eight result rows, Rust 1.97 Linux and macOS tests, public RTL differential checks, production-evaluation smoke tests, and a clean RustSec audit.
CQ-SAT/GCC remains an evaluation-ready research prototype. Independent security review, technical review, and design-partner RTL evidence are still required before any production-grade claim.