Efficient digital quadratic unconstrained binary optimization solvers for SAT problems
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 co...
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
IOP Publishing
2025-01-01
|
| Series: | New Journal of Physics |
| Subjects: | |
| Online Access: | https://doi.org/10.1088/1367-2630/ada572 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1832578896505077760 |
|---|---|
| author | Robert Simon Fong Yanming Song Alexander Yosifov |
| author_facet | Robert Simon Fong Yanming Song Alexander Yosifov |
| author_sort | Robert Simon Fong |
| collection | DOAJ |
| description | 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. |
| format | Article |
| id | doaj-art-948834b8c84148f5a91f91a5dafd02a5 |
| institution | Kabale University |
| issn | 1367-2630 |
| language | English |
| publishDate | 2025-01-01 |
| publisher | IOP Publishing |
| record_format | Article |
| series | New Journal of Physics |
| spelling | doaj-art-948834b8c84148f5a91f91a5dafd02a52025-01-30T13:19:55ZengIOP PublishingNew Journal of Physics1367-26302025-01-0127101302710.1088/1367-2630/ada572Efficient digital quadratic unconstrained binary optimization solvers for SAT problemsRobert Simon Fong0https://orcid.org/0000-0002-3972-6146Yanming Song1https://orcid.org/0009-0007-5037-0850Alexander Yosifov2https://orcid.org/0000-0002-6545-1174School of Computer Science, University of Birmingham , Birmingham B15 2TT, United KingdomTheory Lab, Central Research Institute, 2012 Labs, Huawei Technology Co. Ltd. , Hong Kong Science Park, Hong Kong SAR, People’s Republic of ChinaTheory Lab, Central Research Institute, 2012 Labs, Huawei Technology Co. Ltd. , Hong Kong Science Park, Hong Kong SAR, People’s Republic of ChinaBoolean 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.https://doi.org/10.1088/1367-2630/ada572QUBOsatisfibilityk-SAT |
| spellingShingle | Robert Simon Fong Yanming Song Alexander Yosifov Efficient digital quadratic unconstrained binary optimization solvers for SAT problems New Journal of Physics QUBO satisfibility k-SAT |
| title | Efficient digital quadratic unconstrained binary optimization solvers for SAT problems |
| title_full | Efficient digital quadratic unconstrained binary optimization solvers for SAT problems |
| title_fullStr | Efficient digital quadratic unconstrained binary optimization solvers for SAT problems |
| title_full_unstemmed | Efficient digital quadratic unconstrained binary optimization solvers for SAT problems |
| title_short | Efficient digital quadratic unconstrained binary optimization solvers for SAT problems |
| title_sort | efficient digital quadratic unconstrained binary optimization solvers for sat problems |
| topic | QUBO satisfibility k-SAT |
| url | https://doi.org/10.1088/1367-2630/ada572 |
| work_keys_str_mv | AT robertsimonfong efficientdigitalquadraticunconstrainedbinaryoptimizationsolversforsatproblems AT yanmingsong efficientdigitalquadraticunconstrainedbinaryoptimizationsolversforsatproblems AT alexanderyosifov efficientdigitalquadraticunconstrainedbinaryoptimizationsolversforsatproblems |