In Between Resolution and Cutting Planes: A Study of Proof Systems for Pseudo-Boolean SAT Solving
Lecture Notes in Computer Science(2018)
摘要
We initiate a proof complexity theoretic study of subsystems of cutting planes (CP) modelling proof search in conflict-driven pseudo-Boolean (PB) solvers. These algorithms combine restrictions such as that addition of constraints should always cancel a variable and/or that so-called saturation is used instead of division. It is known that on CNF inputs cutting planes with cancelling addition and saturation is essentially just resolution. We show that even if general addition is allowed, this proof system is still polynomially simulated by resolution with respect to proof size as long as coefficients are polynomially bounded.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络