The Partitioning and Reasoning Project
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. Realworld
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
taskspecific 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

E. Amir and S. McIlraith,
PartitionBased Logical Reasoning for FirstOrder and Propositional Theories,
Artificial Intelligence, 162 (12), pp. 4988, 2005.
(PDF,
PS)

B. MacCartney, S. McIlraith, E. Amir, and T. E. Uribe
Practical PartitionBased Theorem Proving for Large Knowledge Bases,
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 StructureBased 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,
PartitionBased 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 (maxflow software))
Implementation of approximation algorithms for tree decomposition
and treewidth. The software is used for partitioning of logical theories in
propositional and firstorder 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.710. It uses GNU C++ 2.95.3.
Precompiled versions available for the following platforms:

Partitioning V1.2 for SUN/Solaris 2.62.8 (6.4Mb compressed, approximately 38Mb untarred)

Executable Only (V1.2) for SUN/Solaris 2.62.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 untarred)

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 firstorder logical theory for SRI/Mark Stickel's Snark.
RELEVANT RESOURCES AND GROUPS

Kevin Murphy's
web site on
software packages for graphical models / bayesian networks

Dan Geiger's
research group.

Hans L. Bodlaender's
research group.

Uffe Kjærulff's
research 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
research group.

Adnan Darwiche's
research group.

Principles of Knowledge Representation and Reasoning, Inc..

Association for Uncertainty in AI.
Eyal Amir
Sheila A. McIlraith
Last updated on January 1, 2003.