arXiv subjects

Yean-Ru Chen

Publications and source records attributed to Yean-Ru Chen.

4 recordsLinked to original sources

arXiv2026

Quantangle-SAT: A Quantum SAT Solver Based on Entanglement and Equivalence Checking

Satisfiability (SAT) is a central problem in computer science, and advances in SAT-solving algorithms have a far-reaching impact across many fields. Recent works have proposed quantum SAT solvers based on Grover's algorithm, a quantum search technique. However, Grover-based approaches face a key limitation: they typically require prior knowledge of the number of satisfying assignments of the target Boolean formula. This information is unavailable in most practical settings. Quantum counting can be used to estimate this quantity, but it incurs a computational overhead that is several orders of magnitude higher than Grover search. In this paper, we propose a novel quantum SAT solver based on entanglement and equivalence checking. Our method does not assume prior knowledge of the number of solutions and is computationally more efficient than quantum counting. Although the worst case time complexity is inevitably exponential, we prove that the expected time complexity of our approach is only constant time O(1) over random Boolean functions. Experimental results also support our theoretical claim.

quant-ph↗

arXiv2026

A Modular and T-Gate Efficient Architecture for Quantum Leading-Zero/One Counter

The Quantum Leading-Zero/One Counter (QLZOC) is a fundamental component in quantum arithmetic, playing a critical role in normalization, floating-point units, dynamic range scaling, and logarithmic approximations. Conventional designs primarily rely on direct Boolean-to-quantum mapping, which results in inefficient resource utilization such as irregular gate growth and width-dependent resource overhead. In this work, we propose a scalable, modular, and resource efficient architecture for QLZOC by reformulating the counting process into a sequence of systematic conditional bit-flip operations. Moreover, our design achieves functional polymorphism so that the same design can be easily toggled between zero and one detection, while ensuring seamless scalability to any bit-width without manual re-tuning. We further introduce a Parallel QLZOC (PQLZOC) variant and a Fan-Out optimized (FO-PQLZOC) design. In this work, we evaluate resource efficiency based on the classic criteria about T gates, including the number of total T gates being used (T-count) and the number of sequential T gate layers (T-depth). By exploiting the properties of all-zero/one qubit blocks and a hierarchical merge strategy, the proposed FO-PQLZOC reduces the T-depth from O(m) to O(log m), where m is the input size. Comparative analysis demonstrates that our optimized architecture achieves a 40% reduction in T-count and a 60% reduction in T-depth over state-of-the-art designs, providing a high-performance, T-gate efficient solution for general-purpose quantum arithmetic processors.

quant-ph↗

arXiv2023

A Parallel and Distributed Quantum SAT Solver Based on Entanglement and Quantum Teleportation

Boolean satisfiability (SAT) solving is a fundamental problem in computer science. Finding efficient algorithms for SAT solving has broad implications in many areas of computer science and beyond. Quantum SAT solvers have been proposed in the literature based on Grover's algorithm. Although existing quantum SAT solvers can consider all possible inputs at once, they evaluate each clause in the formula one by one sequentially, making the time complexity O(m) -- linear to the number of clauses m -- per Grover iteration. In this work, we develop a parallel quantum SAT solver, which reduces the time complexity in each iteration from linear time O(m) to constant time O(1) by utilising extra entangled qubits. To further improve the scalability of our solution in case of extremely large problems, we develop a distributed version of the proposed parallel SAT solver based on quantum teleportation such that the total qubits required are shared and distributed among a set of quantum computers (nodes), and the quantum SAT solving is accomplished collaboratively by all the nodes. We have proved the correctness of our approaches and demonstrated them in simulations.

quant-ph↗

arXiv2023

A Quantum SMT Solver for Bit-Vector Theory

Given a formula $F$ of satisfiability modulo theory (SMT), the classical SMT solver tries to (1) abstract $F$ as a Boolean formula $F_B$, (2) find a Boolean solution to $F_B$, and (3) check whether the Boolean solution is consistent with the theory. Steps~{(2)} and (3) may need to be performed back and forth until a consistent solution is found. In this work, we develop a quantum SMT solver for the bit-vector theory. With the characteristic of superposition in quantum system, our solver is able to consider all the inputs simultaneously and check their consistency between Boolean and the theory domains in one shot.

cs.LO↗