cdcl-sat-solver:用Java实现的CDCL SAT求解器-源码

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许可证的许可-