Inprocessing Rules

研究动机

预处理(Preprocessing)：搜索前公式化简

内处理(Inprocessing)：搜索中公式化简

问题：简化技术的混合使用从理论上很难保证正确（可满足等价/逻辑等价）

冗余概念

• 解析：​

• 重言：如果，那么​是重言式​

• 包含：如果，而且，那么​被包含

• 阻塞：如果，而且，有是重言式，那么被​​阻塞

  • 阻塞=解析重言

• 解析包含：如果，而且，有包含其他子句，那么在上解析包含

内处理规则框架

公式状态：：不冗余子句[学习子句]文字:子句对

• 学习(LEARN)：在前提条件X下，​
  • X：和​，可满足性等价（不是逻辑等价）
• 遗忘(FORGET)：
• 增强(STRENGTHEN)：
• 削弱(WEAKEN)：在前提条件Y下，​
  • Y：和​，可满足性等价（不是逻辑等价）

模型重建

基于RAT的内处理规则：

• 学习：在​中存在RAT
• 削弱：的在​​中存在RAT
  • ​

问题：的可满足赋值，不是的可满足赋值

解决方法：​中的变量进行调节

贡献与评价

主要贡献：

• 总结了内处理规则的框架
• 给出了证明
• 将现有的技术用该框架进行解释

个人评价：

• 新技术符合框架规则就可以对正确性的保证

总结

SAT问题是数学中的一个基础问题，而逻辑学、图论、计算机科学和运筹学等领域中的众多问题都可以转化为SAT问题。为了提高SAT求解器的性能，现代求解器往往会使用多种推理规则对子句进行化简。这些操作在求解过程前被称为预处理，在求解过程中被称为内处理。本文的作者认为混合使用多种化简技术可能存在求解过程不完整的问题，缺乏相关的理论支持。于是作者通过分析现有的技术，提取出其中的关键步骤，绘制出化简技术之间的关系图，随后提出了一个内处理规则框架，并且证明只要遵循该框架就可以保证求解过程的完整性。作者还将被广泛认可的求解技术套用到框架中以证明框架的合理性。我认为这个内处理框架能够为未来SAT求解器的设计提供指导性的帮助。