Abstract Quantum circuit optimizers use rewrite rules from circuit equivalences, yet prior work has identified thousands of such identities, creating substantial challenges for their storage, management, and effective application. For many widely used unitary gate sets, including Clifford+T, this apparent complexity is largely redundant, raising a fundamental question: How many quantum circuit identities are actually needed to generate all others? In this work, we provide strong evidence that a small pruned set of identities suffices to generate all circuit equivalences of bounded depth. Surprisingly, for circuits on up to nine qubits in which each side of an equality has depth at most ten, fewer than twenty identities are sufficient to derive all others, and for circuits on up to five qubits with depth at most ten, only 17 rules–each involving at most three qubits–are enough. These results enable significantly more compact and efficient rewriting systems for quantum compiler optimization and reveal underlying algebraic structure in common gate sets, showing that the vast majority of known circuit identities are consequences of a small foundational basis.

Program synthesis aims at the automatic generation of programs based on given specifications. Despite significant progress, the inherent complexity of synthesis tasks and the interplay among intention, invention and adaptation limit its scope. A promising yet challenging avenue is the integration of concurrency to enhance synthesis algorithms. While some efforts have applied basic concurrency by parallelizing search spaces, more intricate synthesis scenarios involving interdependent subproblems remain unexplored. In this paper, we focus on string transformation as the target domain and introduce the first concurrent synthesis algorithm that enables asynchronous coordination between deductive and enumerative processes, featuring an asynchronous deducer for dynamic task decomposition, a versatile enumerator for resolving enumeration requests, and an accumulative case splitter for if-then-else condition/branch search and assembling. Our implementation, Synthphonia exhibits substantial performance improvements over state-of-the-art synthesizers, successfully solving 116 challenging string transformation tasks for the first time.

Syntax-guided synthesis has been a prevalent theme in various computer-aided programming systems. However, the domain of bit-vector synthesis poses several unique challenges that have not yet been sufficiently addressed and resolved. In this paper, we propose a novel synthesis approach that incorporates a distinct enumeration strategy based on various factors. Technically, this approach weighs in subexpression recurrence by term-graph-based enumeration, avoids useless candidates by example-guided filtration, prioritizes valuable components identified by large language models. This approach also incorporates a bottom-up deduction step to enhance the enumeration algorithm by considering subproblems that contribute to the deductive resolution. We implement all the enhanced enumeration techniques in our S y G u S solver D ryad S ynth , which outperforms state-of-the-art solvers in terms of the number of solved problems, execution time, and solution size. Notably, D ryad S ynth successfully solved 31 synthesis problems for the first time, including 5 renowned Hacker’s Delight problems.