The most important result in CQ-SAT/GCC v0.5.0 is two lines long:
0,0,10
1,1,01They describe a tiny but serious firmware regression. At frame 0, an infusion pump receives a motor request. At frame 1, its medication door opens while the motor remains active. The safety gate rejects the build, points to the first bad frame and leaves behind the input and latch states needed to replay the failure.
This is a fictional controller, not medical-device software. Yet it is the first example in the project that looks like a product team using the work rather than a researcher measuring it.
That distinction took far longer to reach than the trace suggests.
CQ-SAT/GCC began with one of computer science’s most stubborn questions: if a proposed answer can be checked quickly, must there be a quick way to find it? That is the tension behind P versus NP, and Boolean satisfiability, usually shortened to SAT, is its most famous proving ground. A SAT solver receives variables and logical constraints, then asks whether any assignment of true and false values satisfies them all.
I started with a more tactile question. If the solution is somehow contained in the problem, could there be a shortcut hiding in its structure?
Looking for the shape of a shortcut
The early exploration ranged widely. I tried helper variables, feedback loops, geometric layouts, layered Flower of Life patterns, quaternion structure, musical phrasing, biological sensing, tree communication, osmosis and even the idea of expanding a space to make a route through it shorter.
Some of those ideas sound eccentric when listed together. They served a useful purpose: each forced the same technical question into a different form. Can a large collection of Boolean choices be replaced by a smaller summary without losing whether a solution exists, and can that summary still recover the full solution afterwards?
The second condition is the difficult one. Compression is easy if it is allowed to forget. Exact compression must retain every distinction that could affect the answer later.
The implementation settled on residual formulae. Choose variables in a fixed order. After each true or false decision, simplify the remaining conjunctive normal form, or CNF. If two different decision prefixes leave exactly the same canonical residual CNF, then every future choice affects them identically. They may be merged safely.
choice prefix A -> canonical residual R
choice prefix B -> canonical residual R
|
+-> one shared continuationThis quotient is not a guess. Prefixes merge only when their remaining formulae are exactly identical. One representative path is retained so that a satisfying terminal state can reconstruct a complete assignment.
That was the first durable invariant: reduce repeated future work, but never merge two states merely because they look similar.
The width kept coming back
The obstacle was not a lack of imaginative transformations. It was width.
At a variable boundary, the solver may need to distinguish many residual formulae. For structured problems that vocabulary can stay small. For arbitrary SAT instances it can grow explosively. Adding helper variables sometimes made the graph look friendlier while moving the same information elsewhere. Checkpoint encodings could preserve semantics yet cost more than the work they replaced. A generated summary might be compact for one formula and fail to generalise to the next.
The repository preserves these negative results deliberately. Automatic selector policies did not generalise out of sample. A BDD-to-CNF checkpoint remained exact but was slower than the full CDCL control. A structurally hashed AIG checkpoint expanded the measured prefix rather than compacting it. Lazy observation cones removed many nodes, but not enough reconciliation cost to produce a stable speed-up.
One result was especially clarifying. Reusable global checkpoint clauses beat full CDCL on only 6 of 18 asymmetric cross-family rows, and only five rows amortised within 50 queries. It would have been easy to promote the six wins and hide the twelve losses. Doing so would have produced a brittle solver and a better headline.
Instead, the misses became the product design.
The breakthrough was a boundary
The real breakthrough was not a universal shortcut. It was discovering a regime where exact reuse was valuable, then learning how to refuse everything else cheaply.
Repeated temporal systems supplied that regime. A hardware controller or protocol often applies the same transition relation at every time step. If the one-step relation is deterministic and narrow enough, CQ-SAT/GCC can recognise it, recover local transition functions and reuse repeated symbolic work across a long horizon. Global Checkpoint Clauses, the GCC part of the name, compile exact constraints describing which checkpoint states are reachable and install them once for many later queries.
The released portfolio gate makes the decision without trial-solving candidates. It reads static properties such as transition density, dependency fan-out, state width, query-batch size and assumption density. Dense transitions up to width nine and narrow hub-like structures up to width seven are eligible only when the declared query batch is large enough to amortise compilation. Unknown, wider or unfavourable workloads go to persistent CDCL.
CDCL, or conflict-driven clause learning, is the established general SAT technique used here through Varisat. In this project it is not the embarrassing slow path. It is the exact safety net.
That changes what the portfolio promises. It does not claim to beat CDCL everywhere. It claims that the specialist runs only inside its validated structural boundary, while the fallback preserves correctness everywhere the supported input format permits.
Calibration was another important boundary. A tempting selector can benchmark several approaches on each new formula and choose the winner afterwards. That is useful in some systems, but it is not a cheap shortcut. The released gate performs no per-formula timing calibration and no candidate solve. Its decision is explainable before solving begins.
From laboratory CNF to real models
A specialist trapped inside its own generated benchmarks is still a laboratory instrument. The next step was to accept ASCII AIGER, a standard representation for circuits and sequential systems.
That external format immediately corrected an assumption. A revision-pinned four-bit counter model had dense transitions, so the first gate selected CQ-SAT/GCC. Its full-state property queries were a poor fit and ran at roughly 0.22 times the CDCL baseline. Query shape mattered as well as transition density. Assumption density was added to the static gate, and the same model now routes directly to CDCL.
Input-driven systems exposed a wider boundary. A deterministic closed model has one next state for each current state. Real protocols and controllers also receive scheduler choices, signals and sensor inputs. Version 0.4.0 added an exact Tseitin-unrolled CDCL fallback for those models. It creates explicit input, latch and AND-gate variables at each frame, encodes their relationships exactly, and asks in one aggregate query whether any declared bad output is reachable.
If the aggregate query is unsatisfiable, every input sequence within the bound is safe with respect to the supplied property. If it is satisfiable, binary search finds the shortest bad horizon and the model supplies a complete input and latch trace.
The path was validated on two independently sourced examples. A Peterson mutual-exclusion model remained safe through frame 100 for every scheduler and signal sequence. An eight-bit SPI receiver produced its shortest failure trace at frame 16. Both were routed to CDCL statically because primary inputs place them outside the specialised continuation-quotient regime.
This is where the name CQ-SAT/GCC can be misleading if read too narrowly. The useful system is the portfolio, not merely the exotic backend. Good judgement includes knowing when not to use one’s cleverest algorithm.
The infusion pump made it a product
The earlier examples established exactness, witness recovery and safe routing. They still looked like solver demonstrations. Version 0.5.0 asks a more practical question: what would a firmware engineer actually put in a pull request?
The infusion-pump safety example defines two external inputs, motor_request and door_open, plus one safety property:
The delivered motor enable must never be active while the medication door is open.
The protected controller contains a combinational door interlock. The verifier explores every input sequence through the requested bound, reports SAFE, writes a human-readable report and solver metrics, then exits with status 0.
The regressed controller removes that interlock. The same command returns status 1 and records the shortest violation:
status=UNSAFE
bad_frame=1
frame,latch_bits_low_to_high,input_bits_low_to_high
0,0,10
1,1,01The distinction between exit statuses is a small product detail with outsized value. Zero means the declared bad state was not reachable within the bound. One means the verifier worked and rejected the firmware. Two is reserved for malformed input, invalid arguments or a tool failure. CI can distinguish an unsafe build from a broken safety check.
The command also emits a GitHub Actions annotation and writes safety-report.txt plus solver-metrics.csv. A copyable workflow runs the gate when firmware changes and uploads the artefacts even when the build is rejected. The failure is not merely a red icon. It arrives with a reproduction recipe.
continuation-quotient-sat \
firmware-safety-gate firmware/controller.aag \
100 safety-artifactsThis is intentionally a small fictional model. It proves neither that a real infusion pump is safe nor that an AIGER export perfectly represents its source code, compiler, electronics or physical mechanism. A production team still owns that modelling boundary. Formal verification is exact about the model it receives, not omniscient about the world the model is meant to describe.
That limitation belongs in the feature, not in fine print added later.
What v0.5.0 actually releases
CQ-SAT/GCC v0.5.0 is a Rust 2024 research release under Apache 2.0. Its supported AIGER importer accepts the original five-field ASCII aag format, arbitrary primary inputs, declared latch initial values and multiple bad outputs within a bounded resource envelope. Binary .aig files and extended AIGER 1.9 property sections are not yet supported.
It is not a general-purpose replacement for CDCL. All 40 bundled conventional SATLIB instances were rejected by the conservative structural gate. It is not evidence that P equals NP. It does not make every one of the 18 cross-family benchmark rows faster.
What it does offer is narrower and more credible:
- exact continuation-quotient compilation for small residual state spaces;
- reusable global checkpoint clauses for admitted repeated-query workloads;
- complete witness reconstruction;
- a calibration-free structural portfolio gate;
- exact persistent-CDCL fallback;
- bounded AIGER safety verification with shortest counterexample traces; and
- a product-shaped firmware CI workflow.
The full research findings keep the successful, mixed and falsified experiments together. That record matters because the discarded ideas define the boundary of the result as clearly as the successful ones.
The shortcut was never one road
The project began by looking for a compact route through a huge tree of Boolean choices. The temptation was to believe that the right geometry, helper, feedback rule or algebraic structure might collapse the tree without consequence.
The work eventually produced a different answer. Exact shortcuts exist when future behaviour genuinely repeats. Their value depends on recognising that structure before paying to solve the problem. Outside that regime, integrity is maintained by taking the established road.
In the infusion-pump example, the specialist does not even win the route. Primary inputs send the model to CDCL. Yet the portfolio still turns an unsafe controller into a two-frame explanation before it reaches a product build. That is not a consolation prize. It is the point at which research becomes useful.
The shortest path was not one algorithm that knew everything. It was a system that knew enough to choose, enough to reconstruct its answer, and enough to admit when the shortcut did not apply.
The source, reproducibility instructions and examples are open for scrutiny. The most useful next contribution may be a new admitted workload. It may also be a counterexample that makes the boundary sharper.