Relaxed_LCMDCBD可以复活输出drup文件的代码

标签：文件 LCMDCBD 输出 Relaxed file drup 代码

Relaxed_LCMDCBD是近期主流求解器。其中本身具有导出proof证明UNSAT的相应代码。可以按照以下步骤激活相应代码，求解的同时输出相应drup格式的文件。

---

复活输出drup文件输出的代码
1.在main.c文件头部设置
BoolOption drup 为 true
StringOption drup_file 为 自定义的固定文件名
2.在main.c文件中部将文件打开方式设置为文本
fopen(drup_file, "wb") 改为 fopen(drup_file, "w")
3.在solver.h文件中设置
带头部注释掉#define BIN_DRUP
4.在solver.c中查找BIN_DRUP和drup_file,了解输出情况：
几处化简函数函数体中注释掉了部分相关输出语句；
输出drup主要集中在以下函数体中：
(1) search
(2) removeClause
(3) addClause_
(4) simplifyLearnt_tier2 保留了一部分
(5) simplifyLearnt_core 保留了一部分
(6) solve_() 最后部 关于二进制输出有一句。
5. 说明-由于导出drup文件规模较大-不适合较难的样例求解输出

标签：文件,LCMDCBD,输出,Relaxed,file,drup,代码
From： https://www.cnblogs.com/yuweng1689/p/16651983.html