John van de Wetering

We study the counting version of the Boolean satisfiability problem sSAT using the ZH-calculus, a graphical language originally introduced to reason about quantum circuits. Using this we find a natural extension of #SAT which we call #SAT_±, where variables are additionally labelled by phases, which is GapP-complete. Using graphical reasoning, we find a reduction from #SAT to #2SAT_± in the ZH-calculus. We observe that the DPLL algorithm for #2SAT can be adapted to #2SAT_± directly and hence that Wahlstrom's O^*(1.2377^n) upper bound applies to #2SAT_± as well. Combining this with our reduction from #SAT to #2SAT_± gives us novel upper bounds in terms of clauses and variables that are better than O^*(2^n) for small clause densities of fracmn < 2.25. This is to our knowledge the first non-trivial upper bound for #SAT that is independent of clause size. Our algorithm improves on Dubois' upper bound for #kSAT whenever fracmn < 1.85 and k geq 4, and the Williams' average-case analysis whenever fracmn < 1.21 and k geq 6. We also obtain an upper bound of O^*(1.1740^L) for sSAT in terms of the length of the formula, and find an improved bound on #textbf3SAT for 1.2577 < fracmn łeq frac73. Our results demonstrate that graphical reasoning can lead to new algorithmic insights, even outside the domain of quantum computing that the calculus was intended for. In addition, using the connection to counting problems, we find a new classical simulation algorithm for quantum computations that runs in O(1.38^g) where g is the number of gates.

We present a complete set of rewrite rules for multi-qudit Clifford circuits, where \emph{qudit} denotes a d-level quantum system with d an odd prime. Completeness means that any two Clifford circuits representing the same linear map can be transformed into each other using these rules. In total, there are 19 \emph{Clifford relations}, each involving at most three qudits and admitting an intuitive interpretation. Our approach leverages the isomorphism between the symplectic group $\mathrm{Sp}(2n, \mathbb{Z}_d)$ and the quotient of the Clifford group by the Pauli group. We first derive a complete set of \emph{symplectic relations} for $\mathrm{Sp}(2n, \mathbb{Z}_d)$, and then lift them to Clifford relations by incorporating Pauli corrections. To do this, we introduce a \emph{symplectic normal form} that captures the stabiliser tableau of a Clifford operator and is unique up to Pauli correction. This simplification enables a streamlined derivation of a complete set of 66 relations, which we further compress to 18 symplectic relations. Our computations in $\mathrm{Sp}(2n, \mathbb{Z}_d)$ are formalised in the Agda proof assistant, providing a machine-verified proof of correctness.

The ability to fault-tolerantly prepare cat states, also known as multi-qubit GHZ states, is an important primitive for quantum error correction. It is required for Shor-style syndrome extraction, and can also be used as a subroutine for doing fault-tolerant state preparation of CSS codewords. Existing approaches to fault-tolerant cat state preparations have been found using computationally expensive heuristics involving SAT solving, reinforcement learning or exhaustive analysis. In this paper we constructively find optimal circuits for cat states in a scalable way. In particular, we derive formal lower bounds on the number of CNOT gates required for circuits implementing n-qubit cat-states that do not spread errors of weight at most t for values t = 1, ..., 5. We do this by using fault-equivalent rewrites of ZX-diagrams to reduce it to a problem of characterising certain 3-regular simple graphs. We provide explicit constructions for circuits that match this lower bound for all n and t <= 5. Furthermore, we use SAT solvers to construct circuits for all n <= 50 and t <= 7. We additionally show how to trade CNOT count against depth, in particular allowing us to construct constant-depth fault-tolerant implementations using O(n) ancilla and O(n) CNOT gates.