MaxSAT 分辨率和子立方和
摘要：MaxRes规则在验证不可满足性的背景下被研究。我们展示了它在效果上可以比树形分辨率强数倍，并且当与削弱（MaxResW系统）结合时，可以p-模拟树形分辨率。为了设计一种特定于MaxRes的下界技术（而不仅仅继承来自Res的下界），我们定义了一个新的证明系统，称为SubCubeSums证明系统。这个系统可以p-模拟MaxResW，可以看作是半代数Sherali-Adams证明系统的一个特例。在表达能力上，它是在通信复杂度和扩展复杂度的上下文中研究的锥形juntas的积分约束。我们证明了它在Res中无法模拟。通过一种与MaxResW继承自Res的下界 qualitatively不同的证明技术，我们证明了在SubCubeSums中难以反驳扩展图上的Tseitin矛盾。我们还通过lifting建立了一种新的下界技术：对于在SubCubeSums中需要较大度数的公式，它们在SubCubeSums中的XOR-ication需要较大的大小。
作者：Yuval Filmus, Meena Mahajan, Gaurav Sood, Marc Vinyals
论文ID：2005.11589
分类：Computational Complexity
分类简称：cs.CC
提交时间：2023-04-13