Skip to content

v0.27.0 — Exact Symbolic Input Projection

Choose a tag to compare

@kabudu kabudu released this 18 Jul 15:24
4e8fa29

CQ-SAT/GCC v0.27.0 adds the first exact symbolic-input projection stage for CIQ.

The compiler now propagates input-support masks through AIG transition and property cones, allowing firmware and robotics models to declare up to 64 inputs when no more than eight affect the combined interface. Proven-irrelevant causal observations are removed without training or timing calibration. Recovered projected traces are lifted into complete input vectors and checked by re-evaluating the original AIG.

On a 16-input mobile-robot obstacle-stop regression projected exactly to two inputs, ten trials per horizon produced median end-to-end speedups of 2.46x, 4.00x, 6.76x, and 10.74x at horizons 8, 16, 32, and 64. All 1,240 target rows were independently replayed with fresh CDCL and every full-input witness validated.

The boundary remains explicit: this result applies to wide declared buses with narrow semantic support. Genuinely dense wide-input predicate projection remains open.

Full details: https://github.com/kabudu/continuation-quotient-sat/blob/v0.27.0/docs/SYMBOLIC_INPUT_PROJECTION.md