【文件属性】：
文件名称：drat-trim:DRAT修剪证明检查器
文件大小：6.96MB
文件格式：ZIP
更新时间：2021-04-24 00:04:33
C
DRAT格式和DRAT修剪检查器
证明检查器DRAT-trim可用于检查DIMACS格式的命题公式是否不令人满意。 给定一个命题公式和一个从句证明，DRAT-trim验证该证明是该公式不满足的证明。 条款证明应采用DRAT格式，用于验证SAT比赛的结果。 格式定义如下。
DRAT格式和相应的检查器DRAT-trim是基于以下目标而设计的：1）应该容易发出子句证明，以确保许多SAT求解器将支持它。 2）证明应紧凑，以减少编写证明的开销并确保可以存储证明； 3）证明验证应该是有效的； 和4）最先进的SAT解算器中使用的所有技术都应以以下格式表示。 关于最后一点，当前最先进的SAT求解器中使用的几种技术无法使用分辨率表示。 因此，DRAT格式是扩展分辨率的概括。
简而言之，从句证明的每个步骤都是子句的添加或删除。 每个子句添加步骤应保留可满足性，该可满足性应在多项式时间内计算。 多项式时间检
【文件预览】：
drat-trim-master
----compress.c(5KB)
----decompress.c(3KB)
----README.md(13KB)
----examples()
--------uuf-100-4.cnf(5KB)
--------example-5-vars.lrat(176B)
--------uuf-100-2.drat(11KB)
--------example-5-vars.cnf(103B)
--------R_4_4_18.clrat.bz2(4.19MB)
--------uuf-50-3.lrat(4KB)
--------uuf-100-2.lrat(27KB)
--------uuf-100-3.cnf(5KB)
--------uuf-30-1.cnf(1KB)
--------uuf-50-2.cnf(2KB)
--------uuf-100-5.drat(18KB)
--------uuf-30-1.lrat(1KB)
--------example-5-vars.drat(117B)
--------uuf-100-1.drat(17KB)
--------uuf-50-3.cnf(2KB)
--------uuf-100-4.drat(17KB)
--------uuf-30-1.drat(83B)
--------example-Schur.drup(72B)
--------R_4_4_18.cnf(148KB)
--------uuf-100-3.lrat(54KB)
--------example-4-vars.drat(78B)
--------uuf-50-2.lrat(5KB)
--------uuf-100-3.drat(21KB)
--------example-Schur.drat(32B)
--------example-4-vars.lrat(94B)
--------uuf-100-1.lrat(44KB)
--------uuf-100-5.cnf(5KB)
--------R_4_4_18.drat.bz2(2.65MB)
--------uuf-100-1.cnf(5KB)
--------uuf-50-3.drat(2KB)
--------uuf-100-5.lrat(46KB)
--------example-4-vars.cnf(106B)
--------uuf-50-2.drat(3KB)
--------example-Schur.cnf(486B)
--------uuf-100-4.lrat(43KB)
--------uuf-100-2.cnf(5KB)
----LICENSE(1KB)
----drat-trim.c(57KB)
----lrat-check.c(11KB)
----Makefile(335B)
----run-examples(666B)