论文标题
MaxSat分辨率和子立方体总和
MaxSAT Resolution and Subcube Sums
论文作者
论文摘要
我们在认证难以满足的背景下研究Maxres规则。我们表明，它可以比树状分辨率更强大，并且当通过弱化（系统maxResw）增强时，p缩减了树状分辨率。在设计特定于MaxRes的下边界技术（不仅是从RES继承下限），我们定义了一个称为SubibeSums Proof System的新的证明系统。 P-Sud-Sud-Sud-MaxResw的该系统可被视为半ge骨SHERI-ADAMS防止系统的特殊情况。在表达性方面，这是对通信复杂性和扩展复杂性的圆锥形作物的整体限制。我们表明它不是由RES模拟的。使用与MaxResw从RES继承的下限差异不同的证明技术，我们表明在膨胀者图上的三链蛋白矛盾很难在亚底部中进行反驳。我们还通过举重建立了下限技术：对于需要大尺寸的公式，它们的XOR化材料需要大尺寸的亚剪下。
We study the MaxRes rule in the context of certifying unsatisfiability. We show that it can be exponentially more powerful than tree-like resolution, and when augmented with weakening (the system MaxResW), p-simulates tree-like resolution. In devising a lower bound technique specific to MaxRes (and not merely inheriting lower bounds from Res), we define a new proof system called the SubCubeSums proof system. This system, which p-simulates MaxResW, can be viewed as a special case of the semialgebraic Sherali-Adams proof system. In expressivity, it is the integral restriction of conical juntas studied in the contexts of communication complexity and extension complexity. We show that it is not simulated by Res. Using a proof technique qualitatively different from the lower bounds that MaxResW inherits from Res, we show that Tseitin contradictions on expander graphs are hard to refute in SubCubeSums. We also establish a lower bound technique via lifting: for formulas requiring large degree in SubCubeSums, their XOR-ification requires large size in SubCubeSums.
