Strong Structural Bounds for MaxSAT: The Fine Details of Using Neuromorphic and Quantum Hardware Accelerators

TL;DR

The paper addresses the challenge of leveraging hardware-accelerated solvers for MaxSAT by embedding the problem into QUBO through structure-aware, treewidth-preserving reductions. It proves that MaxSAT, Max2SAT, and QUBO are equivalent under linear-time reductions that preserve either the primal $tw$ or the incidence $itw$, yielding tight ETH/SETH lower bounds and a time-optimal $QUBO$-oriented algorithm. It also develops new upper bounds for MaxSAT variants via reductions to $\#SAT$ and model counting, including linear-time unary, multiplicative, and lexicographic cases, thus offering a unified, width-aware framework for cost-optimal reasoning. Practically, these results clarify when Ising-machine based executables are feasible and guide future experimental deployments by providing explicit width-related performance guarantees and reductions that minimize structural inflation.

Abstract

Hardware accelerators like quantum annealers or neuromorphic chips are capable of finding the ground state of a Hamiltonian. A promising route in utilizing these devices is via methods from automated reasoning: The problem at hand is first encoded into MaxSAT; then MaxSAT is reduced to Max2SAT; and finally, Max2SAT is translated into a Hamiltonian. It was observed that different encodings can dramatically affect the efficiency of the hardware accelerators. Yet, previous studies were only concerned with the size of the encodings rather than with syntactic or structural properties. We establish structure-aware reductions between MaxSAT, Max2SAT, and the quadratic unconstrained binary optimization problem (QUBO) that underlies such hardware accelerators. All these problems turn out to be equivalent under linear-time, treewidth-preserving reductions. As a consequence, we obtain tight lower bounds under ETH and SETH for Max2SAT and QUBO, as well as a new time-optimal fixed-parameter algorithm for QUBO. While our results are tight up to a constant additive factor for the primal treewidth, we require a constant multiplicative factor for the incidence treewidth. To close the emerging gap, we supplement our results with novel time-optimal algorithms for fragments of MaxSAT based on model counting.

Figures (2)

• Figure 1: Illustration of an ipu that operates on an $n$-variable Ising model $H(x_1,\dots,x_n)$. The input are the weights of $H$ given as $n\times n$ upper triangular matrix ($n$ is fixed). The output is a vector $\vec{x}\in\{0,1\}^n$ that minimizes $H(\vec{x})$.
• Figure 2: An overview of our reductions between various variants of maxsat. All reductions in the picture are linear-time computable. An arrow $A\stackrel{a\mathop{\mathrm{\mathrm{tw}}}\nolimits+b}{\rightarrow} B$ means that if the instance of $A$ has primal treewidth $\mathop{\mathrm{\mathrm{tw}}}\nolimits$, the instance of $B$ has primal treewidth at most $a\mathop{\mathrm{\mathrm{tw}}}\nolimits+b$. If the label of an arrow is "$\max(\mathop{\mathrm{\mathrm{tw}}}\nolimits,x)$", the reduction increases the treewidth to at most $x$. Finally, if the arrow is dashed, the reduction requires a tree decomposition as input. The green arrows are implied by the transitive closure.

Theorems & Definitions (41)

• Theorem 1: Main Theorem
• Corollary 1: qubo Upper Bound
• Corollary 2: max2sat Lower Bound
• Corollary 3: qubo Lower Bound
• Theorem 2
• Theorem 3
• Corollary 4
• proof
• Example 1
• Example 2