第9章 预处理

简介

其他领域中的问题：自动编码生成SAT问题，再使用SAT求解器求解。

冗余：自动编码会产生冗余的变量或子句

预处理技术：消除冗余（重新编码），提高求解效率（推理）

内处理技术：对CDCL的生成子句应用预处理技术

冗余不一定是坏事：CDCL求解器一定程度上利用了冗余

• 基于解析及其变体
  • 单位传播
  • 有界变量消除
  • 超二元解析
  • 高级技术（蒸馏、活化）
• 冗余检测
  • 字句包含
  • 隐藏文字消除
  • 等价文字替换
  • 阻塞子句消除（及推广）

经典预处理技术

• 单位传播

• （前瞻）失败文字检测

• 纯文字检测

• 包含：包含

  • 正向包含（当前子句是否被其他子句包含）：将某个子句的所有变量全部临时赋值为假，使用单监视文字判断

  • 反向包含（当前子句是否包含其他子句）：维护每个文字在子句中的出现列表

  • 自包含解析：

• 连通块：超图(Hypergraph)：变量为顶点，子句为超边(Hyperedge)
  

基于解析的预处理

• 有界变量消除：对某个变量执行所有可以进行的解析，并删除所有带有该变量的子句。

  问题：子句数量增长速度为平方级

  • 选择正/负文字较少的变量
  • 结合重言式检测、包含检测等

• 等价文字替换：二元蕴含图中的强连通分量

  

  冲突检测：存在正文字到负文字的路径

• 超二元解析：单位传播的推广
  定义：

• 现代探测技术：

  非对称文字：若可以通过单位传播推出，则中的被称为非对称文字

  以上操作被称为非对称文字消除，但为了寻找冗余，考虑用这种方法添加文字

  非对称重言AT（隐藏重言消除HTE）：

反向单位传播RUP：会产生冲突

基本方法：将C中的文字设置为false再进行单位传播

活化(Distillation)：每当一个文字设置为false，进行一次单位传播

• C中如果有文字被设置为真，则该子句为非对称重言，删除或替换为学习子句
• C中如果有文字被设置为假，则该文字为非对称文字，可以删除该文字

蒸馏(Vivification)：使用trie减少冗余

可满足性等价的预处理

• 阻塞子句：子句C中某个文字的所有解析都为重言式

  没有阻塞C，阻塞C，删除C不影响可满足性。

  • 解析非对称重言RAT：子句C中的一个文字l的所有解析都为非对称重言式

• 覆盖文字：子句C中某个文字的所有解析中的非重言式 都包含某个文字k，则被称为覆盖文字

模型重建

在预处理（模型简化）的过程中，可能会消除部分变量（有界变量消除等）或删除部分子句（阻塞子句等）

需求：当最终判断SAT可满足时，需要反推到原始模型

方法：尝试-反转

可参考内处理论文

简单类

• 平凡可满足公式：每个公式至少有一个正/负文字
• Horn公式：每个公式至多有一个正文字
  • 证明：如果存在一个单位子句，进行赋值并单位传播，直到不存在单位子句。此时若产生空子句，则不满足；否则符合平凡可满足公式。
  • dual-Horn公式：每个公式至多有一个负文字
• 2-CNF公式：每个公式有且仅有两个文字
  • 方法1：转换为检测图上是否存在的路径
  • 方法2：随机游走
  • 方法3：解析，2-CNF解析仅能产生2-CNF，且2-CNF的总数为
• 仿射公式（XOR公式、奇偶校验）：转换为个子句
  • 高斯消元法