IEEE International Symposium on Multiple-Valued Logic (ISMVL)

Quantum Algorithm for Maximum Satisfiability

Abdirahman Alasow, Marek A. Perkowski

Published May 1, 2022• 7 citations

Abstract

Satisfiability (SAT) problem in engineering and computer science is to find the set of assignment values of input variables for the given Boolean function that evaluate this function to TRUE or prove that such satisfying values do not exist. For POS SAT Problem, we propose a novel quantum algorithm for the maximum satisfiability (MAX-SAT) which returns the maximum number of OR terms that are satisfied for the SAT-unsatisfiable function, providing us with the information how far the given Boolean function is from the SAT satisfaction. We use Grover's algorithm with a new block called quantum counter in the oracle circuit.

DOI: 10.1109/ismvl52857.2022.00012

Related papers

Quantum Algorithm for Variant Maximum Satisfiability

Abdirahman Alasow, Peter Jin, Marek A. Perkowski

In this paper, we proposed a novel quantum algorithm for the maximum satisfiability problem. Satisfiability (SAT) is to find the set of assignment values of input variables for the given Boolean function that evaluates this function as TRUE or prove that such satisfying values do not exist. For a POS SAT problem, we proposed a novel quantum algorithm for the maximum satisfiability (MAX-SAT), which returns the maximum number of OR terms that are satisfied for the SAT-unsatisfiable function, providing us with information on how far the given Boolean function is from the SAT satisfaction. We used Grover’s algorithm with a new block called quantum counter in the oracle circuit. The proposed circuit can be adapted for various forms of satisfiability expressions and several satisfiability-like problems. Using the quantum counter and mirrors for SAT terms reduces the need for ancilla qubits and realizes a large Toffoli gate that is then not needed. Our circuit reduces the number of ancilla qubits for the terms T of the Boolean function from T of ancilla qubits to ≈log2T+1. We analyzed and compared the quantum cost of the traditional oracle design with our design which gives a low quantum cost.

EntropyNov 5, 20223 citations

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

Shang-Wei Lin, Ji-Qing Yan, Yean-Ru Chen +2 more

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-pharXiv:2604.18218Apr 21, 20260 citations

Quantum Computing Approach for Solving Exactly-1 3-SAT Using Grover's Algorithm

E. Afreen Banu, Amol Atmaram Dhumal, Lukesh Kadu +3 more

This study investigates the application of quantum computing to the Boolean satisfaction problem (SAT), with a special focus on the special case of the Exactly-1 3-SAT problem. Quantum computing has shown significant advantages in solving various computational problems and achieving exponential accelerations. This study designs and implements a quantum algorithm to identify assignments that prove Boolean formulas of bound form using the Grover search algorithm. We tested the implementation of three quantum circuits using as many quantum techniques as possible using the IBM quantum simulator. Only the second implementation showed consistent results due to the number of qubits, decoherence time, and circuit complexity. This study demonstrates that the design of algorithms meets hardware constraints and lays the foundation for future research as quantum devices improve.

International Conference for Advancement in Technology (ICONAT)Sep 19, 20250 citations

Quantum Algorithm for Solving Tautology and Satisfiability Problems

Amrita Mitra

This paper proposes a quantum algorithm for solving the tautology and the satisfiability problems for a Boolean formula. Let’s say we are given a Boolean formula. The variables of the Boolean formula can take only two values—TRUE or FALSE. The tautology problem asks whether the Boolean formula always evaluates to TRUE for all values of its Boolean variables. The satisfiability problem asks whether the Boolean formula can evaluate to TRUE for at least one set of values of its Boolean variables. This paper proposes that both problems can be solved using the proposed quantum algorithm. The tautology problem is known to be co-NP-complete. The satisfiability problem is known to be NP-complete.

Journal of Quantum Information ScienceJan 1, 20260 citations

Procedure of Solving 3-SAT Problem by Combining Quantum Search Algorithm and DPLL Algorithm

Runkai Zhang, Jing Chen, Huiling Zhao

Although some classical algorithms have been applied to solve the satisfiability problem, more effective methods are still explored because existing algorithms are constrained by inadequate computing capability of traditional computers. The parallelism of quantum computation makes quantum algorithms with promising potential to improve the computing ability, but existing quantum algorithms still require too large number of qubits to solve a simple problem effectively. In this paper, an optimized data structure was structured to solve Boolean satisfiability problem by utilizing Grover's algorithm, and then the corresponding formula was proposed to balance variables in consideration of complexity. With reasonable simplification, quantum circuits were built to decrease the number of qubits required in Grover's algorithm. The result of verification experiment further demonstrated that the proposed approach is simple, reliable and of a certain practical value.

Computing Performance and Communication systemsDec 4, 20204 citations

A benchmarking study of grover's algorithm for solving boolean sat with quantum circuits

Jirapas U. Jipipob

This study explores how well Grover's Algorithm performs in solving the Boolean Satisfiability Problem (SAT) using quantum circuits. The algorithm is implemented with IBM's Qiskit framework and compared to classical brute-force methods. Experiments focus on 3-SAT, 4-SAT, and 5-SAT problems, using quantum simulators and IBM quantum hardware. The results show that Grover's Algorithm is more efficient, offering a theoretical quadratic speedup over classical methods. However, practical issues like limited qubit availability, hardware noise, and optimization challenges impact its current performance. The data highlights the potential for quantum computing to scale and solve NP-complete problems. This research shows how quantum computing can improve problem-solving and lays the groundwork for future studies on more complex SAT problems and advanced quantum hardware.

Jan 1, 20250 citations