邻居变量：如果两个变量出现在同一个子句中，称他们是邻居。 变量x的格局：一个由x的所有邻居变量的赋值构成的向量。
格局检测用于SAT问题
中国科学院软件研究所
Institute of Software,Chinese Academy of Sciences
CC for SAT：对于一个变量v，如果从上次v改变赋值之后， v的格局没
用局部搜索求解以下MaxSAT（或SAT）实例 {x1 \/ ~x2, x1 \/ x2, x2 \/x3, ~x1 \/ x2 \/~x3}
赋值 初始 000 Step 1 001 Step 2 101 Step 3 110
不满足的子句 x1 \/ x2, x2 \/x3 x1 \/ x2 ~x1 \/ x2 \/~x3 无 （找到最优解）
有改变过，那么禁止v变回原来的赋值。
顶点覆盖问题
中国科学院软件研究所
Institute of Software,Chinese Academy of Sciences
顶点覆盖：对于一个无向图，一个顶点覆盖是一个顶点子集，使得每
条边都至少有一个点属于该集合。
最小顶点覆盖问题：给定一个无向图，找出最小的顶点覆盖。
局部搜索
中国科学院软件研究所
Institute of Software,Chinese Academy of Sciences
简单地说，局部搜索是：
先产生一个（或一群）完整的候选解，然后进行迭代改进，每一步只修改 解的某个局部（比如一个基本单元），直到得到一个令人满意的解或者达 到某个资源限制（一般是时间限制）。
格局检测（configuration checking，简称CC）的直观理解：
无法记忆整个解，但可以记忆每个解部件的环境及其变化。 通过检测解部件的环境，减少解的局部结构上的循环，以此减少整
