MaxSAT 的强结构下界：使用神经形态与量子硬件加速器的精细细节
计算机科学中的逻辑
2025-03-06 v2 量子物理
摘要
量子退火器或神经形态芯片等硬件加速器能够寻找哈密顿量的基态。利用这些设备的一条有前景的途径是通过自动推理方法：首先将手头的问题编码为 MaxSAT；然后将 MaxSAT 归约为 Max2SAT；最后将 Max2SAT 转化为哈密顿量。已有观察表明，不同的编码会极大地影响硬件加速器的效率。然而，以往的研究仅关注编码的大小，而非句法或结构性质。我们在 MaxSAT、Max2SAT 以及此类硬件加速器所基于的二次无约束二元优化问题 (QUBO) 之间建立了结构感知的归约。所有这些问题在线性时间且保持树宽的归约下被证明是等价的。作为推论，我们得到了基于 ETH 和 SETH 的 Max2SAT 和 QUBO 的紧致下界，以及一种新的时间最优的 QUBO 固定参数算法。虽然我们的结果对于原始树宽在常数加性因子内是紧致的，但对于关联树宽则需要常数乘性因子。为了弥合由此产生的差距，我们基于模型计数补充了 MaxSAT 片段的新型时间最优算法。
引用
@article{arxiv.2412.10289,
title = {Strong Structural Bounds for MaxSAT: The Fine Details of Using Neuromorphic and Quantum Hardware Accelerators},
author = {Max Bannach and Jai Grover and Markus Hecher},
journal= {arXiv preprint arXiv:2412.10289},
year = {2025}
}