SATQUBOLIB
A Python Framework for Creating and Benchmarking (Max-)3SAT QUBOs
Sebastian Zielinski (Ludwig Maximilians University)
Magdalena Benkard (Ludwig Maximilians University)
Jonas Nüßlein (Ludwig Maximilians University)
Claudia Linnhoff-Popien (Ludwig Maximilians University)
Sebastian Feld (TU Delft - Quantum Circuit Architectures and Technology)
More Info
expand_more
Other than for strictly personal use, it is not permitted to download, forward or distribute the text or part of it, without the consent of the author(s) and/or copyright holder(s), unless the work is under an open content license such as Creative Commons.
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.