drat trim:DRAT修剪证明检查器 源码

DRAT格式和DRAT修剪检查器 证明检查器DRAT-trim可用于检查DIMACS格式的命题公式是否不令人满意。 给定一个命题公式和一个从句证明,DRAT-trim验证该证明是该公式不满足的证明。 条款证明应采用DRAT格式,用于验证SAT比赛的结果。 格式定义如下。 DRAT格式和相应的检查器DRAT-trim是基于以下目标而设计的:1)应该容易发出子句证明,以确保许多SAT求解器将支持它。 2)证明应紧凑,以减少编写证明的开销并确保可以存储证明; 3)证明验证应该是有效的; 和4)最先进的SAT解算器中使用的所有技术都应以以下格式表示。 关于最后一点,当前最先进的SAT求解器中使用的几种技术无法使用分辨率表示。 因此,DRAT格式是扩展分辨率的概括。 简而言之,从句证明的每个步骤都是子句的添加或删除。 每个子句添加步骤应保留可满足性,该可满足性应在多项式时间内计算。 多项式时间检