Strong Structural Bounds for MaxSAT: The Fine Details of Using Neuromorphic and Quantum Hardware Accelerators
摘要
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 accelerators. All these problems turn out to be equivalent under linear-time, treewidth-preserving reductions. As a consequence, we obtain tight lower bounds under \(\mathchoice{{ \textrm{ETH}}}{{ \textrm{ETH}}}{{ \textrm{ETH}}}{{ \textrm{ETH}}}\) and \(\mathchoice{{ \textrm{SETH}}}{{ \textrm{SETH}}}{{ \textrm{SETH}}}{{ \textrm{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 multiplicative factor for the incidence treewidth. To close this gap, we supplement our results with time-optimal algorithms for fragments of maxsat based on model counting.