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许可证的许可-
2021-11-05 20:22:19
2.01MB
Java
1