Joao Marques-Silva, Ines Lynce and Sharad Malik
| 4.1. Introduction | |
|
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. |
|
| The chapter is organized as follows. The next section introduces the notation used throughout the chapter. Afterwards, Section 4.3 summarizes the organization of modern CDCL SAT solvers. Section 4.4 details conflict analysis, the procedure used for learning new clauses. Section 4.5 outlines more recent techniques that have been shown to be effective in practice. The chapter concludes in Section 4.6 by providing a historical perspective of the work on CDCL SAT solvers. | |
| 4.3. Organization of CDCL Solvers | |
| 4.5.3. Conflict-Driven Branching Heuristics | |
| The early branching heuristics made use of all the information available from the data structures, namely the number of satisfied/unsatisfied and unassigned literals. These heuristics are updated during the search and also take into account the clauses that are learnt. An overview on such heuristics is provided in [MS99]. | |
| More recently, a different kind of variable selection heuristic (referred to as VSIDS, Variable State Independent Decaying Sum) has been proposed by Chaff authors [MMZ+01]. One of the reasons for proposing this new heuristic was the introduction of lazy data structures, where the knowledge of the dynamic size of a clause is not accurate. Hence, the heuristics described above cannot be used. | |
| VSIDS selects the literal that appears most frequently over all the clauses, which means that one counter is required for each one of the literals. Initially, all counters are set to zero. During the search, the metrics only have to be updated when a new recorded clause is created. More than to develop an accurate heuristic, the motivation has been to design a fast (but dynamically adapting) heuristic. In fact, one of the key properties of this strategy is the very low overhead, due to being independent of the variable state. | |
| Two Chaff-like SAT solvers, BerkMin [GN02] and siege [Rya04], have improved the VSIDS heuristic. BerkMin also measures clauses’ age and activity for deciding the next branching variable, whereas siege gives priority to assigning variables on recently recorded clauses. | |