没有新变量的更短证明
摘要：SAT求解器的证明格式在过去十年中多样化，实现了新的功能，如扩展的类分辨率能力、非常通用的扩展无规则、包含证明提示和伪布尔推理。干扰基方法已被证明是有效的，并且一些理论工作已经在更好地解释它们的限制和语义方面进行了。在这项工作中，我们结合了（Buss, Thapen 2019）中的包容冗余概念和（Rebola-Pardo, Suda 2018）中的重写逻辑框架。然后，自然的泛化变得明显，可以比（Heule, Kiesl, Biere 2017）的鸽洞原理证明更短，并产生更小的不可满足核生成。
作者：Adri''an Rebola-Pardo
论文ID：2307.12098
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-07-25