arXiv subjects

Shiguang Feng

Publications and source records attributed to Shiguang Feng.

17 recordsLinked to original sources

arXiv2026

On the completeness of transformation rules in reversible logic synthesis

Transformation rules play a central role in reversible circuit optimization, template-based rewriting, and equivalence checking, and establishing their completeness is a fundamental problem in reversible logic synthesis. In this work, we investigate the completeness of transformation rules for reversible circuits both with and without ancillary bits and garbage outputs. For reversible circuits without ancillary bits and garbage outputs, we introduce a refined and complete transformation rule set $\mathcal{RC}^{r}$, obtained by replacing one rule in the rule set $\mathcal{RC}$ proposed in the previous work (TCAD, 45, pp. 3711--3724, 2026) with a simpler and widely adopted transformation rule. Since all rules in $\mathcal{RC}^{r}$ are commonly used in reversible logic synthesis, this result reveals that practically adopted transformation rules are already sufficient to establish a complete rewriting framework. Based on this result, we further propose an extended rule set, denoted by $\mathcal{RC}^+$, and prove its completeness for reversible circuits with ancillary bits and garbage outputs. To the best of our knowledge, this work presents the first complete transformation rule set for arbitrary reversible circuits, regardless of whether ancillary bits or garbage outputs are employed. The proposed framework establishes a theoretical foundation for circuit optimization, template generation, and equivalence checking, and may facilitate the development of automated design tools for reversible and quantum circuits.

cs.ET↗

arXiv2026

Agnostic learning of qudit stabilizer states

Learning a classical description of a quantum state is a fundamental task in quantum computation. Among the most important classes of quantum states are stabilizer states, which play a central role in quantum error correction and fault-tolerant computation. To mitigate the effects of realistic noise, agnostic learning of stabilizer states has emerged as a natural and well-motivated problem. Recently, Chen \textit{et al.} [STOC'25, p. 429-438] resolved this problem for qubit systems by using a stabilizer bootstrapping framework. However, the agnostic learning of qudit stabilizer states remains largely unexplored, since the qudit setting introduces fundamental structural differences that prevent a direct generalization of existing qubit techniques. In this paper, we successfully generalize the stabilizer bootstrapping framework to qudit systems and present the first efficient quantum algorithm for agnostic learning of qudit stabilizer states. Specifically, given copies of an unknown $n$-qudit pure state $|\psi\rangle$ that has fidelity $\tau$ with some stabilizer state, our algorithm outputs a stabilizer state $|\phi\rangle$ such that $\left| \braket{\phi|\psi} \right|^2 \geq \tau - \varepsilon$ with high probability. The algorithm uses only single-copy and four-copy measurements, and its sample and time complexity scale as $(d/\tau)^{O(d^2 \log(1/\tau))} \cdot \mathrm{poly}(n, 1/\varepsilon)$, where the dimension $d$ is an odd prime. As a direct corollary, our algorithm enables efficient estimation of the magic of a quantum state, as quantified by its stabilizer fidelity. Completing the picture, we also present a streamlined algorithm for the high-fidelity regime $\tau > \cos^2(\pi/8)$, establishing a qudit analogue of the threshold-based approach in prior qubit work.

quant-ph↗

arXiv2026

Decidability and Undecidability Results for LIA-Definable Impartial Combinatorial Games

Combinatorial game theory is a branch of mathematics and theoretical computer science that studies deterministic games with perfect information and no elements of chance. The majority of combinatorial games are impartial and formalized in linear integer arithmetic, which we call LIA-definable impartial combinatorial games (ICGs). This paper studies decidability and undecidability questions for these games. We prove that deciding whether an LIA-definable ICG is terminating or cyclic is undecidable in general, while the corresponding questions become decidable for terminating LIA-definable ICGs. We also show that deciding whether an LIA formula exactly characterizes the set of winning, losing, or draw states of an LIA-definable ICG is undecidable in general and decidable for terminating LIA-definable ICGs. For state-level questions, deciding whether a state is winning or losing remains undecidable even for terminating LIA-definable ICGs, but becomes decidable for terminating finite-depth LIA-definable ICGs. Finally, deciding whether a state is draw for an LIA-definable ICG is undecidable in general and decidable for terminating LIA-definable ICGs.

cs.GT↗

arXiv2025

A complete set of transformation rules for reversible circuits

Reversible logic synthesis is a crucial component in quantum electronic design automation. While rule-based methodologies have gained prominence in reversible circuit optimization, the completeness of the transformation rule systems is a longstanding problem in this domain. In this work, we propose the first complete set of transformation rules for reversible circuits, comprising five fundamental rules: any two equivalent reversible circuits can be transformed into each other using the rules. To prove the completeness, a canonical circuit representation for reversible functions is introduced, and we show that every reversible function is computed by a unique reversible circuit in the canonical form, and any reversible circuit can be transformed into its canonical form by applying the rules.

quant-ph↗

arXiv2025

Deterministic quantum search on all Laplacian integral graphs

Searching for an unknown marked vertex on a given graph (also known as spatial search) is an extensively discussed topic in the area of quantum algorithms, with a plethora of results based on different quantum walk models and targeting various types of graphs. Most of these algorithms have a non-zero probability of failure. In recent years, there have been some efforts to design quantum spatial search algorithms with $100\%$ success probability. However, these works either only work for very special graphs or only for the case where there is only one marked vertex. In this work, we propose a different and elegant approach to quantum spatial search, obtaining deterministic quantum search algorithms that can find a marked vertex with certainty on any Laplacian integral graph with any predetermined proportion of marked vertices. Thus, this work discovers the largest class of graphs so far that allow deterministic quantum search, making it easy to design deterministic quantum search algorithms for many graphs, including the different graphs discussed in previous works, in a unified framework.

quant-ph↗

arXiv2024

Revisiting fixed-point quantum search: proof of the quasi-Chebyshev lemma

The original Grover's algorithm suffers from the souffle problem, which means that the success probability of quantum search decreases dramatically if the iteration time is too small or too large from the right time. To overcome the souffle problem, the fixed-point quantum search with an optimal number of queries was proposed [Phys. Rev. Lett. 113, 210501 (2014)], which always finds a marked state with a high probability when a lower bound of the proportion of marked states is given. The fixed-point quantum search relies on a key lemma regarding the explicit formula of recursive quasi-Chebyshev polynomials, but its proof is not given explicitly. In this work, we give a detailed proof of this lemma, thus providing a sound foundation for the correctness of the fixed-point quantum search. This lemma may be of independent interest as well, since it expands the mathematical form of the recursive relation of Chebyshev polynomials of the first kind, and it also constitutes a key component in overcoming the souffle problem of quantum walk-based search algorithms, for example, robust quantum walk search on complete bipartite graphs [Phys. Rev. A 106, 052207 (2022)]. The lemma is also central to a recently proposed quantum algorithm named quantum phase discrimination, which has become a fundamental subroutine in quantum search on graphs [arxiv: 2504.15194]. Hopefully, more applications of the lemma will be found in the future.

quant-ph↗

arXiv2023

Nearest neighbor synthesis of CNOT circuits on general quantum architectures

NISQ devices have inherent limitations in terms of connectivity and hardware noise. The synthesis of CNOT circuits considers the physical constraints and transforms quantum algorithms into low-level quantum circuits that can execute on physical chips correctly. In the current trend, quantum chip architectures without Hamiltonian paths are gradually replacing architectures with Hamiltonian paths due to their scalability and low-noise characteristics. To this end, this paper addresses the nearest neighbor synthesis of CNOT circuits in the architectures with and without Hamiltonian paths, aiming to enhance the fidelity of the circuits after execution. Firstly, a key-qubit priority mapping model for general quantum architectures is proposed. Secondly, the initial mapping is further improved by using tabu search to reduce the number of CNOT gates after circuit synthesis and enhance its fidelity. Finally, the noise-aware CNOT circuit nearest neighbor synthesis algorithm for the general architecture is proposed based on the key-qubit priority mapping model. The algorithm is demonstrated on several popular cloud quantum computing platforms and simulators, showing that it effectively optimizes the fidelity of CNOT circuits compared with mainstream methods. Moreover, the method can be extended to more general circuits, thereby improving the overall performance of quantum computing on NISQ devices.

quant-ph↗

arXiv2023

Universal approach to deterministic spatial search via alternating quantum walks

Spatial search is an important problem in quantum computation, which aims to find a marked vertex on a graph. We propose a novel approach for designing deterministic quantum search algorithms on a variety of graphs via alternating quantum walks. Our approach is universal because it does not require an instance-specific analysis for different graphs. We highlight the flexibility of our approach by proving that for Johnson graphs, rook graphs, complete-square graphs and complete bipartite graphs, our quantum algorithms can find the marked vertex with $100\%$ success probability and achieve quadratic speedups over classical algorithms. This not only gives an alternative succinct way to prove the existing results, but also leads to new interesting findings on more general graphs.

quant-ph↗

arXiv2023

The expressive power of revised Datalog on problems with closure properties

In this paper, we study the expressive power of revised Datalog on the problems that are closed under substructures. We show that revised Datalog cannot define all the problems that are in PTIME and closed under substructures. As a corollary, LFP cannot define all the extension-closed problems that are in PTIME.

cs.LO↗

arXiv2023

Capturing the polynomial hierarchy by second-order revised Krom logic

We study the expressive power and complexity of second-order revised Krom logic (SO-KROM$^{r}$). On ordered finite structures, we show that its existential fragment $Σ^1_1$-KROM$^r$ equals $Σ^1_1$-KROM, and captures NL. On all finite structures, for $k\geq 1$, we show that $Σ^1_{k}$ equals $Σ^1_{k+1}$-KROM$^r$ if $k$ is even, and $Π^1_{k}$ equals $Π^1_{k+1}$-KROM$^r$ if $k$ is odd. The result gives an alternative logic to capture the polynomial hierarchy. We also introduce an extended version of second-order Krom logic (SO-EKROM). On ordered finite structures, we prove that SO-EKROM collapses to $Π^{1}_{2}$-EKROM and equals $Π^1_1$. Both SO-EKROM and $Π^{1}_{2}$-EKROM capture co-NP on ordered finite structures.

cs.LO↗

arXiv2023

Quantum and classical query complexities for determining connectedness of matroids

Connectivity is a fundamental structural property of matroids, and has been studied algorithmically over 50 years. In 1974, Cunningham proposed a deterministic algorithm consuming $O(n^{2})$ queries to the independence oracle to determine whether a matroid is connected. Since then, no algorithm, not even a random one, has worked better. To the best of our knowledge, the classical query complexity lower bound and the quantum complexity for this problem have not been considered. Thus, in this paper we are devoted to addressing these issues, and our contributions are threefold as follows: (i) First, we prove that the randomized query complexity of determining whether a matroid is connected is $Ω(n^2)$ and thus the algorithm proposed by Cunningham is optimal in classical computing. (ii) Second, we present a quantum algorithm with $O(n^{3/2})$ queries, which exhibits provable quantum speedups over classical ones. (iii) Third, we prove that any quantum algorithm requires $Ω(n)$ queries, which indicates that quantum algorithms can achieve at most a quadratic speedup over classical ones. Therefore, we have a relatively comprehensive understanding of the potential of quantum computing in determining the connectedness of matroids.\

quant-ph↗

arXiv2022

The Complexity and Expressive Power of Second-Order Extended Logic

We study the expressive powers of SO-HORN$^{*}$, SO-HORN$^{r}$ and SO-HORN$^{*r}$ on all finite structures. We show that SO-HORN$^{r}$, SO-HORN$^{*r}$, FO(LFP) coincide with each other and SO-HORN$^{*}$ is proper sublogic of SO-HORN$^{r}$. To prove this result, we introduce the notions of DATALOG$^{*}$ program, DATALOG$^{r}$ program and their stratified versions, S-DATALOG$^{*}$ program and S-DATALOG$^{r}$ program. It is shown that, on all structures, DATALOG$^{r}$ and S-DATALOG$^{r}$ are equivalent and DATALOG$^{*}$ is a proper sublogic of DATALOG$^{r}$. SO-HORN$^{*}$ and SO-HORN$^{r}$ can be treated as the negations of DATALOG$^{*}$ and DATALOG$^{r}$, respectively. We also show that SO-EHORN$^{r}$ logic which is an extended version of SO-HORN captures co-NP on all finite structures.

cs.LO↗

arXiv2022

The Complexity of Quantum Circuit Mapping with Fixed Parameters

A quantum circuit must be preprocessed before implementing on NISQ devices due to the connectivity constraint. Quantum circuit mapping (QCM) transforms the circuit into an equivalent one that is compliant with the NISQ device's architecture constraint by adding SWAP gates. The QCM problem asks the minimal number of auxiliary SWAP gates, and is NP-complete. The complexity of QCM with fixed parameters is studied in the paper. We give an exact algorithm for QCM, and show that the algorithm runs in polynomial time if the NISQ device's architecture is fixed. If the number of qubits of the quantum circuit is fixed, we show that the QCM problem is NL-complete by a reduction from the undirected shortest path problem. Moreover, the fixed-parameter complexity of QCM is W[1]-hard when parameterized by the number of qubits of the quantum circuit. We prove the result by a reduction from the clique problem. If taking the depth of the quantum circuits and the coupling graphs as parameters, we show that the QCM problem is still NP-complete over shallow quantum circuits, and planar, bipartite and degree bounded coupling graphs.

quant-ph↗

arXiv2021

A Variation-Aware Quantum Circuit Mapping Approach Based on Multi-agent Cooperation

The quantum circuit mapping approach is an indispensable part of the software stack for the noisy intermediatescale quantum (NISQ) device. It has a significant impact on the reliability of computational tasks on NISQ devices. To improve the overall fidelity of physical circuits, we propose a quantum circuit mapping method based on multi-agent cooperation. This approach considers the Spatio-temporal variation of quantum operation quality on the NISQ device when inserting ancillary operation. It consists of two core components: the qubit placement algorithm and the qubit routing method. The qubit placement algorithm exploits the iterated local search framework to find a desirable initial mapping for the reduced symmetric form of the original circuit. The qubit routing method generates the physical circuit through multi-agent communication and collaboration. Each agent inserts the ancillary gates independently according to its environment state. The quality of the physical circuit evolves according to an information-exchanging mechanism between agents, which combines the local search and global search. To experiment on the benchmark circuits (with hundreds of quantum gates) beyond the capacity of current NISQ devices, we build a noisy simulator with gate error 10x lower than that of the latest NISQ device of IBM. The experimental results confirm the performance of our approach in improving circuit fidelity. Compared with the stateof-the-art method, our method can improve the success rate by 25.86% on average and 95.42% at maximum.

quant-ph↗

arXiv2017

Path Checking for MTL and TPTL over Data Words

Metric temporal logic (MTL) and timed propositional temporal logic (TPTL) are quantitative extensions of linear temporal logic, which are prominent and widely used in the verification of real-timed systems. It was recently shown that the path checking problem for MTL, when evaluated over finite timed words, is in the parallel complexity class NC. In this paper, we derive precise complexity results for the path-checking problem for MTL and TPTL when evaluated over infinite data words over the non-negative integers. Such words may be seen as the behaviours of one-counter machines. For this setting, we give a complete analysis of the complexity of the path-checking problem depending on the number of register variables and the encoding of constraint numbers (unary or binary). As the two main results, we prove that the path-checking problem for MTL is P-complete, whereas the path-checking problem for TPTL is PSPACE-complete. The results yield the precise complexity of model checking deterministic one-counter machines against formulae of MTL and TPTL.

cs.LO↗

arXiv2015

Satisfiability of ECTL* with tree constraints

Recently, we have shown that satisfiability for $\mathsf{ECTL}^*$ with constraints over $\mathbb{Z}$ is decidable using a new technique. This approach reduces the satisfiability problem of $\mathsf{ECTL}^*$ with constraints over some structure A (or class of structures) to the problem whether A has a certain model theoretic property that we called EHD (for "existence of homomorphisms is decidable"). Here we apply this approach to concrete domains that are tree-like and obtain several results. We show that satisfiability of $\mathsf{ECTL}^*$ with constraints is decidable over (i) semi-linear orders (i.e., tree-like structures where branches form arbitrary linear orders), (ii) ordinal trees (semi-linear orders where the branches form ordinals), and (iii) infinitely branching trees of height h for each fixed $h\in \mathbb{N}$. We prove that all these classes of structures have the property EHD. In contrast, we introduce Ehrenfeucht-Fraisse-games for $\mathsf{WMSO}+\mathsf{B}$ (weak $\mathsf{MSO}$ with the bounding quantifier) and use them to show that the infinite (order) tree does not have property EHD. As a consequence, a different approach has to be taken in order to settle the question whether satisfiability of $\mathsf{ECTL}^*$ (or even $\mathsf{LTL}$) with constraints over the infinite (order) tree is decidable.

cs.LO↗

arXiv2014

On the Expressiveness of TPTL and MTL over ω-Data Words

Metric Temporal Logic (MTL) and Timed Propositional Temporal Logic (TPTL) are prominent extensions of Linear Temporal Logic to specify properties about data languages. In this paper, we consider the class of data languages of non-monotonic data words over the natural numbers. We prove that, in this setting, TPTL is strictly more expressive than MTL. To this end, we introduce Ehrenfeucht-Fraisse (EF) games for MTL. Using EF games for MTL, we also prove that the MTL definability decision problem ("Given a TPTL-formula, is the language defined by this formula definable in MTL?") is undecidable. We also define EF games for TPTL, and we show the effect of various syntactic restrictions on the expressiveness of MTL and TPTL.

cs.LO↗