The Partitioning and Reasoning Project


  • 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.


    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.


    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.


    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.  [new]
    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.


    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.

    Kevin Murphy's web site on software packages for graphical models / bayesian networks
    Dan Geiger's reserach group.
    Hans L. Bodlaender's reserach group.
    Uffe Kjśrulff's reserach group.
    A compendium of NP optimization problems
    METIS: Serial graph/mesh partitioning & sparse matrix ordering package for VLSI, finite element methods, linear programming and other problems.
    An experimental comparison of flow algorithms
    Graphviz, a graph visualization software including the programs "dot" and "dotty".
    Andrew Goldberg's Network Optimization Library
    Mark Stickel's theorem prover SNARK
    Cycorp's CYC.
    DARPA's RKF and HPKB programs.
    Rina Dechter's reserach group.
    Adnan Darwiche's reserach group.
    Principles of Knowledge Representation and Reasoning, Inc..
    Association for Uncertainty in AI.

    Eyal Amir Sheila A. McIlraith Last updated on November 9, 2001.