Reasoning with propositional knowledge: frameworks for boolean satisfiability and knowledge compilation

This dissertation is concerned with two fundamental problems that arise when reasoning about knowledge expressed in propositional logic. The first problem is the Boolean satisfiability problem, whereas the second problem is known as knowledge compilation. We introduce several frameworks for studying reasoning algorithms related to these problems. Based on the proposed frameworks, we derive practical algorithms for more efficient reasoning as well as theoretical results that shed light on the strengths and limitations of various reasoning approaches. In the case of Boolean satisfiability, we propose a framework that captures the essence of the state-of-the-art algorithm for solving this problem. Based on this framework, we answer an open question by precisely characterizing the inferential power of this algorithm. Even though this algorithm has traditionally been regarded as a combinatorial search algorithm, we are able to achieve this characterization using only the language of proof complexity. We then propose two practical techniques for improving the efficiency of the algorithm from this perspective. In the case of knowledge compilation, we propose a new propositional language that could provide compact representations of propositional knowledge. This language also serves as a framework that unifies many well-known languages, including the influential ordered binary decision diagram (OBDD). We then study the new language, as well as some of its distinguished restrictions, in terms of (i) useful reasoning operations it allows and (ii) its ability to represent propositional knowledge compactly. We also introduce a framework for characterizing the sizes of Boolean functions represented in this language. We derive lower and upper bounds that subsume existing bounds known for the size of OBDDs. We show that our bound results can be used to obtain interesting size bounds for various Boolean functions.