The Partitioning and Reasoning Project

Investigators

Eyal Amir,
Sheila A. McIlraith, together with

Bill MacCartney,
Tomas Uribe

This work is supported by DARPA grant N66001-97-C-8554-P00004 (Richard Fikes PI), NAVY grant N66001-00-C-8027 (Richard Fikes PI), AFOSR grant AFF49620-97-1-0207 (John McCarthy PI) and by DARPA grant N66001-00-C-8018 (RKF program) (John McCarthy PI, through a subcontract to SRI).
Some of this work is done in collaboration and coordination with Mark Stickel and Vinay Chaudhri from SRI.

AUTOMATIC DECOMPOSITION

The problem of partitioning knowledge and reasoning with it efficiently after it is decomposed is central to theoretical and practical computer science. One important decomposition problem is that of finding tree decompositions (equivalently, triangulations or variable ordering) of minimum treewidth for graphs. Real-world problems in artificial intelligence, VLSI design and databases are efficiently solvable if we have an efficient approximation algorithm for tree decomposition.

The automatic partitioning project is concerned with automatically finding triangulations and tree decompositions that are close to optimal (theoretically or experimentally) and are efficient enough to use for large problems (thousands to millions of nodes). It is also concerned with the development of new optimization criteria together with new reasoning techniques and new methods for decomposing graphs along these criteria.

REASONING WITH PARTITIONS OF LOGICAL KNOWLEDGE

There is growing interest in building large knowledge bases (KBs) of everyday knowledge about the world, teamed with theorem provers to perform inference. Such KBs comprise tens/hundreds of thousands of logical axioms. One approach to dealing with the size and complexity of these KBs is to structure the content in some way, such as into multiple domain- or task-specific KBs, or into microtheories.

In this project we investigate how to reason effectively with partitioned sets of logical axioms that have overlap in content, and that may even have different reasoning engines. More generally, we investigate the problem of how to exploit structure inherent in a set of logical axioms to induce a partitioning of the axioms that will improve the efficiency of reasoning.

PAPERS

B. MacCartney, S. McIlraith, E. Amir, and T. E. Uribe Practical Partition-Based Theorem Proving for Large Knowledge Bases, to appear in 18th Intl' Joint Conference on Artificial Intelligence (IJCAI'03), 2003.

S. McIlraith and E. Amir, Theorem proving with structured theories, 17th Intl' Joint Conference on Artificial Intelligence (IJCAI'01), 2001. Preliminary versions appeared in LICS workshop on Theory and Applications of Satisfiability Testing (SAT 2001) and Fifth Symposium on the logical formalization of commonsense reasoning.

E. Amir and S. McIlraith, Solving Satisfiability using Decomposition and the Most Constrained Subproblem, LICS workshop on Theory and Applications of Satisfiability Testing (SAT 2001), 2001. Proceedings of SAT 2001 appear in Electronic Notes in Discrete Mathematics (Elsevier Science). Also in IJCAI'01 workshop on Distributed Constraint Reasoning

Eyal Amir, Efficient Approximation for Triangulation of Minimum Treewidth, 17th Conference on Uncertainty in Artificial Intelligence (UAI '01), 2001.

E. Amir and S. McIlraith, Improving the Efficiency of Reasoning Through Structure-Based Reformulation, Proceedings of the 4th Intl' Symposium on Abstraction, Reformulation and Approximation (SARA'00), B.Y. Choueiry and T. Walsh Eds., Lecture Notes in Artificial Intelligence 1864. Springer.

E. Amir and S. McIlraith, Partition-Based Logical Reasoning, 7th International Conference on Principles of Knowledge Representation and Reasoning (KR'2000), 2000.

SOFTWARE

E. Amir, Partitioning Version 1.2, (README,COPYRIGHT,COPYRIGHT.PRF (max-flow software))
Implementation of approximation algorithms for tree decomposition and treewidth. The software is used for partitioning of logical theories in propositional and first-order logic and triangulation of Bayesian networks (assuming all variables are binary) and undirected graphs with no weights.
Platforms: Implementation compiles and runs successfully on Sun/Sparc/Solaris 2.6,2.7,2.8 (SunOS 5.6,5.7,5.8) and Linux KDE 2.4.7-10. It uses GNU C++ 2.95.3.
Precompiled versions available for the following platforms:

Partitioning V1.2 for SUN/Solaris 2.6-2.8 (6.4Mb compressed, approximately 38Mb un-tarred)

Executable Only (V1.2) for SUN/Solaris 2.6-2.8 (5.4Mb). Includes hMETIS, software from George Karypis, the University of Minnesota. Use of this software is subject to some conditions.

Partitioning V1.2 for Linux Redhat 7.2 (5.7Mb compressed, approximately 31Mb un-tarred)

Executable Only (V1.2) for Linux Redhat 7.2 (3.4Mb). Includes hMETIS, software from George Karypis, the University of Minnesota. Use of this software is subject to some conditions.

Acknowledgements:

Mike Stilman debugged and made some of the code of sp more efficient. He also wrote two of the programs in this package: "pto" and "otp".

Satish Kumar wrote the code for directing edges in response to a query (application "direct_edges") and "tp_split" which performs some of the pipeline involved in partitioning a first-order logical theory for SRI/Mark Stickel's Snark.