SATQUBOLIB

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.