Mining Propositional Simplification Proofs for Small Validating Clauses
Mining Propositional Simplification Proofs for Small Validating Clauses
复制标题
小型验证子句的挖掘命题简化证明
DOI：
10.1016/j.entcs.2005.12.008
复制
发表时间：
2005
期刊：
影响因子：
--
通讯作者：
Aaron Stump
中科院分区：
文献类型：
--
作者：
Ian Wehrman;Aaron Stump
在SMT系统中获取小冲突子句的问题最近受到了极大的关注。我们报告了正在进行的工作，以找到当前部分分配的小子集，这些子集在目标公式已被命题简化为布尔值时隐含目标公式。使用的方法是代数证明挖掘。来自命题推理机的目标等价于布尔值（在当前赋值中）的证明被视为一阶项。然后定义了一个证明之间的方程理论，这是关于准序的声音“证明了一个更一般的集合定理”。理论完成，以获得一个收敛的重写系统，把证明成一个规范的形式。虽然我们的规范形式没有使用当前赋值的最小子集，但它确实删除了许多不必要的证明部分。本文最后讨论了问题的复杂性和方法的有效性。
The problem of obtaining small conflict clauses in SMT systems has received a great deal of attention recently. We report work in progress to find small subsets of the current partial assignment that imply the goal formula when it has been propositionally simplified to a boolean value. The approach used is algebraic proof mining. Proofs from a propositional reasoner that the goal is equivalent to a boolean value (in the current assignment) are viewed as first-order terms. An equational theory between proofs is then defined, which is sound with respect to the quasi-order “proves a more general set theorems.” The theory is completed to obtain a convergent rewrite system that puts proofs into a canonical form. While our canonical form does not use the smallest subset of the current assignment, it does drop many unnecessary parts of the proof. The paper concludes with discussion of the complexity of the problem and effectiveness of the approach.