Abstract
In this paper, we present an open-source Python framework, called satqubolib. This framework aims to provide all necessary tools for solving (MAX)-3SAT problems on quantum hardware systems via Quadratic Unconstrained Binary Optimization (QUBO). Our framework solves two major issues when solving (MAX)-3SAT instances in the context of quantum computing. Firstly, a common way of solving satisfiability instances with quantum methods is, to transform these instances into instances of QUBO, as QUBO is the input format for quantum annealers and the Quantum Approximate Optimization Algorithm (QAOA) on quantum gate systems. Studies have shown, that the choice of this transformation can significantly impact the solution quality of quantum hardware systems. Thus, our framework provides thousands of usable QUBO transformations for satisfiability problems. Doing so also enables practitioners from any domain to immediately explore and use quantum techniques as a potential solver for their domain-specific problems, as long as they can be encoded as satisfiability problems. As a second contribution, we created a dataset of 6000 practically hard and satisfiable SAT instances that are also small enough to be solved with current quantum(-hybrid) methods. This dataset enables meaningful benchmarking of new quantum, quantum-hybrid, and classical methods for solving satisfiability problems.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
- 2.
pip install satqubolib
- 3.
References
2011, S.C.: Sat competition 2011: Benchmark submission guidelines (2011). https://satcompetition.github.io/2023/benchmarks.html. Accessed 9 Feb 2024
Abate, P., Di Cosmo, R., Gousios, G., Zacchiroli, S.: Dependency solving is still hard, but we are getting better at it. In: 2020 IEEE 27th International Conference on Software Analysis, Evolution and Reengineering (SANER), pp. 547–551. IEEE (2020)
Arora, S., Barak, B.: Computational complexity: a modern approach. Cambrtidge University Press (2009)
Balyo, T., Heule, M., Iser, M., Järvisalo, M., Suda, M. (eds.): Proceedings of SAT Competition 2023: Solver, Benchmark and Proof Checker Descriptions. Department of Computer Science Series of Publications B, Department of Computer Science, University of Helsinki, Finland (2023)
Barták, R., Salido, M.A., Rossi, F.: Constraint satisfaction techniques in planning and scheduling. J. Intell. Manuf. 21, 5–15 (2010)
Biere, A., Fleury, M.: Kissat homepage (2020). https://fmv.jku.at/kissat/ Accessed Feb 11 2024
Chancellor, N., Zohren, S., Warburton, P.A., Benjamin, S.C., Roberts, S.: A direct mapping of max k-sat and high order parity checks to a chimera graph. Sci. Rep. 6(1), 37107 (2016)
Choi, V.: Adiabatic quantum algorithms for the np-complete maximum-weight independent set, exact cover and 3sat problems. arXiv preprint arXiv:1004.2226 (2010)
Cook, S.A.: The complexity of theorem-proving procedures. In: Proceedings of the Third Annual ACM Symposium on Theory of Computing, pp. 151–158 (1971)
Duan, Q., Al-Haj, S., Al-Shaer, E.: Provable configuration planning for wireless sensor networks. In: 2012 8th International Conference on Network and Service Management (cnsm) and 2012 Workshop on Systems Virtualiztion Management (svm), pp. 316–321. IEEE (2012)
Escamocher, G., O’Sullivan, B., Prestwich, S.D.: Generating difficult sat instances by preventing triangles. arXiv preprint arXiv:1903.03592 (2019)
Glover, F., Kochenberger, G., Du, Y.: A tutorial on formulating and using qubo models. arXiv preprint arXiv:1811.11538 (2018)
Gutin, G., Karapetyan, D.: Constraint branching in workflow satisfiability problem. In: Proceedings of the 25th ACM Symposium on Access Control Models and Technologies, pp. 93–103 (2020)
Hoos, H.H., Stützle, T.: Satlib: an online resource for research on sat. Sat 2000, 283–292 (2000)
Ignatiev, A., Morgado, A., Marques-Silva, J.: PySAT: a python toolkit for prototyping with SAT oracles. In: Beyersdorff, O., Wintersteiger, C.M. (eds.) Theory and Applications of Satisfiability Testing – SAT 2018: 21st International Conference, SAT 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9–12, 2018, Proceedings, pp. 428–437. Springer International Publishing, Cham (2018). https://doi.org/10.1007/978-3-319-94144-8_26
Jose, M., Majumdar, R.: Cause clue clauses: error localization using maximum satisfiability. ACM SIGPLAN Notices 46(6), 437–446 (2011)
Karapetyan, D., Parkes, A.J., Gutin, G., Gagarin, A.: Pattern-based approach to the workflow satisfiability problem with user-independent constraints. J. Artif. Intell. Res. 66, 85–122 (2019)
Krüger, T., Mauerer, W.: Quantum annealing-based software components: An experimental case study with sat solving. In: Proceedings of the IEEE/ACM 42nd International Conference on Software Engineering Workshops, pp. 445–450 (2020)
Lucas, A.: Ising formulations of many np problems. Front. Phys. 2, 5 (2014)
Marques-Silva, J.P., Sakallah, K.A.: Boolean satisfiability in electronic design automation. In: Proceedings of the 37th Annual Design Automation Conference, pp. 675–680 (2000)
Nüßlein, J., Gabor, T., Linnhoff-Popien, C., Feld, S.: Algorithmic qubo formulations for k-sat and hamiltonian cycles. In: Proceedings of the Genetic and Evolutionary Computation Conference Companion, pp. 2240–2246 (2022)
Nüßlein, J., Zielinski, S., Gabor, T., Linnhoff-Popien, C., Feld, S.: Solving (max) 3-sat via quadratic unconstrained binary optimization. arXiv preprint arXiv:2302.03536 (2023)
Radicchi, F., Vilone, D., Yoon, S., Meyer-Ortmanns, H.: Social balance as a satisfiability problem of computer science. Phys. Rev. E 75(2), 026106 (2007)
Rintanen, J.: Planning as satisfiability: Heuristics. Artif. Intell. 193, 45–86 (2012)
Rintanen, J., Heljanko, K., Niemelä, I.: Planning as satisfiability: parallel plans and algorithms for plan search. Artif. Intell. 170(12–13), 1031–1080 (2006)
Selman, B., Mitchell, D.G., Levesque, H.J.: Generating hard satisfiability problems. Artif. Intell. 81(1–2), 17–29 (1996)
Shor, P.W.: Algorithms for quantum computation: discrete logarithms and factoring. In: Proceedings 35th Annual Symposium on Foundations of Computer Science, pp. 124–134. IEEE (1994)
Spence, I.: Balanced random sat benchmarks. SAT Competition 2017, 53 (2017)
Verma, A., Lewis, M., Kochenberger, G.: Efficient qubo transformation for higher degree pseudo boolean functions. arXiv preprint arXiv:2107.11695 (2021)
Zaman, M., Tanahashi, K., Tanaka, S.: Pyqubo: Python library for mapping combinatorial optimization problems to qubo form. IEEE Trans. Comput. 71(4), 838–850 (2021)
Zielinski, S., Nüßlein, J., Stein, J., Gabor, T., Linnhoff-Popien, C., Feld, S.: Influence of different 3sat-to-qubo transformations on the solution quality of quantum annealing: A benchmark study. In: Proceedings of the Companion Conference on Genetic and Evolutionary Computation, pp. 2263–2271. GECCO ’23 Companion, Association for Computing Machinery, New York, NY, USA (2023). https://doi.org/10.1145/3583133.3596330
Zielinski, S., Nüßlein, J., Stein, J., Gabor, T., Linnhoff-Popien, C., Feld, S.: Pattern qubos: algorithmic construction of 3sat-to-qubo transformations. Electronics 12(16) (2023). https://doi.org/10.3390/electronics12163492, https://www.mdpi.com/2079-9292/12/16/3492
Acknowledgments
The partial funding of this paper by the German Federal Ministry of Education and Research through the funding program “quantum technologies — from basic research to market” (contract number: 13N16196) is gratefully acknowledged.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2024 The Author(s), under exclusive license to Springer Nature Switzerland AG
About this paper
Cite this paper
Zielinski, S., Benkard, M., Nüßlein, J., Linnhoff-Popien, C., Feld, S. (2024). SATQUBOLIB: A Python Framework for Creating and Benchmarking (Max-)3SAT QUBOs. In: Phillipson, F., Eichler, G., Erfurth, C., Fahrnberger, G. (eds) Innovations for Community Services. I4CS 2024. Communications in Computer and Information Science, vol 2109. Springer, Cham. https://doi.org/10.1007/978-3-031-60433-1_4
Download citation
DOI: https://doi.org/10.1007/978-3-031-60433-1_4
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-031-60432-4
Online ISBN: 978-3-031-60433-1
eBook Packages: Computer ScienceComputer Science (R0)