MiniSAT

Solver.h

• newVar 方法用于创建新的布尔变量，允许用户定义变量的极性和是否作为决策变量。
• addClause 方法用于向求解器添加不同形式的子句（如单位子句、二元子句、三元子句等）。
• solve 系列方法实现了不同的求解方式，可以传入假设条件，也可以不带任何假设地搜索解。
• value, modelValue 等方法可以用于获取当前求解过程中的变量和文字的状态。
• 提供 setConfBudget 和 setPropBudget 等方法用于设置求解器的冲突和传播预算，帮助控制资源消耗。
• 内部数据结构
  • clauses 和 learnts 分别存储问题的原始子句和学习到的子句。
  • trail 和 trail_lim 用于保存分配给文字的决策顺序，帮助在搜索中进行回溯。
  • activity 是用于启发式搜索的变量活动度，用于决定哪些变量将被优先选中。
  • order_heap 是一个优先队列，管理当前待决策变量的顺序。
• 求解器的几个核心功能
  • 子句附加和分离: attachClause 和 detachClause 实现了对子句的附加与删除。
  • 冲突分析: analyze 方法实现了冲突子句的回溯分析，计算出学习子句，并决定回溯的层次。
  • 启发式决策: pickBranchLit 方法选择下一个用于分支的变量。
  • 垃圾收集: garbageCollect 和 checkGarbage 方法用于管理内存，确保在必要时进行垃圾回收。

SolverType.h

• 变量和文字
  • Var 类型: 变量被定义为整数类型，表示从 0 开始的非负整数，并可用于数组索引。
  • Lit 结构体: 文字（Literal）用来表示一个变量及其极性（正或负）。文字通过一个整数来编码，正文字和负文字使用不同的整数值（变量编号 * 2 表示正文字，变量编号 * 2 + 1 表示负文字）。
  • 运算符重载: 提供了对文字的运算符重载，包括比较运算符（==, !=, <）、取反运算符（~）、和基于布尔值的异或运算符（^）。
  • 文字的创建: mkLit 函数用于通过变量编号和极性（正负）来创建一个文字。
• Lifted Booleans
  • lbool 类: 这是一个三值布尔类型（l_True, l_False, l_Undef），用于处理 SAT 问题中的未定义值情况。

  • 提供了布尔运算符（如逻辑与 && 和逻辑或

    ）的重载，实现了 lbool 类型的值操作。

• 子句
  • Clause 类: 子句是文字的一个集合，它在 SAT 问题中表示一个 CNF（合取范式）公式中的一个子句。
    • 数据布局: 子句数据结构中包含子句的文字、是否是学习子句、是否有附加数据等信息。还可以包含额外的活动度和抽象信息。
    • subsumes 方法: 用于检查当前子句是否能够吸取（subsumes）另一个子句，并可能简化它。
    • strengthen 方法: 通过删除一个文字来强化子句，并重新计算其抽象信息。
• 子句分配器
  • ClauseAllocator 类: 用于在内存中分配和管理子句。
    • alloc 函数根据传入的文字集合和是否是学习子句来分配子句的内存空间。
    • 还提供了内存移动、释放和重新定位的方法，用于动态管理子句在求解过程中内存的使用。
• OccLists 和 CMap
  • OccLists 模板类: 用于维护文字的发生列表，即跟踪一个文字在哪些子句中出现。这个数据结构可以进行懒惰删除，并包含清理脏数据的方法。
  • CMap 模板类: 用于将子句映射到某些值上，它封装了哈希映射（Map）的功能。