A long term goal motivating this project is the development of a universal computational engine to support reasoning across different applications of intelligent systems (e.g., planning and diagnosis). The project is founded on an approach that compiles knowledge bases into a taxonomy of tractable forms, which result from imposing various conditions, such as decomposability and determinism, on Negation Normal Form (NNF). Certain queries, which are generally intractable, become tractable on the compiled NNF forms. To implement a task like planning or diagnosis, all one needs to do is compile their knowledge base to the most succinct subset of NNF that provides polytime support for the queries required by the task. The project will focus in particular on algorithms for imposing various conditions on NNF compilations, using both top-down and bottom-up compilation techniques, to support a larger set of tractable forms. This will lead to developing and evaluating a more powerful inference engine than traditional SAT solvers, supported by a more comprehensive set of queries and transformations on knowledge bases. It will also lead to extending the compilation approach to a larger class of AI applications.
