布尔约束传播BCP——文献学习CDCL Solver Additions: Local Look-Ahead,All-Unit-UIP Learning and On-the-Fly Probing(

Posted 2020-12-12 yuweng1689

文献名称  CDCL Solver Additions: Local Look-Ahead,All-Unit-UIP Learning and On-the-Fly Probing

 　　　　Norbert Manthey:CDCL Solver Additions: Local Look-Ahead, All-Unit-UIP Learning and On-the-Fly Probing. KI 2014: 98-110

---

 

Abstract

Many applications can be tackled with modern CDCL SAT solvers. However, most of todays CDCL solvers guide their search with a simple, but very fast to compute decision heuristic. In contrast to CDCL solvers, SAT solvers that are based on look-ahead procedures spend more time for decisions and with their local reasoning. This paper proposes three light-weight additions to the CDCL algorithm, local look-ahead, all-unit-UIP learning and on-the-fly-probing which allow the search to find unit clauses that are hard to find by unit propagation and clause learning alone. With the additional reasoning steps of these techniques the resulting algorithm is able to solve SAT formulas that cannot be solved by the original algorithm.

译文：基于预测程序的SAT求解器将花费更多的时间用于决策和本地推理。 译文：本文对CDCL算法进行了三种轻量级的改进，即局部提前查找、全单元uip学习和实时探测，使搜索能够找到单靠单元传播和子句学习难以找到的单元子句。

1 Introduction

 

 

3 Finding Backbone Literals on the Fly

 

3.3 Learning Multiple Unit Clauses

Modern SAT solvers learn a single clause when a conflict is obtained, usually by resolution according to the first-UIP scheme [28]. In case a unit clause C = x is learned, then all decision literals are removed from the current interpretation J, the unit clause (x) is added and then unit propagation is performed. As illustrated in the following example, the standard learning procedure might miss learning additional unit clauses which can be collected easily by a slight modification of the learning procedure. Given the formula and let J be the interpretation of the form J = abcdefgijlkm after the two decisions a and c. Then, the clause (j ∨ l ∨ m) is the empty clause under the interpretation J.

译文：现代SAT求解器在获得冲突时只学习单个子句，通常根据first-uip方案[28]进行求解。 译文：如下例所示，标准的学习过程可能会遗漏学习附加单元子句，而这些附加单元子句可以通过对学习过程稍加修改而轻松收集。