Boolean quantification techniques with applications in formal verification: Algorithms and analysis

Quantification is a construct in mathematical logic that specifies the extent of validity of a predicate. This thesis considers the two fundamental types of quantification in Boolean logic, universal quantification and existential quantification. These two types of Boolean quantification exist in the problem formulations of many applications such as Electronic Design Automation (EDA) and Artificial Intelligence (AI). Boolean quantification problems mainly consist of two tasks: one is a decision problem that determines whether a Quantified Boolean Formula (QBF) is true or false; the other is to perform quantifier elimination that produces a quantifier free Boolean propositional formula given a Boolean formula with a subset of its variables quantified. Boolean quantification has been studied by many researchers and significant progress has been made in this area. Yet it is a hard problem and practical applications require continued success in this domain. This thesis mainly concerns various Boolean quantification techniques, with emphasis on their applications in EDA. This thesis investigates various aspects of Boolean quantification, including analysis and implementation of QBF solvers and using problem structural information to help both QBF evaluation and quantifier elimination computation.; A QBF solver is a software program to solve the QBF problem. The QBF problem determines whether a QBF is true or false. It is a generalization of the Boolean Satisfiability (SAT) problem. The SAT problem determines whether there exists a variable assignment that makes a Boolean propositional formula true. A Boolean propositional formula consists of Boolean propositions (statements that are true or false) connected by Boolean logic connectives such as "NOT" (¬), "AND" (∧) and "OR"' (∨). In a QBF, either an existential quantifier (∃) or a universal quantifier (∀) is applied to each variable of a Boolean propositional formula. A QBF is more expressive and more compact for problem representation than a Boolean propositional formula. The success of using SAT solvers for Boolean propositional formulas in many real-world applications has inspired research in developing efficient QBF solvers. However, existing QBF solvers are not efficient enough for practical applications.; This thesis provides a comparative study of algorithms for evaluating 2QBF, which is a special class of QBF in the sense that a 2QBF can be expressed using exactly one universal quantifier followed by exactly one existential quantifier. The 2QBF problem (NPNP-complete) is believed to be simpler to solve than general QBFs (PSPACE-complete). This study shows that it is worthwhile to consider solving 2QBFs as a distinct category from solving general QBFs since SAT techniques are easier to leverage in 2QBF solvers. Moreover, solving 2QBFs provides insight to solving QBFs in general. The experiments show that solvers based on different algorithms each have their own strengths and weaknesses.; Specifically, this thesis provides an analysis of the applicability of a class of widely used QBF algorithms, called search-based algorithms, for the sequential circuit state space diameter problem. The sequential circuit state space diameter problem is representative of a class of sequential verification problems. The analysis points out the inherent insufficiency of the search-based QBF algorithms for this problem and highlights the importance of exploring other non-search based QBF algorithms.; Certain application-specific knowledge may be helpful for improving the performance of QBF solvers. This thesis examines encoding of an important problem structural information, called the circuit observability don't care (ODC) information, in the QBF problem representation and exploiting this information during the DPLL-based QBF solving process. The DPLL procedure for QBF is probably the most important search-based procedure and is used as the basic framework for many QBF s...