Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Log inSign up
Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Blog
Job Board
Q3AS

© 2026 Aqora Quantum S.A.S.

TermsPrivacyLegal Notice

Qeios

An Approximate QUBO Formulation for Solving Practical SAT Problems

Tomohiro Sonobe

Published Apr 2, 2025• 0 citations
Publisher

Abstract

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.

DOI
10.32388/jd6k4g.3

Related papers

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

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 29, 2025•0 citations

Efficient digital quadratic unconstrained binary optimization solvers for SAT problems

Robert Simon Fong, Yanming Song, Alexander Yosifov

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.

arXiv:2408.03757•New Journal of Physics•Jan 1, 2025•1 citation

Algorithmic QUBO formulations for k -SAT and hamiltonian cycles

Jonas Nüßlein, Thomas Gabor, Claudia Linnhoff–Popien +1 more

Quadratic Unconstrained Binary Optimization (QUBO) can be seen as a generic language for optimization problems. QUBOs attract particular attention since they can be solved with quantum hardware, like quantum annealers or quantum gate computers running QAOA. In this paper, we present two novel QUBO formulations for k-SAT and Hamiltonian Cycles that scale significantly better than existing approaches. For k-SAT we reduce the growth of the QUBO matrix from O(k) to O(log(k)). For Hamiltonian Cycles the matrix no longer grows quadratically in the number of nodes, as currently, but linearly in the number of edges and logarithmically in the number of nodes.

arXiv:2204.13539•Genetic and Evolutionary Computation Conference Companion (GECCO Companion)•Jul 9, 2022•18 citations

Resource-Constrained Heuristic for Max-SAT

Brian Matejek, Daniel Elenius, Cale M. Gentry +2 more

We propose a resource-constrained heuristic for instances of Max-SAT that iteratively decomposes a larger problem into smaller subcomponents that can be solved by optimized solvers and hardware. The unconstrained outer loop maintains the state space of a given problem and selects a subset of the SAT variables for optimization independent of previous calls. The resource-constrained inner loop maximizes the number of satisfiable clauses in the "sub-SAT" problem. Our outer loop is agnostic to the mechanisms of the inner loop, allowing for the use of traditional solvers for the optimization step. However, we can also transform the selected "sub-SAT" problem into a quadratic unconstrained binary optimization (QUBO) one and use specialized hardware for optimization. In contrast to existing solutions that convert a SAT instance into a QUBO one before decomposition, we choose a subset of the SAT variables before QUBO optimization. We analyze a set of variable selection methods, including a novel graph-based method that exploits the structure of a given SAT instance. The number of QUBO variables needed to encode a (sub-)SAT problem varies, so we additionally learn a model that predicts the size of sub-SAT problems that will fit a fixed-size QUBO solver. We empirically demonstrate our results on a set of randomly generated Max-SAT instances as well as real world examples from the Max-SAT evaluation benchmarks and outperform existing QUBO decomposer solutions.

arXiv:2410.09173•Oct 11, 2024•1 citation

A penalty-free QUBO formulation for the minimum maximal matching problem

Yozo Nakahara, Shunsuke Tsukiyama, Koji Nakano +2 more

Given an undirected graph, a matching is a set of edges with no shared vertices. A maximal matching cannot be extended by adding edges without violating this condition. The minimum maximal matching problem seeks the smallest such matching. While it can be formulated as a Quadratic Unconstrained Binary Optimization (QUBO) problem, existing methods require complex penalty terms. This paper presents a novel, penalty-free QUBO formulation that is simpler and more intuitive. We analyze its theoretical properties and evaluate its performance using several QUBO solvers. Our approach enhances the practicality of QUBO-based optimization for combinatorial graph problems.

International Journal of Parallel Emergent and Distributed Systems•Nov 7, 2025•0 citations
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.
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.
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) can be seen as a generic language for optimization problems. QUBOs attract particular attention since they can be solved with quantum hardware, like quantum annealers or quantum gate computers running QAOA. In this paper, we present two novel QUBO formulations for k-SAT and Hamiltonian Cycles that scale significantly better than existing approaches. For k-SAT we reduce the growth of the QUBO matrix from O(k) to O(log(k)). For Hamiltonian Cycles the matrix no longer grows quadratically in the number of nodes, as currently, but linearly in the number of edges and logarithmically in the number of nodes.
We propose a resource-constrained heuristic for instances of Max-SAT that iteratively decomposes a larger problem into smaller subcomponents that can be solved by optimized solvers and hardware. The unconstrained outer loop maintains the state space of a given problem and selects a subset of the SAT variables for optimization independent of previous calls. The resource-constrained inner loop maximizes the number of satisfiable clauses in the "sub-SAT" problem. Our outer loop is agnostic to the mechanisms of the inner loop, allowing for the use of traditional solvers for the optimization step. However, we can also transform the selected "sub-SAT" problem into a quadratic unconstrained binary optimization (QUBO) one and use specialized hardware for optimization. In contrast to existing solutions that convert a SAT instance into a QUBO one before decomposition, we choose a subset of the SAT variables before QUBO optimization. We analyze a set of variable selection methods, including a novel graph-based method that exploits the structure of a given SAT instance. The number of QUBO variables needed to encode a (sub-)SAT problem varies, so we additionally learn a model that predicts the size of sub-SAT problems that will fit a fixed-size QUBO solver. We empirically demonstrate our results on a set of randomly generated Max-SAT instances as well as real world examples from the Max-SAT evaluation benchmarks and outperform existing QUBO decomposer solutions.
Given an undirected graph, a matching is a set of edges with no shared vertices. A maximal matching cannot be extended by adding edges without violating this condition. The minimum maximal matching problem seeks the smallest such matching. While it can be formulated as a Quadratic Unconstrained Binary Optimization (QUBO) problem, existing methods require complex penalty terms. This paper presents a novel, penalty-free QUBO formulation that is simpler and more intuitive. We analyze its theoretical properties and evaluate its performance using several QUBO solvers. Our approach enhances the practicality of QUBO-based optimization for combinatorial graph problems.