文件名称：cdcl-sat-solver:用Java实现的CDCL SAT求解器
文件大小：2.01MB
文件格式：ZIP
更新时间：2024-06-06 14:43:40
Java
cdcl-sat-solver 用于大学课程的用Java实现的CDCL SAT求解器。 先决条件 Java 8 测试用例 样本测试用例 文件夹inputs中提供了一些示例CNF公式。 生成新的测试用例 在src/com/kentnek/cdcl/FormulaHelper.java运行main()方法。 生成的CNF公式将被写入inputs/generated文件夹。 运行求解器 使用所需测试用例的路径更新src/com/kentnek/cdcl/Main.java中的INPUT_FILE_PATH常量的值。 运行main()方法。 如果公式是可满足的，则求解器将输出一个分配并进行验证。 如果公式不满足要求，则求解器将生成反驳证明，对其进行验证并将其写入proofs文件夹中的输出文件。 作者 肯特·阮（ Kent Nguyen） -初期工作- 执照 此项目已获得MIT许可证的许可-
【文件预览】：
cdcl-sat-solver-master
----src()
--------com()
----inputs()
--------others()
--------simple()
--------generated()
----reports()
--------Stage 1 Report.pdf(948KB)
--------Stage 2 Report.pdf(993KB)
----LICENSE.md(1KB)
----README.md(1KB)
----.gitignore(26B)
----proofs()
--------unsat_simple_N3.txt(262B)
--------unsat_simple_N6.txt(242B)
--------unsat_simple_N2.txt(128B)
--------N20_K3_L100_unsat.txt(2KB)
--------unsat_simple_N2_prop.txt(107B)
--------N50_K3_L300_unsat.txt(6KB)