支持SAT本地搜索的数据结构

Question

Walksat和GSAT 是众所周知且简单的本地搜索算法，用于解决布尔值的满意度问题。 GSAT算法的伪代码是从该问题中复制的 实施GSAT算法 - 如何选择要翻转哪个文字？ 并在下面介绍。

procedure GSAT(A,Max_Tries,Max_Flips)
  A: is a CNF formula
  for i:=1 to Max_Tries do
    S <- instantiation of variables
    for j:=1 to Max_Iter do
      if A satisfiable by S then
        return S
      endif
      V <- the variable whose flip yield the most important raise in the number of satisfied clauses;
      S <- S with V flipped;
    endfor
  endfor
  return the best instantiation found
end GSAT

在这里，我们翻转最大化满意子句数量的变量。这如何有效地完成？幼稚的方法是翻转每个变量，对于每个步骤，通过所有子句，并计算了其中有多少个子句。即使可以在恒定时间内查询一项条款，幼稚的方法仍将以$ O（vc）$时间运行，其中$ v $是变量的数量和$ c $条款的数量。我确定我们可以做得更好，因此问题：

许多本地搜索算法翻转变量的分配，以最大化满意子句的数量。实际上，该操作有效地支持了哪些数据结构？

这是我觉得教科书经常忽略的东西。一个例子是著名的 罗素和诺维格书.

Answer 1

所需的数据结构是 发生列表, ，每个变量包含条款的列表中发生的变量。这些列表是在CNF首次读取时构建一次。它们在下面的步骤3和5中使用，以避免扫描整个CNF公式以计算满足条款。

比翻转每个变量更好的算法是：

1. 仅列出不满意子句中发生的变量。
2. 从此列表中选择一个变量$ x $。
3. 计算满足包含$ x $的条款的数量。
4. 翻转$ x $。
5. 计算满足包含$ x $的条款的数量。
6. 解开$ x $。
7. 从步骤5中减去步骤3的结果，并以$ x $记录。
8. 在步骤1中发现的其余变量重复步骤2-7。
9. 在步骤7中以最高数字记录的变量翻转。

例如，数据结构的参考（通常也称为邻接列表） Lynce和Marques-Silva，回溯SAT Solvers的有效数据结构，2004年。