# Hardware Model Checking Algorithms and Techniques
## 2 Background and Notation
### Decision Problems  
In Section 2.1, we have presented logic as a tool to formalize and reason about a world of interest, whereas in Section 2.5 we have provided some background knowledge about commonly used models for representing combinational and sequential hardware circuits. Our aim is to use the tool of logic, and in particular Propositional Logic, to provide a formal representation of hardware sequential systems and reason about some of their properties. In particular, we are interested in asking certain questions about the formalized systems and having those questions answered by algorithmic procedures. We are, thus, interested in solving some computational problems arising from those questions, which typically belong to the class of _decision problems_. In this section we provide an overview of decision problems and their properties and we present Boolean Satisfiability (SAT), a fundamental decision problem in computer science of particular interest in the context of this paper. **Definition 28** (Decision Problems and Instances). : _A decision problem \(\mathcal{P}\) is any arbitrary question admitting a YES or NO answer over an infinite set of inputs. An instance of a decision problem \(\mathcal{P}\) is a particular input for \(\mathcal{P}\). We distinguish between Yes-instances, instances for which \(\mathcal{P}\) gives a Yes answer, and No-instances, instances for which \(\mathcal{P}\) gives a No answer._  
Traditionally, a decision problem is identified by its set of Yes-instances. Instances of a decision problem are usually encoded as strings over an alphabet \(\Sigma\). As a consequence, a decision problem \(\mathcal{P}\) is often defined as a _formal language_\(\mathcal{L}(\mathcal{P})\) over that alphabet and can be formulated as an instance of the _membership problem_ for \(\mathcal{L}(\mathcal{P})\). **Theorem 1** (Decision Problems as Membership Problems). : _Given a decision problem \(\mathcal{P}\), determining whether the answer to a given instance is Yes is equivalent to determining whether an encoding \(w\in\Sigma^{*}\) of that instance over an alphabet \(\Sigma\) is in the corresponding language \(\mathcal{L}(\mathcal{P})\)._  
In order to solve a decision problem \(\mathcal{P}\), we are interested in algorithms that terminate with a correct answer for every input of \(\mathcal{P}\), as formalized by the following definitions. **Definition 29** (Soundness and Completeness of an Algorithm). : _An algorithm for a given decision problem \(\mathcal{P}\) is sound iff when it returns a YES answer the input is a YES-instance of \(\mathcal{P}\). An algorithm for a given decision problem \(\mathcal{P}\) is complete iff it always terminates and it returns a YES answer when the input is a YES-instance of \(\mathcal{P}\)._  
Unsound algorithms are rarely of practical interest. Incomplete algorithms may be effective in solving only Yes- or No-instances of a decision problem. Ideally, however, we would like to have an algorithm for a decision problem \(\mathcal{P}\) that is both sound and complete. **Definition 30** (Decision Procedure). : _A decision procedure is an algorithmic procedure that, given an instance of a decision problem \(\mathcal{P}\), always terminates with a correct Yes or No answer._  
**Definition 31** (Decidability of a Decision Problem). : _A decision problem for which there exists a decision procedure is said to be decidable._  
Decidability is an important property to determine whether a given problem may be tackled algorithmically. Many important problems are undecidable, such as the so-called _Entscheidungsproblem_ asking for the validity of a first-order formula in the general case (proved undecidable by [PERSON] and [PERSON]). Sometimes, decision procedures are also asked to produce certificates as a way to prove that the results of their computation are correct. **Definition 32** (Certificates). : _A certificate is a string of symbols that can be used to prove the answer of a decision procedure on a given instance.