第5章 基于前瞻的SAT求解器

简介

应用场景

• 密度(density)：子句数量/变量数量
  • 单位传播的代价
  • 密度越大，子句数量多，惰性数据结构具有优势
• 直径(diameter)：，其中代表最短路径长度
  • 解析图：点（子句），边（子句之间能进行解析）
  • 局部性好，子句学习具有优势

前瞻(LookAhead)

启发

• 差异启发：前瞻变量的效果，选出
• 方向启发：决策变量的赋值选择，或
• 预选启发：前瞻变量的选择

差异启发(Diff)

差异基于：

：大小为k的子句的重要性

​​：大小为k的子句子集

• 子句约简启发(Clause Reduction Heuristic)

• 加权二元启发(Weight Binaries Heuristic)

  • 关注二元子句和能与之进行解析的子句数量

• 主干搜索启发(Backbone Search Heuristic)

• 主干搜索重规范化启发(Backbone Search Renormalized Heuristic)

混合差异(MIXDIFF)

​

方向启发

如果始终选择正确的赋值：无需回溯即可求解可满足的实例，P=NP

• 较少计算时间：较快遇到冲突（CDCL求解器中较多）
  • posit求解器：的短子句中正文字多，
• 较高可满足可能性
  • kcnfs求解器：中正文字多，
  • march求解器：，​
  • OKsolver求解器：选择较小值​
• 混合
  • march_ks求解器：若，正常决策；否则反向决策

预选启发

收益：减少计算开销；损失：无法选择有效的变量

• • 二元子句出现次数
  • 深度较浅时不执行预选
  • 至少预选10个变量

• 子句约简近似(Clause Reduction Approximation)

  • ​

局部学习

• 必要赋值：和的前瞻都对​产生相同的赋值
• 约束解析：不是通过二元+二元解析形成的子句
  • 除外都符合约束解析（实际中没有这么多）

自发(Autarkies)推理

目的：检测出可以直接赋值的变量，化简公式

• 纯文字：

• 差异启发中检测

  	2	2	1	2	2	0	1	2	1	0

• 自发推理：前瞻后仅有一个子句未被满足

  剩余：。（：；：）

  推理：和​

  • 前瞻的顺序会影响到DIFF启发的评分(WBH,BSH,CRA)

两次前瞻

条件：

• 两次前瞻推理

  第一次：

  第二次：第一次结果中所有自由变量，假设检测到失败文字

  推理：​

  • 两次前瞻会影响到DIFF启发的评分

急切数据结构（Eager Data-Structure）

目的：减少单位传播的成本

惰性数据结构不适合：无法快速得到约简后的新子句

• 二元蕴含数组

  

  • 子句被分为​
  • 单位传播时优先进行二元子句

• 移除不活跃子句

  • 已经满足的子句

  • 转化为二元子句

• 基于树的前瞻

  冗余：，前瞻被前瞻和前瞻所包含。

  

总结

• 基于启发的完备算法
  • 差异
  • 方向
  • 预选
• 局部子句学习
• 急切数据结构