Improved Single Pass Algorithms for Resolution Proof Reduction
Improved Single Pass Algorithms for Resolution Proof Reduction
复制标题
改进的单通道算法可降低分辨率证明
DOI：
10.1007/978-3-642-33386-6_10
复制
发表时间：
2012
期刊：
影响因子：
--
通讯作者：
Ashutosh Gupta
中科院分区：
文献类型：
--
作者：
Ashutosh Gupta
不可满足性证明在验证中有许多应用。今天，许多SAT求解器都能够产生不可满足性的分辨率证明。为了提高效率，较小的证明优于较大的证明。求解器在生成证明的同时和之后应用证明归约方法来移除证明的冗余部分。减少分辨率证明的一种方法是冗余分辨率减少，即，移除解决方案证明路径中的重复枢轴（又名枢轴回收）。已知的单遍算法仅尝试移除证明中为树的部分中的冗余。在本文中，我们提出了三个修改，以改善算法，使冗余可以发现的部分证明，是DAG。与已知算法相比，第一修改算法覆盖更大数量的冗余，而不产生任何额外的成本。第二个修改的算法覆盖了更多的冗余，但它可能具有更长的运行时间。我们的第三个修改后的算法是参数化的，可以权衡运行时间和覆盖率的冗余。我们已经实现了我们的算法在OpenSMT和应用它们的不满足性证明的198个例子，从平原MUS轨道的SAT11比赛。与原始算法相比，第一和第二算法分别额外删除了0.89%和10.57%的子句。对于参数的特定值，第三种算法删除的子句几乎与第二种算法一样多，但速度明显更快。
Unsatisfiability proofs find many applications in verification. Today, many SAT solvers are capable of producingresolution proofsof unsatisfiability. For efficiency smaller proofs are preferred over bigger ones. The solvers apply proof reduction methods to remove redundant parts of the proofs while and after generating the proofs. One method of reducing resolution proofs isredundant resolution reduction, i.e., removing repeated pivots in the paths of resolution proofs (akaPivot recycle). The known single pass algorithm only tries to remove redundancies in the parts of the proof that are trees. In this paper, we presentthreemodifications to improve the algorithm such that the redundancies can be found in the parts of the proofs that are DAGs. The first modified algorithm covers greater number of redundancies as compared to the known algorithm without incurring any additional cost. The second modified algorithm covers even greater number of the redundancies but it may have longer run times. Our third modified algorithm is parametrized and can trade off between run times and the coverage of the redundancies. We have implemented our algorithms in OpenSMT and applied them on unsatisfiability proofs of 198 examples from plain MUS track of SAT11 competition. The first and second algorithm additionally remove 0.89% and 10.57% of clauses respectively as compared to the original algorithm. For certain value of the parameter, the third algorithm removes almost as many clauses as the second algorithm but is significantly faster.
登录
查看更多内容
用于验证重放的数据压缩
DOI：
--
发表时间：
2008
期刊：
Journal of automated reasoning
影响因子：
--
作者：
Hasan Amjad
通讯作者：
Hasan Amjad
通过公共子证明提取来压缩命题证明
DOI：
--
发表时间：
2007
期刊：
International Conference/Workshop on Computer Aided Systems Theory
影响因子：
--
作者：
C. Sinz
通讯作者：
C. Sinz
DOI：
10.1017/s0890060403171065
发表时间：
2003-02
期刊：
Artificial Intelligence for Engineering Design, Analysis and Manufacturing
影响因子：
--
作者：
C. Sinz;Andreas Kaiser;W. Küchlin
通讯作者：
C. Sinz;Andreas Kaiser;W. Küchlin
大锤：审判日
DOI：
10.1007/978-3-642-14203-1_9
发表时间：
2010
期刊：
Proceedings of the 2015 Conference on Certified Programs and Proofs
影响因子：
--
作者：
S. Böhme;T. Nipkow
通讯作者：
T. Nipkow
DOI：
--
发表时间：
2007
期刊：
International Workshop Automated Verification Critical Systems
影响因子：
--
作者：
Hasan Amjad
通讯作者：
Hasan Amjad