Partition-Based
Logical Reasoning
Bill MacCartney (KSL), Sheila A. McIlraith (KSL),
Eyal Amir (FRG/Berkeley), Tomas Uribe (SRI)
Richard Fikes and John McCarthy
Knowledge Systems Lab | Formal Reasoning Group
Stanford University
with thanks to
Mark Stickel and Vinay Chaudhri of SRI
Motivation
• With large KBs, general-purpose reasoners
suffer from combinatorial explosion.
 Can we focus reasoning by decomposing the KB into a
network of minimally-connected partitions?
• Special-purpose reasoners can be highly efficient
in specific domains, but how to integrate them?
 Given a network of (possibly heterogeneous) knowledge systems,
how can we achieve efficient global reasoning?
• Can we exploit implicit structure of knowledge to
make reasoning more focused & efficient?
Bill MacCartney, Stanford KSL
11/14/02
Overview
• Algorithms and theoretical results
 Automatic partitioning of large KBs
 Reasoning with partitions using message passing (MP)
• Experimental testing
 Empirical validation of the effectiveness of partitioning
 Even better when combined with good local strategies
• Surprising, productive results
 Partitioning can induce near-optimal symbol orderings
 MP can integrate special-purpose reasoners
 Many new research questions
Bill MacCartney, Stanford KSL
11/14/02
Automatic partitioning
• Begin with a KB in PL or FOL
• Construct symbol graph

Edges join symbols which appear together in an axiom
• Apply tree decomposition algorithm


“Alg 5”: a variant of min-fill
“Alg 6”: a divide-and-conquer tree-width algorithm
• Partition axioms correspondingly


Each partition has its own vocabulary
“Link languages” are defined by shared vocabulary
Efficient reasoning depends on keeping
partition sizes and link sizes small
Bill MacCartney, Stanford KSL
11/14/02
Reasoning with partitions: an example
Query:
 U  V  Z theory
?
A simpleQpropositional
Partition 1
Theory
(1)
(2)
(3)
(4)
(12)
(16)
(17)
(18)
{Q R S T}
Q  R  T
S  T
S  R
SR
Q
R  T
ST
T
{{TT}}
Partition 2
(5)
(6)
(7)
(8)
(13)
(14)
(18)
(19)
(20)
(21)
{T U V W}
T  U  V  W
T  W
U  W
V  W
U
V
T
U  V  W
V  W
W
{{W
W}}
Partition
{Q R S3T U V{W X Y Z}
(9)
(10)
(11)
(15)
(21)
W  X  Z
XY
W  Y  Z
Z
W
(22) W  Y  Z
(23) W  Z
(24) Z
(25) 
Using partitioning, this query took just 10 resolution steps.
Using set-of-support, the same query can take 28 steps.
Bill MacCartney, Stanford KSL
11/14/02
Reasoning with partitions using MP
MP Algorithm
[Amir & McIlraith 2000]
• Start with a tree-structured
partition graph
• Identify goal partition
• Direct edges toward goal
(fixing outbound link language Li for each partition)
• Concurrently, in each partition:
 Generate consequences in Li
 Pass messages in Li toward goal
Bill MacCartney, Stanford KSL
11/14/02
Characteristics of MP
• Reasoning is performed locally
in each partition
• Relevant results propagate
toward goal partition
• Globally sound & complete
… provided each local reasoner is sound &
complete for Li-consequence finding
• Performance is worst-case
exponential within partitions,
but linear in tree structure
Bill MacCartney, Stanford KSL
Minimizes
between-partition
deduction
Focuses
within-partition
deduction
Supports parallel
processing
Different reasoners
in different partitions
11/14/02
Experimental Testing
• Do “real world” KBs exhibit inherent structure?
 Can we generate partitionings in which both partition sizes and
link language sizes are small?
 Can partition-based reasoning outperform other strategies?
• Experimental testbed
 Theorem prover: SNARK
– Thanks to Mark Stickel and SRI
 KB: Cyc
– A subset on spatial relationships, ~750 axioms, ~150 symbols
– We’re working on adding SUMO, Geo-Logica, RCC-8
 Queries
– Cyc queries provided by Vinay Chaudhri
Bill MacCartney, Stanford KSL
11/14/02
Results: automatic partitioning
• Partition graph is largely independent of query
 But edges may need to be redirected
• We’re experimenting with multiple algorithms
Alg 5
Alg 6
124
40
Max symbols/partition
16
19
Max symbols/link
14
17
Max axioms/partition
80
95
Max partitions/axiom
25
28
152
152
Number of partitions
Axioms in multiple partitions
Bill MacCartney, Stanford KSL
11/14/02
Testing MP
• “Vanilla” MP vs. common restriction strategies
 Use MP with no local strategy
 Compare to no strategy, ordered resolution, set-of-support
• “Smart” MP vs. set-of-support
 In SNARK testbed, we use MP + set-of-support
to approximate MP with smart local strategy
 Within-partition restriction strategies should do better
• Partition-derived symbol ordering
 Use partitioning to induce symbol ordering
 Compare partition-derived ordering with set-of-support
 What if we combine them?
Bill MacCartney, Stanford KSL
11/14/02
“Vanilla” MP vs. common strategies
Performance of MP and other common strategies
(relative to no strategy)
# of resolution steps, relative to no strategy
100%
90%
80%
q1
70%
q2
60%
q3
50%
q4
q5
40%
q6
30%
q7
20%
10%
0%
None
Bill MacCartney, Stanford KSL
Ordering
Set-of-support
MP (alg 5)
MP (alg 6)
11/14/02
“Smart” MP vs. set-of-support
Performance of MP and MP + SoS
(relative to no strategy)
# of resolution steps, relative to no strategy
100%
90%
80%
q1
70%
q2
60%
q3
50%
q4
q5
40%
q6
30%
q7
20%
10%
0%
SoS
Bill MacCartney, Stanford KSL
MP5
MP6
MP5 + SoS
MP6 + SoS
11/14/02
Partition-derived ordering (PDO)
Performance of partition-derived ordering
(relative to no strategy)
# of resolution steps, relative to no strategy
100%
90%
80%
q1
70%
q2
60%
q3
50%
q4
q5
40%
q6
30%
q7
20%
10%
0%
SoS
Bill MacCartney, Stanford KSL
PDO5
PDO6
PDO5 + SoS
PDO6 + SoS
11/14/02
MP and PDO vs. SoS
Performance of MP + SoS and PDO + SoS
# of resolution steps, relative to set-of-support
(relative to SoS)
100%
90%
80%
q1
70%
q2
60%
q3
50%
q4
q5
40%
q6
30%
q7
20%
10%
0%
SoS
Bill MacCartney, Stanford KSL
MP5 + SoS
MP6 + SoS
PDO5 + SoS
PDO6 + SoS
11/14/02
Ongoing research
• Testing on more KBs
• Partition-derived symbol orderings
 Can we beat hand-crafted symbol orderings?
• Within-partition restriction strategies
 Focus reasoning on Li-consequence finding
• Completeness results
 When is partitioning + set-of-support complete?
• Distributed implementations
 Demonstrate integration of heterogeneous reasoners
Bill MacCartney, Stanford KSL
11/14/02
Conclusions
• Partitioning can speed up reasoning
 Makes large KBs tractable by exploiting implicit structure
 Reasoning becomes significantly more focused and efficient
 Smarter local strategies should do even better
• Partition-derived ordering is surprisingly effective
 Especially when combined with set-of-support
 Automatic alternative to hand-crafted orderings
• Partitioning supports heterogeneous
local reasoners
 Efficient special-purpose reasoners can be cleanly integrated
 MP ensures global soundness & completeness
Bill MacCartney, Stanford KSL
11/14/02
References
Web
www.ksl.stanford.edu/projects/RKF/Partitioning/
Papers
• Amir, E. and McIlraith, S., “Partition-Based Logical Reasoning for First-Order
and Propositional Theories,” Artificial Intelligence journal, accepted for
publication.
• McIlraith, S. and Amir, E., “Theorem Proving with Structured Theories,” 17th
International Joint Conference on Artificial Intelligence (IJCAI-01), 2001.
• Amir, E., “Efficient Approximation for Triangulation of Minimum Treewidth,”
17th Conference on Uncertainty in Artificial Intelligence (UAI ’01), 2001.
• Amir, E. and McIlraith, S., “Solving Satisfiability using Decomposition and the
Most Constrained Subproblem.” Proceedings of SAT 2001, 2001.
• Amir, E. and McIlraith, S., “Partition-Based Logical Reasoning,” 7th International
Conference on Principles of Knowledge Representation and Reasoning (KR
’2000), 2000.
Bill MacCartney, Stanford KSL
11/14/02
The End
Bill MacCartney, Stanford KSL
11/14/02
Example
The espresso machine theory
(1)
(2)
(3)
(4)
(5)
(6)
(7)
(8)
(9)
(10)
(11)
ok-pump  on-pump  water
man-fill  water
man-fill  on-pump
man-fill  on-pump
water  ok-boiler  on-boiler  steam
water  steam
on-boiler  steam
ok-boiler  steam
steam  coffee  hot-drink
steam  tea  hot-drink
coffee  tea
Bill MacCartney, Stanford KSL
11/14/02
Example: partitioning
Step 1: construct symbol graph
(1)
(2)
(3)
(4)
(5)
(6)
(7)
(8)
(9)
(10)
(11)
ok-pump  on-pump  water
man-fill  water
man-fill  on-pump
man-fill  on-pump
water  ok-boiler  on-boiler  steam
water  steam
on-boiler  steam
ok-boiler  steam
steam  coffee  hot-drink
steam  tea  hot-drink
coffee  tea
man-fill
on-pump
water
ok-boiler
on-boiler
steam
coffee
hot-drink
Bill MacCartney, Stanford KSL
ok-pump
tea
11/14/02
Example: partitioning
Step 2: graph decomposition
man-fill
ok-pump
on-pump
ok-boiler
on-boiler
water
on-pump
water
ok-boiler
steam
on-boiler
steam
steam
coffee
Bill MacCartney, Stanford KSL
ok-pump
water
water
hot-drink
man-fill
tea
steam
coffee
hot-drink
tea
11/14/02
Example: partitioning
Step 3: generate partition graph
man-fill
ok-pump
water
on-pump
(1)
(2)
(3)
(4)
water
water
ok-boiler
steam
on-boiler
steam
steam
coffee
hot-drink
tea
Bill MacCartney, Stanford KSL
(5)
(6)
(7)
(8)
ok-pump  on-pump  water
man-fill  water
man-fill  on-pump
man-fill  on-pump
water
water  ok-boiler  on-boiler  steam
water  steam
on-boiler  steam
ok-boiler  steam
steam
(9) steam  coffee  hot-drink
(10) steam  tea  hot-drink
(11) coffee  tea
11/14/02
Example: add query to partition graph
Query: If the pump is OK and the boiler is OK and the
boiler is on, do we get a hot drink?
(1)
(2)
(3)
(4)
(5)
(6)
(7)
(8)
ok-pump  on-pump  water
man-fill  water
man-fill  on-pump
man-fill  on-pump
water
water  ok-boiler  on-boiler  steam
water  steam
on-boiler  steam
ok-boiler  steam
steam
(9) steam  coffee  hot-drink
(10) steam  tea  hot-drink
(11) coffee  tea
Bill MacCartney, Stanford KSL
(12) ok-pump
(13) ok-boiler
(14) on-boiler
(15) hot-drink
11/14/02
Example of MP
Using set-of-support, SNARK took 28 steps to prove this.
Using partitioning, SNARK took just 11 steps.
(1)
(2)
(3)
(4)
(5)
(6)
(7)
(8)
ok-pump  on-pump  water
man-fill  water
man-fill  on-pump
man-fill  on-pump
water
water  ok-boiler  on-boiler  steam
water  steam
on-boiler  steam
ok-boiler  steam
steam
(9) steam  coffee  hot-drink
(10) steam  tea  hot-drink
(11) coffee  tea
Bill MacCartney, Stanford KSL
(12)
(16)
(17)
(18)
ok-pump
on-pump  water
man-fill  water
water
(13)
(14)
(19)
(20)
ok-boiler
on-boiler
ok-boiler  on-boiler  steam
steam
(15)
(21)
(22)
(23)
hot-drink
steam  tea  hot-drink
steam  hot-drink
hot-drink
(24) 
11/14/02
Automatic partitioning
Bill MacCartney, Stanford KSL
11/14/02
Queries
hd-q1
If the pump is OK and the boiler is OK and the boiler is on, do we get a hot
drink?
cyc-p5
If A and B are inside C, can C be inside A?
cyc-p7
If A and B are part of C and C is at D, where is A?
cyc-p1
Suppose that A is touching B and B is inside C and C is at D. Is A at D?
cyc-v5
A has parts B, C, and D. B has parts E, and F. Is F near A?
cyc-p3
If C is between A and B, and both A and B are inside D, and D is at E, is C at
E?
cyc-p4
If C is between A and B, and both A and B are at D, is C also at D?
Bill MacCartney, Stanford KSL
11/14/02
Descargar

PBLR Presentation - Stanford University