文献阅读——Conflict-Driven Clause Learning SAT Solvers

One of the main reasons for the widespread use of SAT in many applications is that Conflict-Driven Clause Learning (CDCL) Boolean Satisfiability (SAT) solvers are so effective in practice. Since their inception in the mid-90s, CDCL SAT solvers have been applied, in many cases with remarkable success, to a number of practical applications. Examples of applications include hardware and software model checking, planning, equivalence checking, bioinformatics, hardware and software test pattern generation, software package dependencies, and cryptography.

This chapter surveys the organization of CDCL solvers, from the original solvers that inspired modern CDCL SAT solvers, to the most recent and proven techniques.

The organization of CDCL SAT solvers is primarily inspired by DPLL solvers. As a result, and even though the chapter is self-contained, a reasonable knowledge of the organization of DPLL is assumed.

In order to offer a detailed account of CDCL SAT solvers, a number of concepts have to be introduced, which serve to formalize the operations implemented by any DPLL SAT solver.译文：为了提供CDCL SAT求解器的详细描述，必须引入许多概念，这些概念用于形式化任何DPLL SAT求解器实现的操作

DPLL corresponds to backtrack search, where at each step a variable and a propositional value are selected for branching purposes. With each branching step, two values can be assigned to a variable, either 0 or 1. Branching corresponds to assigning the chosen value to the chosen variable.

Afterwards, the logical consequences of each branching step are evaluated. 译文：然后，评估每个分支步骤的逻辑结果。

Each time an unsatisfied clause (i.e. a conflict) is identified, backtracking is executed. Backtracking corresponds to undoing branching steps until an unflipped branch is reached. 译文：回溯对应于撤销分支步骤，直到到达未翻转的分支。

When both values have been assigned to the selected variable at a branching step, backtracking will undo this branching step.

If for the first branching step both values have been considered, and backtracking undoes this first branching step, then the CNF formula can be declared unsatisfiable. 译文：如果在第一个分支步骤中考虑了两个值，并且回溯撤消了第一个分支步骤，那么CNF公式可以声明为不可满足。

This kind of backtracking is called chronological backtracking. An alternative backtracking scheme is non-chronological backtracking, which is described later in this chapter. A more detailed description of the DPLL algorithm is given in Part 1, Chapter 3.

Besides using DPLL, building a state-of-the-art CDCL SAT solver involves a number of additional key techniques:

• Learning new clauses from conflicts during backtrack search [MSS96].

• Exploiting structure of conflicts during clause learning [MSS96].

• Using lazy data structures for the representation of formulas [MMZ+01].

• Branching heuristics must have low computational overhead, and must receive feedback from backtrack search [MMZ+01]. 译文：分支启发式算法必须具有较低的计算开销，并且必须从回溯搜索接收反馈

• Periodically restarting backtrack search [GSK98].

• Additional techniques include deletion policies for learnt clauses [GN02], the actual implementation of lazy data structures [Rya04], the organization of unit propagation [LSB05], among others.