| abstract: | 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 lights on the strengths and
limitations of various reasoning approaches.
In the case of Boolean satisfiability, we propose a framework that
captures the essences 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 size lower and upper bounds that subsume
existing bounds known for OBDD. We show that our bound results can
be used to obtain interesting size bounds for various Boolean
functions. |