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.

翻译：量子退火器或神经形态芯片等硬件加速器能够找到哈密顿量的基态。利用这些设备的一条有前景的途径是通过自动推理方法：首先将待解问题编码为MaxSAT；然后将MaxSAT规约为Max2SAT；最后将Max2SAT转化为哈密顿量。已有研究观察到，不同编码方式会显著影响硬件加速器的效率。然而，先前研究仅关注编码规模，而未考虑句法或结构特性。本文建立了MaxSAT、Max2SAT与作为此类硬件加速器基础的二次无约束二进制优化问题（QUBO）之间的结构感知规约关系。在线性时间且保持树宽不变的规约下，这些问题被证明是等价的。由此，我们获得了Max2SAT和QUBO在ETH与SETH假设下的紧致下界，以及一种新的时间最优固定参数QUBO算法。虽然我们的结果在原始树宽上达到常数加性因子的紧致性，但在关联树宽上需要常数乘性因子。为填补由此产生的间隙，我们基于模型计数方法，为MaxSAT的片段补充了新颖的时间最优算法。