The Partitioning and Reasoning Project
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
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.
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
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),
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
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.
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.
RELEVANT RESOURCES AND GROUPS
web site on
software packages for graphical models / bayesian networks
Hans L. Bodlaender's
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".
Network Optimization Library
theorem prover SNARK
DARPA's RKF and
Principles of Knowledge Representation and Reasoning, Inc..
Association for Uncertainty in AI.
Sheila A. McIlraith
Last updated on November 9, 2001.