li-sat-solver:信息学逻辑课程的基本 SAT 求解器实现

SAT求解器 基于算法的 C++ 实现。 该求解器是课程的作业，旨在为我们提供 SAT 求解技术的基础知识。 目录 实现的功能 基准框架 结果 源代码和脚本 编译和执行求解器 请参阅结果和源代码以及脚本部分以了解项目结构的概述。 实现的功能 基于已经提供的代码，为了降低求解器的执行时间，已经实现了以下增强功能： 出现列表 BCP（Boolean Constraint Propagation）过程（在代码中称为propagateGivesConflict() ）不再遍历整个子句集。 相反，使用了几个额外的数据结构，以尽量减少每次传播文字时访问的子句数量。 这些数据结构称为出现列表，是一对列表，由变量索引。 这些列表中的每一项实际上都是另一个列表，其中包含变量作为正字面量或负字面量出现的子句。 因此，这些列表分别被命名为positiveClauses和negativeClauses 。