© 2026 Aqora Quantum S.A.S.

Terms Privacy Legal Notice

arXiv:2408.03757 · New Journal of Physics

Efficient digital quadratic unconstrained binary optimization solvers for SAT problems

Robert Simon Fong, Yanming Song, Alexander Yosifov

Published Jan 1, 2025• 1 citation

Abstract

Abstract Boolean satisfiability (SAT) is a propositional logic problem of determining whether an assignment of variables satisfies a Boolean formula. Many combinatorial optimization problems can be formulated in Boolean SAT logic—either as k-SAT decision problems or Max k-SAT optimization problems, with conflict-driven clause learning (CDCL) solvers being the most prominent. Despite their ability to handle large instances, CDCL-based solvers have fundamental scalability limitations. In light of this, we propose recently-developed quadratic unconstrained binary optimization (QUBO) solvers as an alternative platform for 3-SAT problems. To utilize them, we implement a 2-step [3-SAT]-[Max 2-SAT]-[QUBO] conversion procedure and present a novel approach using linear systems and Diophantine equation to calculate the number of both satisfied and violated clauses of the original 3-SAT instance from the transformed Max 2-SAT formulation. We then demonstrate, through numerical simulations on several benchmark instances, that digital QUBO solvers can achieve state-of-the-art accuracy on 78-variable 3-SAT benchmark problems. Our work facilitates the broader use of quantum annealers on noisy intermediate-scale quantum devices, as well as their quantum-inspired digital counterparts, for solving 3-SAT problems.

DOI: 10.1088/1367-2630/ada572

Related papers

Transformation-Dependent Performance-Enhancement of Digital Annealer for 3-SAT

Münch, Christian, Fritz Schinkel, Sebastian Zielinski +1 more

Quadratic Unconstrained Binary Optimization (QUBO) problems are NP-hard problems and many real-world problems can be formulated as QUBO. Currently there are no algorithms known that can solve arbitrary instances of NP-hard problems efficiently. Therefore special-purpose hardware such as Digital Annealer, other Ising machines, as well as quantum annealers might lead to benefits in solving such problems. We study a particularly hard class of problems which can be formulated as QUBOs, namely Boolean satisfiability (SAT) problems, and specifically 3-SAT. One intriguing aspect about 3-SAT problems is that there are different transformations from 3-SAT to QUBO. We study the transformations' influence on the problem solution, using Digital Annealer as a special-purpose solver. Besides well-known transformations we investigate a novel in this context not yet discussed transformation, using less auxiliary variables and leading to very good performance. Using exact diagonalization, we explain the differences in performance originating from the different transformations. We envision that this knowledge allows for specifically engineering transformations that improve a solvers capacity to find high quality solutions. Furthermore, we show that the Digital Annealer outperforms a quantum annealer in solving hard 3-SAT instances.

arXiv:2312.11645•Dec 18, 2023•1 citation

A quantum annealing approach for boolean satisfiability problem

Juexiao Su, Tianheng Tu, Lei He

Quantum annealing device has shown a great potential in solving discrete problems that are theoretically and empirically hard. Boolean Satisfiability (SAT) problem, determining if there is an assignment of variables that satisfies a given Boolean function, is the first proven NP-complete problem widely used in various domains. Here, we present a novel mapping of the SAT problem to the quadratic unconstrained binary optimization problem (QUBO), and further develop a tool flow embedding the proposed QUBO to the architecture of the commercialized quantum computer D-Wave. By leveraging electronic design automation techniques including synthesis, placement and routing, this is not only the first work providing the detail flow that embeds the QUBO, but also a technique scalable for real world applications and some hard SAT problems with over 6000 variables in QUBO. Based on our results, we discuss the challenges in solving SAT using the current generation of annealing device, and explore the problem solving capability of future quantum annealing computers.

ACM/IEEE Design Automation Conference (DAC)•May 25, 2016•39 citations

Efficient QUBO transformation for Higher Degree Pseudo Boolean Functions

Amit Verma, Mark W. Lewis, Gary A. Kochenberger

Quadratic Unconstrained Binary Optimization (QUBO) is recognized as a unifying framework for modeling a wide range of problems. Problems can be solved with commercial solvers customized for solving QUBO and since QUBO have degree two, it is useful to have a method for transforming higher degree pseudo-Boolean problems to QUBO format. The standard transformation approach requires additional auxiliary variables supported by penalty terms for each higher degree term. This paper improves on the existing cubic-to-quadratic transformation approach by minimizing the number of additional variables as well as penalty coefficient. Extensive experimental testing on Max 3-SAT modeled as QUBO shows a near 100% reduction in the subproblem size used for minimization of the number of auxiliary variables.

arXiv:2107.11695•Jul 24, 2021•5 citations

On Optimal QUBO Encoding of Boolean Logic, (Max-)3-SAT and (Max-)k-SAT with Integer Programming

Gregory Morse, Tamás Kozsik

We present an asymptotic improvement in the number of variables (n + m⌊log 2(k − 1)⌋) required for state-of-the-art formulation of (max-)k-SAT problems when encoded as a quadratic unconstrained binary optimization (QUBO) problem. We further show a variable reduction technique (max-)3-SAT formula which achieves the optimal number of substitution variables. We show optimality empirically by presenting an integer linear programming (ILP) construction for arbitrary Boolean formulas. We show how various goals can be encoded, and this model can be generalized to searching for arbitrary substitution variable functions. Lastly, we show the optimal high-order substitution reduction in cubic QUBO equations which has smaller coefficients than the typical construction used.

International Conference on Algorithms, Computing and Systems (ICACS)•Oct 19, 2023•2 citations

An Approximate QUBO Formulation for Solving Practical SAT Problems

Tomohiro Sonobe

In this paper, we introduce an approximate quadratic unconstrained binary optimization (QUBO) formulation for satisfiability (SAT) problems derived from real-world applications. The proposed method is an inexact (approximate) formulation of a SAT instance as a QUBO, where the ground state of the QUBO does not correspond to the solution of the SAT instance. The method leverages the fact that practical SAT instances often contain many binary (size 2) clauses, allowing us to use a MAX2SAT formulation directly. In comparative experiments using existing formulations, the proposed method exhibits superior performance on the pigeonhole principle, graph coloring problems, and a subset of instances from the SAT Competition 2023.

Qeios•Apr 2, 2025•0 citations

An Approximated QUBO Formulation for Solving Practical SAT Problems

Tomohiro Sonobe

In this paper, we introduce an approximated quadratic unconstrained binary optimization (QUBO) formulation on satisfiability (SAT) problems derived from real-world applications. The proposed method is an inexact (approximated) formalization of a SAT instance to a QUBO, where the ground state of the QUBO does not correspond to the solution of the SAT instance. The method leverages the fact that practical SAT instances often contain many binary (size 2) clauses, allowing us to directly use a MAX2SAT formalization. In comparative experiments using existing formulations, the proposed method exhibits superior performance on the pigeonhole principle, graph coloring problems, and a subset of instances from the SAT Competition 2023. Notably, we were able to find the exact solutions of PHP instances using our method, despite its approximate formalization.

Qeios•Jan 3, 2025•0 citations

Abstract Boolean satisfiability (SAT) is a propositional logic problem of determining whether an assignment of variables satisfies a Boolean formula. Many combinatorial optimization problems can be formulated in Boolean SAT logic—either as k-SAT decision problems or Max k-SAT optimization problems, with conflict-driven clause learning (CDCL) solvers being the most prominent. Despite their ability to handle large instances, CDCL-based solvers have fundamental scalability limitations. In light of this, we propose recently-developed quadratic unconstrained binary optimization (QUBO) solvers as an alternative platform for 3-SAT problems. To utilize them, we implement a 2-step [3-SAT]-[Max 2-SAT]-[QUBO] conversion procedure and present a novel approach using linear systems and Diophantine equation to calculate the number of both satisfied and violated clauses of the original 3-SAT instance from the transformed Max 2-SAT formulation. We then demonstrate, through numerical simulations on several benchmark instances, that digital QUBO solvers can achieve state-of-the-art accuracy on 78-variable 3-SAT benchmark problems. Our work facilitates the broader use of quantum annealers on noisy intermediate-scale quantum devices, as well as their quantum-inspired digital counterparts, for solving 3-SAT problems.

Quadratic Unconstrained Binary Optimization (QUBO) problems are NP-hard problems and many real-world problems can be formulated as QUBO. Currently there are no algorithms known that can solve arbitrary instances of NP-hard problems efficiently. Therefore special-purpose hardware such as Digital Annealer, other Ising machines, as well as quantum annealers might lead to benefits in solving such problems. We study a particularly hard class of problems which can be formulated as QUBOs, namely Boolean satisfiability (SAT) problems, and specifically 3-SAT. One intriguing aspect about 3-SAT problems is that there are different transformations from 3-SAT to QUBO. We study the transformations' influence on the problem solution, using Digital Annealer as a special-purpose solver. Besides well-known transformations we investigate a novel in this context not yet discussed transformation, using less auxiliary variables and leading to very good performance. Using exact diagonalization, we explain the differences in performance originating from the different transformations. We envision that this knowledge allows for specifically engineering transformations that improve a solvers capacity to find high quality solutions. Furthermore, we show that the Digital Annealer outperforms a quantum annealer in solving hard 3-SAT instances.

Quantum annealing device has shown a great potential in solving discrete problems that are theoretically and empirically hard. Boolean Satisfiability (SAT) problem, determining if there is an assignment of variables that satisfies a given Boolean function, is the first proven NP-complete problem widely used in various domains. Here, we present a novel mapping of the SAT problem to the quadratic unconstrained binary optimization problem (QUBO), and further develop a tool flow embedding the proposed QUBO to the architecture of the commercialized quantum computer D-Wave. By leveraging electronic design automation techniques including synthesis, placement and routing, this is not only the first work providing the detail flow that embeds the QUBO, but also a technique scalable for real world applications and some hard SAT problems with over 6000 variables in QUBO. Based on our results, we discuss the challenges in solving SAT using the current generation of annealing device, and explore the problem solving capability of future quantum annealing computers.

Quadratic Unconstrained Binary Optimization (QUBO) is recognized as a unifying framework for modeling a wide range of problems. Problems can be solved with commercial solvers customized for solving QUBO and since QUBO have degree two, it is useful to have a method for transforming higher degree pseudo-Boolean problems to QUBO format. The standard transformation approach requires additional auxiliary variables supported by penalty terms for each higher degree term. This paper improves on the existing cubic-to-quadratic transformation approach by minimizing the number of additional variables as well as penalty coefficient. Extensive experimental testing on Max 3-SAT modeled as QUBO shows a near 100% reduction in the subproblem size used for minimization of the number of auxiliary variables.

We present an asymptotic improvement in the number of variables (n + m⌊log 2(k − 1)⌋) required for state-of-the-art formulation of (max-)k-SAT problems when encoded as a quadratic unconstrained binary optimization (QUBO) problem. We further show a variable reduction technique (max-)3-SAT formula which achieves the optimal number of substitution variables. We show optimality empirically by presenting an integer linear programming (ILP) construction for arbitrary Boolean formulas. We show how various goals can be encoded, and this model can be generalized to searching for arbitrary substitution variable functions. Lastly, we show the optimal high-order substitution reduction in cubic QUBO equations which has smaller coefficients than the typical construction used.

In this paper, we introduce an approximate quadratic unconstrained binary optimization (QUBO) formulation for satisfiability (SAT) problems derived from real-world applications. The proposed method is an inexact (approximate) formulation of a SAT instance as a QUBO, where the ground state of the QUBO does not correspond to the solution of the SAT instance. The method leverages the fact that practical SAT instances often contain many binary (size 2) clauses, allowing us to use a MAX2SAT formulation directly. In comparative experiments using existing formulations, the proposed method exhibits superior performance on the pigeonhole principle, graph coloring problems, and a subset of instances from the SAT Competition 2023.

In this paper, we introduce an approximated quadratic unconstrained binary optimization (QUBO) formulation on satisfiability (SAT) problems derived from real-world applications. The proposed method is an inexact (approximated) formalization of a SAT instance to a QUBO, where the ground state of the QUBO does not correspond to the solution of the SAT instance. The method leverages the fact that practical SAT instances often contain many binary (size 2) clauses, allowing us to directly use a MAX2SAT formalization. In comparative experiments using existing formulations, the proposed method exhibits superior performance on the pigeonhole principle, graph coloring problems, and a subset of instances from the SAT Competition 2023. Notably, we were able to find the exact solutions of PHP instances using our method, despite its approximate formalization.