# Hardware Model Checking Algorithms and Techniques
## 2 Background and Notation
### Decision Problems
We distinguish YES-certificates, produced by the algorithm to certify a YES answer, and NO-certificates, produced by the algorithm to certify a NO answer._  
The typical decision problems we are interested in concern the satisfiability or validity of formulas in some logical system \(\mathcal{L}\). Those two problems are interchangeable, as deciding the satisfiability of a formula \(\varphi\) can be seen as the negation of the decision problem to determine whether the formula \(\
eg\varphi\) is valid. Focusing on the validity problem, we can formulate such a problem as the membership problem of a formula \(\varphi\) to the language of logically valid formulas of \(\mathcal{L}\) (or the language theorems, supposing \(\mathcal{L}\) to be sound and complete). In what follows, we assume \(\mathcal{L}\) to be both sound and complete. This is because we are mainly interested in decision problems over propositional logics, which are both sound and complete under the usual semantics and proof systems. Considering logical systems that are both sound and complete, we equate the problem of validity (checking whether a formula is a tautology in \(\mathcal{L}\)) to the problem of derivability (checking whether the formula is a theorem in \(\mathcal{L}\)). Proposition (or Boolean) Satisfiability (SAT) is the problem to decide whether a given propositional formula is satisfiable, as defined in Definition 16. **Definition 33** (Boolean Satisfiability Problem). : _Given a propositional formula \(\varphi\) over the propositional variables \(V\), SAT is the problem to determine whether \(\exists\mu(V):\mu=\varphi\). If that is the case, the formula \(\varphi\) is a Yes-instance of the problem and is said to be satisfiable (Sat). The model \(\mu\) is a Yes-certificate for the problem on \(\varphi\). Otherwise, the formula \(\varphi\) is a No-instance of the problem and is said to be unsatisfiable (Unsat)._  
SAT is a fundamental decision problem in computer science, important from both the theoretical and the practical perspective. From the theoretical standpoint, SAT plays a central role in computational complexity theory. From the practical standpoint, SAT can be used as a modeling framework to encode many computationally hard problems. SAT is known to be a computationally hard problem: it is, in fact, a member of the NP-complete class of complexity [24]. This briefly means that no algorithm is currently known that is able to solve all instances of SAT in a polynomial amount of time. Despite this theoretical limitation, the SAT problem is considered in many cases to be tractable, thanks to the fact that its instances often present some kind of structure arising from the application domain they originate from. Currently, state-of-the-art SAT solvers are able to handle SAT instances up to millions of variables and constraints. **Definition 34** (SAT-Solving Algorithm). : _A SAT-solving algorithm is a decision procedure to answer the SAT problem._  
A _SAT solver_ is software that runs a SAT-solving algorithm, taking a propositional formula (usually in CNF) as input and determining whether or not such a formula can be satisfied by a truth assignment of its variables. SAT-solving algorithms are usually designed as search procedures over the space of truth assignments, following the highly influential DPLL [25] algorithm. To give a better understanding of the subject at hand, Algorithm 1 highlights the top-level procedure of DPLL; a brief description follows as well as a partial example of the assignment's space exploration. Figure 1 depicts a search tree enumerating all the truth assignments, one for each leaf node, over three variables, taking into account \(CNF=\{\{\
eg x,y\},\{\
eg y,\
eg z\}\}\) as a target formula. Given the visual representation, it is easy to see how looking for a satisfying  
assignment is equal to looking for a path, and hence a leaf node, that satisfies a given CNF.