Implementing 3-SAT Gadgets for Quantum Annealers with Random Instances

The Maximum Boolean Satisfiability Problem (also known as the Max-SAT problem) is the problem of determining the maximum number of disjunctive clauses that can be satisfied (i.e., made true) by an assignment of truth values to the formula’s variables. This is a generalization of the well-known Boolean Satisfiability Problem (also known as the SAT problem), the first problem that was proven to be NP-complete. With the proliferation of quantum computing, a current approach to tackle this optimization problem is Quantum Annealing (QA). In this work, we compare several gadgets that translate 3-SAT problems into Quadratic Unconstrained Binary Optimization (QUBO) problems to be able to solve them in a quantum annealer. We show the performance superiority of the not-yet-considered gadgets in comparison to state-of-the-art approaches when solving random instances in D-Wave’s quantum annealer.