Information Technology Reference
In-Depth Information
Fig. 1.
Translation of a cyclic graph to a tree [3]
Algorithm 1 (Message Passing) [3]
1. Determine
≺
k
according to Definition 1.
2. Perform consequence finding in each
A
i
in parallel. If
A
k
|
=
Q
, then return YES.
3. For every
i,j
∈
V
such that
j
is the parent of
i
, if there is a consequence
ϕ
of the
partition
A
i
such that
ϕ
∈L
(
l
(
i,j
))
, then add
ϕ
to the axiom set
A
j
.
4. Repeat Steps 2 to 3 until no more new consequence is found.
Algorithm 1 works well for theorem proving at
A
k
when the induced graph is a tree.
However, if there is a cycle, we need to break it to transform the graph to a tree.
Algorithm 2 (Cycle Cut) [3]
1. Find a shortest cycle
v
1
,...,v
c
(=
v
1
)(
v
i
∈
V
)
in
G
. If there is no cycle, return
G
.
2. Select
a
such that
a<c
and
Σ
j<c,j
=
a
|
l
(
v
j
,v
j
+1
)
∪
l
(
v
a
,v
a
+1
)
|
is smallest.
3. For every
j<c
,
j
=
a
,let
l
(
v
j
,v
j
+1
):=
l
(
v
j
,v
j
+1
)
∪
l
(
v
a
,v
a
+1
)
.
4. Put
E
:=
E
\{
(
v
a
,v
a
+1
)
}
and
l
(
v
a
,v
a
+1
):=
∅
,thengotoStep1.
When there are multiple shortest cycles, common edges should be removed. But if there
is no common edge, edges are removed so that the sum of the sizes of communication
languages becomes the smallest. It is important to decide the order to remove edges al-
though any ordering results in a translation to a tree. Cycle Cut Algorithm 2 is designed
to minimize the total size of the communication languages.
Figure 1 shows an example of cycle cut. The left figure is translated to the right
figure. Firstly, the shortest cycle (1,3), (3,4), (4,1) is considered, and then the edge (4,1)
is deleted. The communication language of (4,1) is then added to those of (1,3) and
(3,4). Next, from the cycle (1,3), (3,2), (2,1), the edge (3,2) is removed, and
s
is added
to
l
(1
,
3)
and
l
(2
,
1)
. Then, the cycle (1,3), (3,4), (4,2), (2,1) is taken, and the edge (4,2)
is removed from it, but
s
is already in
l
(3
,
4)
and
l
(4
,
2)
. Now Algorithm 1 is applied;
¬
p
∨
s
is sent from
A
2
to
A
1
, deducing
q
∨
r
∨
s
(as the resolvent of
¬
p
∨
s
and
p
∨
q
∨
r
),
which is then sent from
A
1
to
A
3
, deducing
r
∨
s
(as the resolvent of
q
∨
r
∨
s
and
¬
q
∨
s
), which is sent from
A
3
to
A
4
. Finally, the conclusion
s
is obtained at
A
4
.
=
i≤n
A
i
and a formula
Theorem 1
.
[3]
Suppose an axiom set and its partitions
A
Q
n
)
. If the consequence finding procedure in each partition is sound
and complete, applying Algorithm 2 and then Algorithm 1 returns YES iff
∈L
(
A
k
)(
k
≤
A|
=
Q
.
