Computational Properties of Binary Decision Diagrams

The subject of the research proposal is Binary Decision Diagrams (BDDs). This concept has attracted widespread interest that independently arose both in theory of computation and in practical work related to the verification of hardware. Various kinds of BDDs (e.g. Ordered BDD) are widely used in the design and verification of hard-ware digital circuits for information processing, control and computing systems. In theory, BDDs are intensively investigated as a computational model that provides a theoretical measure for the memory of real-life computers. The goal of the research project is investigation of several problems that arose due to interaction between applied and theoretical computer science and whose solution could lead to the design of effective (randomized) algorithms or at least to a better understanding of computational feasibility. More specifically, we plan to work in the following directions. 1. Obtain better inapproximability results for the Ordered BDD minimization. Identify classes of boolean functions for which effective approximations exist. 2. Precisely determine the worst case running time of any implementation of the Davis-Putnam algorithm for Satisfiability (or, equivalently, the efficiency of the tree-like resolution method in automated theorem proving). 3. Classify the complexity of the monotone dualization problem.