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

TL;DR

This paper develops structure-aware reductions between MaxSAT, Max2SAT, and QUBO, providing tight bounds and algorithms that leverage structural properties like treewidth to optimize hardware acceleration methods.

Contribution

It introduces linear-time, treewidth-preserving reductions between MaxSAT, Max2SAT, and QUBO, establishing tight bounds and new algorithms based on structural properties.

Findings

All problems are equivalent under treewidth-preserving reductions.

Established tight lower bounds for Max2SAT and QUBO under ETH and SETH.

Provided time-optimal algorithms for certain MaxSAT fragments.

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.