Quantum at 30,000 ft: Qubits exploit superposition (0 AND 1 simultaneously) and entanglement (correlated qubits). This session is not about building quantum hardware — it's about #SAT (model counting), a classical technique used to verify quantum circuits, applied to industrial controller verification.
#SAT vs SAT
— SAT asks "is there ANY satisfying assignment?" (#P-complete). #SAT asks "HOW MANY satisfying assignments exist?" For controller verification: count how many states satisfy a safety property. If all do, the controller is safe.
Reversible Computing
— Every operation has a unique inverse (no information loss). Reversible verification means counting preimages of a state: "how many paths lead to FAULT?" This is a #SAT problem.
Bounded Model Checking
— Instead of exhaustive exploration (state explosion at 10^6), bound search to k steps: "Can the controller reach FAULT within 10 transitions?" #SAT solves this check for 10^4–10^6 states.
INDUSTRIAL BENCHMARK GAP
Laarman's position: quantum hardware is 2030+. But #SAT for controller verification is useful TODAY. No real-world industrial #SAT benchmark exists — tools like aQa and decision diagrams are ready, but a concrete benchmark from FluidOps would be the first of its kind.
Q: How far can #SAT go for classical industrial controller verification?
→ Laarman confirmed 10^4-state systems are within reach. Suggested encoding the 6-state pump machine as a reversible system for full preimage verification. The 300 state spaces (6 states × 50 pump models) are well within #SAT solver capability.