An Approximated QUBO Formulation for Solving Practical SAT Problems

In this paper, we introduce an approximated quadratic unconstrained binary optimization (QUBO) formulation on satisfiability (SAT) problems derived from real-world applications. The proposed method is an inexact (approximated) formalization of a SAT instance to a QUBO, where the ground state of the QUBO does not correspond to the solution of the SAT instance. The method leverages the fact that practical SAT instances often contain many binary (size 2) clauses, allowing us to directly use a MAX2SAT formalization. In comparative experiments using existing formulations, the proposed method exhibits superior performance on the pigeonhole principle, graph coloring problems, and a subset of instances from the SAT Competition 2023. Notably, we were able to find the exact solutions of PHP instances using our method, despite its approximate formalization.