Information Technology Reference
In-Depth Information
3.3
Partition-Based Consequence Finding
We here propose a new method to construct the communication language so that Mes-
sage Passing Algorithm can be made complete for consequence finding.
Suppose the whole axiom set and its partitions
=
i≤n
A
i
. Recall that the com-
A
mon language of
A
i
and
A
j
is
C
(
i,j
)=
S
(
A
i
)
∩
S
(
A
j
)(
i,j
≤
ni
=
j
)
. Here,
we construct the communication language
l
(
i,j
)
between
A
i
and
A
j
for consequence
finding by extending
C
(
i,j
)
.Let
P
=
be the given production field. By adding the
literals appearing in
L
to the common language, each communication language in the
case of trees is defined as
L
l
(
i,j
)=
C
(
i,j
)
∪ S
(
L
)
.
(3)
When there are cycles in the graph
G
, the final communication language is set after all
cycles are cut using Algorithm 2. For example, suppose that an edge
(
s, r
)
is removed
from a cycle. Then, the communication language of an edge
(
i,j
)(
=(
s, r
))
in the cycle
is defined in the same way as before:
l
(
i,j
)=
C
(
i,j
)
∪
l
(
s, r
)
∪
S
(
L
)
.
(4)
Two remarks are noted here. Firstly, in (3) and (4), the polarity of each literal in
L
from the production field
are lost within the symbols
S
(
L
)
. Although this does not
harm soundness and completeness of distributed consequence finding, there is some
redundancy in communication. Then, unlike the case of common language
C
(
i,j
)
,we
can keep the polarity of each literal in
L
in any
l
(
i,j
)
so that unnecessary clauses
possessing literals that do not belong to
P
P
are not communicated between partitions.
Second, when
C
(
i,j
)=
the edge
(
i,j
)
does not exist in the graph
G
. In this case,
l
(
i,j
)
need not be updated as
S
(
L
)
using (3) and actually the edge is kept unnecessary.
In fact, if we could add the literals from the production field to those non-existent edges
in
G
, then the resulting graph
G
would become strongly connected. By applying Cycle
Cut Algorithm 2 to
G
, the minimal way is to cut those added edges again. However,
other edges already have the literals
S
(
L
)
so their communication languages do not
change. Hence, we do not have to reconsider non-existent edges in
G
.
∅
Algorithm 3 (Partition-based Consequence Finding)
1. If there is a cycle in the induced graph
G
, select some
k
≤
n
and apply Cycle Cut
Algorithm 2 to
G
and transform it to a tree.
2. Determine the communication language between all pairs of partitions. For each
leaf partition
A
i
, do the following.
3. If
A
i
is the root partition, let
P
i
be the original production field
P
=
L
.Oth-
erwise, let
j
be the parent of
i
, and define the production field of
A
i
as
P
i
=
,where
l
(
i,j
)
±
is the set of literals constructed from
l
(
i,j
)
. Perform con-
sequence finding in
l
(
i,j
)
±
A
i
with the production field
P
i
,andlet
Cn
i
:=
Carc
(
A
i
,
P
i
)
.
Output each characteristic clause
C
∈
Cn
i
if
C
belongs to the original production
.
4. For each clause
C
field
P
=
L
∈
Cn
i
, check if
C
∈L
(
l
(
i,j
))
. If so, send
C
to
A
j
and let
)
.Put
i
:=
j
.
5. As long as there is a clause to be sent to the parent partition, repeat Steps 3 to 5.
A
j
:=
μ
(
A
j
∪{
C
}
