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 后,就会有三种情况:

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

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

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

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

导入的文字为零

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

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

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

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

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

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

  1. size = 0,说明该子句是空子句,直接标记 UNSAT,返回。
  2. 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() 的具体实现:

选出最具有代表性的两个文字,移动到前两个,这是因为这个移动是初步处理,最好只凭借前两个文字的赋值情况能体现整个语句的情况,并且选择的文字要满足后续变动更概率小的情况,因此采用以下策略选择变量:

  1. 未赋值变量是最好的。
  2. 真假相比,优先选赋值为真的文字。
  3. 如果都是假,优先选 level 大的。
  4. 如果都是真,优先选 level 小的。

那么排序的算法过程就可以描述了:

  1. 首先确定第一个位置的文字,将它与所有文字比较,比它更合适的将它代替。
  2. 步骤一结束后,第一个位置的文字如果是假,那么说明该子句不可满足,所以两个监听变量都应该是假,按照前面的步骤选出假中更好的。
  3. 如果第一个文字未赋值或者为真,那么子句应该是可满足的,这里第二个元素的确定,找个未赋值或者为真的都可以,它们两个的优先级是一样的。我猜测是因为这种情况是最常见的情况,这时候强行优先去找未赋值的会浪费太多时间,遇到为真的直接结束寻找就好。

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

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

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

  1. u=0, v<0,说明所有其他文字是假,所以 u 只能赋值为真。
  2. u=0, v>0,说明有一个未赋值的变量,但是子句已经满足了,此时 u 也可以进行赋值,并且赋值真或假都是合法的。
  3. 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 重启:

image.png

每次产生学习子句后,会调用 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 的情况更简单。

标签: none

仅有一条评论
添加新评论