On Optimal QUBO Encoding of Boolean Logic, (Max-)3-SAT and (Max-)k-SAT with Integer Programming
Gregory Morse, Tamás Kozsik · 2023
We present an asymptotic improvement in the number of variables (n + m⌊log 2(k − 1)⌋) required for state-of-the-art formulation of (max-)k-SAT problems when encoded as a quadratic unconstrained binary optimization (QUBO) problem. We further show a variable reduction technique (max-)3-SAT formula which achieves the optimal number of substitution variables. We show optimality empirically by presenting an integer linear programming (ILP) construction for arbitrary Boolean formulas. We show how various goals can be encoded, and this model can be generalized to searching for arbitrary substitution variable functions. Lastly, we show the optimal high-order substitution reduction in cubic QUBO equations which has smaller coefficients than the typical construction used.