# Hardware Model Checking Algorithms and Techniques
## 2 Background and Notation
### Decision Problems
Furthermore, taking into account the tree topology and the leaf values, it is possible to identify simplifying steps that reduce the search space, e.g., neither \(\mu_{3}\) nor \(\mu_{4}\) can lead to satisfying assignments; thus, it is irrelevant to evaluate the role of variable \(z\) given a partial assignment that reaches such a branch. In order to evaluate the amount of work that the DPLL algorithm has to perform, a common notion used is that of the _termination tree_, which evaluates the actual search tree considered during exploration. Figure 2 depicts a partial termination tree taking into account the same example introduced in Figure 1. Within a termination tree, one can find conflicts (\(\boldsymbol{\mathcal{A}}\)) and valid (\(\boldsymbol{\mathcal{V}}\)) assignments, as well as a trace for the conditioned CNF at each level of the search space. Most modern state-of-the-art SAT solvers employs a SAT-solving algorithm called _Conflict-Driven Clause Learning_ (CDCL) [26]. CDCL is based on _clause learning_ and _non-chronological backtracking_ in order to avoid repeated exploration of regions of the search space that do not lead to a satisfying assignment. During search, CDCL algorithms maintain a _trail_ of literals representing the current partial assignment. Under a given partial assignment, each clause loaded in the solver can be either _satisfied, conflicts, units_ or _unresolved_. Clauses are satisfied if at least one of their literals is satisfied. If each literal in a clause is falsified, then the whole clause is a conflict. If all but one literals of the clause are falsified, then the clause is a unit. Otherwise the clause is unresolved. If a clause is a unit, its only non-falsified  
Figure 1: Search tree enumerating all possible assignments for three variables \(x\), \(y\) and \(z\) with respect to \(CNF=\{\{-x,y\},\{-y,-z\}\}\). Solid (dashed) edges correspond to _true_ (_false_) assignments. Figure 2: Partial termination tree associated with the example of Figure 1 where each node is labeled with the corresponding CNF. Crosses denote contradiction within a given path whereas check marks denote admissible assignments. literal is implied by the current partial assignment; thus, its variable can be assigned so that the literal is satisfied. ```
0:\(C\) a set of clauses. 0:\(res\in\{\textsc{Sat},\textsc{Unsat}\}\). 1:procedureDPLL(\(C\))
2:while\(\exists\) unit clause \(l\in C\)do
3:\(C\leftarrow\textsc{UnitPropagate}(C,l)\)
4:while\(\exists\) pure literal \(l\in C\)do
5:\(C\leftarrow\textsc{PureLiteralAssign}(C,l)\)
6:if\(C=\emptyset\)then
7:returnSat
8:ifempty clause \(\in C\)then
9:returnUnsat
10:\(l\leftarrow\textsc{ChooseLiteral}(C)\)
11:returnDPLL(\(C\cup l\)) or DPLL(\(C\cup\
eg l\))
```  
**Algorithm 1** Top-level procedure of the DPLL algorithm. The search starts by selecting a variable, using some suitable heuristic, and assigning it a truth value. This process is called _decision_. After a decision has been made, some of the clauses loaded in the solver may have become conflicts or unit clauses. The solver looks up for unit clauses using efficient data structures, called _watch lists_, in order to perform _Boolean Constraint Propagation_ (BCP). During BCP, the solver finds and assigns every clause that is a unit under the current partial assignment. Such a procedure iterates until either no more unit clauses can be found or the solver has found a conflict. In the first case, the solver proceeds with the next decision. In the second case, the solver analyzes the sequence of assignments that have led to the conflict, a process called _conflict analysis_[26]. The result of such an analysis is a _learned clause_ catching the causes of the conflict. Such a clause is added to the current formula in order to avoid future iterations to enter the region of the search space that led to the conflict (_learning_). The algorithm, thus, performs non-chronological backtracking canceling enough of its latest decisions (even all of them) to leave such a region of space and then resume search on another region.