KISSAT 源码分析

kissat_assign_reference

多元子句的赋值，需要调用的函数。

void
kissat_assign_reference (kissat * solver,
             unsigned lit, reference ref, clause * reason)
{
  assert (reason == kissat_dereference_clause (solver, ref));
  assigned *assigned = solver->assigned;
  value *values = solver->values;
  const unsigned level =
    kissat_assignment_level (solver, values, assigned, lit, reason);
  assert (level <= solver->level);
  assert (ref != DECISION_REASON);
  assert (ref != UNIT_REASON);
  kissat_assign (solver, solver->probing, level, false, false, lit, ref);
  LOGREF (ref, "assign %s reason", LOGLIT (lit));
}

kissat_add 添加变量

kissat_add 是一个处理子句和文字的函数，用于添加文字和子句到求解器内部数据结构。

其中涉及到的步骤非常多，大体过程描述如下：

导入的文字非零

这时候就是导入一个子句的一个文字，需要缓存起来。

调用 kissat_import_literal，将外部文字 elit 转换为内部文字 ilit

然后检查这个变量是否已经定了值[了]()，比如前面有该文字的单元子句出现就会出现这个情况。

kissat_fixed 函数的定义是，若该变量是顶层 level，并且已经被赋值，则返回被赋的值，否则返回 0。也就是函数名称意义上的(如果有的情况下)返回定(fixed)值。

调用 kissat_fixed 的拿到返回值 value 后，就会有三种情况：

value > 0，这时候说明该文字已经为真，并且是顶层传播为真，该子句在任何情况下恒为真，是不需要考虑的，此时标记 solver->clause_satisfied = true，在后续的过程中该子句不需要考虑。
value < 0，这时候说明该文字恒为假，那么这个文字在这个子句中是没有意义的，所以要把这个文字删了，目的是增快后面对数据结构操作的效率。标记 solver->clause_shrink 为 true，代表需要收缩子句。
value = 0，这个是最常见的情况[，]()即插入的文字是普通文字，没什么特殊性质，这时候直接插入到子句里面就好了。

除了最直观的几种情况，还有一些其他情况可以优化：

一个文字和它的负文字同时出现在一个子句，那么该子句需要判定恒真，可以直接删掉。
如果一个文字在子句中出现多次（虽然不符合 CNF 文件格式规范），那么保留一个就好。

解决的办法就是定义一个 mark 数组，标记子句的正负出现是否出现过，实现起来就比较简单了。

导入的文字为零

这时候说明子句读入完成，我们就需要把子句作为一个整体进行各种处理了。

第一步如果有一下情形之一的，直接跳过处理，该子句没有意义：

前面导入的子句出现了矛盾，这时候后面的子句全都不处理了，包括当前子句。solver->inconsistent
该子句已经有了恒真文字，该子句也不需要处理。solver->clause_satisfied
该子句有正负文字同时出现，solver->clause_trivial

否则的话，就开始对子句进行初步的处理，正确加载进所有数据结构[。]()

首先调用 kissat_activate_literals，激活所有变量。该函数做了几方面的事，将变量加入全局变量表，然后赋予初始评分，加入堆中，该函数连续调用 kissat_mark_removed_literal 把所有变量标记为可以删除的，和 kissat_mark_added_literal 把所有变量标记为纳入计算。

接下来是对于各种 size 的子句的特殊处理：

size = 0，说明该子句是空子句，直接标记 UNSAT，返回。
size = 1，说明该子句是单元子句，调用 kissat_original_unit 为其直接赋值，然后开始单元传播 kissat_search_propagate。

最普通的情况就是 size > 1，说明该子句是需要进行监听单元传播赋值了，需要把两个变量载入 watch 监听表里。

首先调用 kissat_new_original_clause 创建一个 reference 类型编号（实际上就是 unsigned int），代表该子句的编号。在这个函数中会对文字进行一个排序（kissat_sort_literals sort.c）

sort.c - kissat_sort_literals() 的具体实现：
选出最具有代表性的两个文字，移动到前两个，这是因为这个移动是初步处理，最好只凭借前两个文字的赋值情况能体现整个语句的情况，并且选择的文字要满足后续变动更概率小的情况，因此采用以下策略选择变量：
未赋值变量是最好的。
真假相比，优先选赋值为真的文字。
如果都是假，优先选 level 大的。
如果都是真，优先选 level 小的。
那么排序的算法过程就可以描述了：
首先确定第一个位置的文字，将它与所有文字比较，比它更合适的将它代替。
步骤一结束后，第一个位置的文字如果是假，那么说明该子句不可满足，所以两个监听变量都应该是假，按照前面的步骤选出假中更好的。
如果第一个文字未赋值或者为真，那么子句应该是可满足的，这里第二个元素的确定，找个未赋值或者为真的都可以，它们两个的优先级是一样的。我猜测是因为这种情况是最常见的情况，这时候强行优先去找未赋值的会浪费太多时间，遇到为真的直接结束寻找就好。

排序的过程走完，我们找到两个最具有代表性的变量，通过对它们的分析，就可以得到子句的状态。

这时候调用 new_clause 函数，将子句移动到数据结构中，并且根据 size 添加好对应形式的监听。

在某些情况下，子句是有可能进行赋值的：

u=0, v<0，说明所有其他文字是假，所以 u 只能赋值为真。
u=0, v>0，说明有一个未赋值的变量，但是子句已经满足了，此时 u 也可以进行赋值，并且赋值真或假都是合法的。
u<0, v<0，说明所有文字全部为假，也需要考虑重新赋值。

除此之外还有冲突需要回跳的情况，需要调用 kissat_backtrack_without_updating_phases 就不详细看了。

单元传播的实现

核心函数是 proplit.h 中的 search_propagate_literal

核心算法如下：

找到某个文字的所有监听器，挨个遍历
如果是二元子句，单独处理。如果另一个文字 blocking 是 false，那就冲突了，进行冲突分析。如果另一个文字未赋值，直接调用赋值函数进行赋值。
如果是非二元子句，考察记录的另一个文字 other，如果 other > 0，那么 continue。否则就搜索子句找到一个 >=0 的文字作为新的 other，找到之后与 other 交换。如果找不到并且当前 other 是负的，那就遇到冲突了。除此之外的情况就是 other=0，这时候对 other 赋值 = 1。

加快找到未赋值变量的方法：记录一个 searched 变量，优先往后搜，找不到了再往前搜。
增强程序局部性的方法：修改 watch 的时候调用带 delay 的函数，等单元传播所有修改都确定之后，统一修改 watch 结构的数据

冲突分析

kissat 代码实现不太好，并且没有啥优化的空间，以后有需要再看。

最终分析完调用 kissat_learn_clause(solver) 进行学习子句的处理。

分析完，把涉及的分析变量调用 kissat_bump_analyzed 对变量进行打分，增加这些变量的权重。

然后还会调用 kissat_update_target_and_best_phases，对 phase 的赋值进行操作。

变量分支

decide 分支的时候有两种模式 stable 和 focus。
前者使用 VSIDS 对变量进行评分，后者是 VMTF，即优先队列，每次把冲突涉及的变量移动到队首。

stable mode

冲突分析之后会把所有分析过的变量存到 solver->analyzed 中，然后会调用 kissat_bump_analyzed 对变量进行打分，最终会调用 bump_analyzed_variable_scores 进行打分。

计算方式为 new_score = old_score + inc。

其中 inc 为 solver->scinc，是一个预定义的常量。

如果评分溢出，就会调用 rescale_scores 进行等比例缩放。

具体过程是：

记录 solver->scint 为评分的分母，最终的评分需要除这个分母。
找到最大评分和 solver->scint 中最大的，分子分母全部除以这个值。

每一轮都需要削弱旧变量的评分，具体实现过程在 bump_score_increment ，大致过程如下：

系统存在一个给定的 decay 常量，将该常量 * 1e-3。
将分母乘上 1.0 / （1.0 - decay），可以将分母变大，这样起到了等比削弱所有变量评分的作用。

focus mode

这个模式下采用 VMTF(Variables Move To Front) 方法。

将所有未赋值变量插到队列里，调用 move_analyzed_variables_to_front_of_queue 把上一轮分析的变量提到最前。

变量决策

根据 VSIDS 或者 VMTF 可以找到一个决策变量，但是为这个决策变量赋值为真还是假，还需要更多的处理。

主要的过程在 decide.c 中的 decide_phase 函数中：

如果处在 forcephase 模式，直接赋值为 0
否则检查 target 数组，有的话返回对应的赋值
如果 target 数组没有赋值，那么返回 saved 数组的值
如果都没有赋值，返回 INITIAL_PHASE，默认为 1

rephase 重新改变赋值倾向

有关对 target 和 saved 的赋值，需要用到很多技术。

冲突分析后进行回跳的时候，在 stable 模式下，会调用 kissat_update_target_and_best_phases。

这个函数会比较当前 level 的已赋值变量数是不是历史最多，如果是的话，那就把当前的赋值情况，全部赋给 target 和 saved。

除了在冲突分析的时候进行 rephase，求解器还会额外按一定的间隔，一定方式重置 rephase 的数据。

间隔取决于 solver->limits.rephase.conflicts，一旦冲突达到限制，那么就会 rephase。

重置 rephase 有几种方式：

best: 将 best 赋值给 saved
walk: 如果 local search 的解有提升则赋值为本次 local search 的解，否则赋值为 best。
original: 将默认相位 INITIAL_PHASE 赋值给 saved。
inverted: 将默认的相反相位赋值 INITIAL_PHASE 赋值给 saved
random: 将 saved 赋值为随机的一组赋值
flipped: 反转当前的 saved 赋值

实现方式是取模，找到当前选中的方式，然后通过函数指针调用具体的方法。

static char (*rephase_schedule[]) (kissat *) = {
  rephase_best, rephase_walking, rephase_inverted,
  rephase_best, rephase_walking, rephase_original,
};
const uint64_t count = GET (rephased);
const uint64_t select = (count - 1) % (uint64_t) size_rephase_schedule;
const char type = rephase_schedule[select] (solver);

reduce 删减子句

首先调用 collect_reducibles() ，扫描可以删除的子句。

然后调用 mark_less_useful_clauses_as_garbage , 修改对应 Clause c->garbage 的属性，按照定义的参数，修改对应的数据结构删除。

restart 重启

stable 模式下，采用 luby 重启：

每次产生学习子句后，会调用 kissat_tick_reluctant ，即完成一次，由该函数计数，然后将 reluctant->trigger 设置为 true。

下一次判断是否重启的时候，就会触发重启操作了。

focus 模式下，采用 glucose 重启，记录最近的学习子句的 LBD 的加权平均，和历史所有子句的 LBD 加权平均。

smooth.c 里面定义了对 LBD 加权赋值的操作，能够让数值更加平滑。

如果 fast >= margin * slow，触发重启条件。

const double fast = AVERAGE (fast_glue);
const double slow = AVERAGE (slow_glue);
const double margin = (100.0 + GET_OPTION (restartmargin)) / 100.0;
const double limit = margin * slow;
LOG ("restart glue limit %g = %.02f * %g (slow glue) %c %g (fast glue)",
     limit, margin, slow,
     (limit > fast ? '>' : limit == fast ? '=' : '<'), fast);
return (limit <= fast);

触发重启后的过程大概如下：

调用 kissat_update_target_and_best_phases，把当前的赋值存到 target 和 best 当中。

然后调用 kissat_backtrack_without_updating_phases ，开始 backtrack，修改所有相关的数据结构和数组，直接回到 0 层。

重用 trail

这部分技术在最新版的 kissat 中已经被删除了，不太知道原因是什么。

重用的过程主要是回跳不一定直接回跳到顶层，进行一个搜索树的复用，stable 模式的大概过程如下：

找到目前评分最高的变量，记录它的评分。
遍历 trail，找到第一个比它评分小的，就直接回跳到该变量的上一级 level，这样评分比它大的变量都会保留，那么之前搜索的高评分变量赋值可以一定程度的复用。
记录上一个在 trail 遇到的 DECISION_REASON 变量，如果当前变量评分大于上一个，那也结束，直接跳到该变量上一级的 level。如果当前变量前一个 DECISION_REASON 直接 DECIDE 赋值的变量评分比它低，那么这个搜索树从上个 DECISTION 变量到后面这部分的意义就不是很大，这些层的数据就都不要了。

focus 模式的过程是类似的，比这个 VSIDS 的情况更简单。

YuhangQ

最近回复

其它