Information Technology Reference
In-Depth Information
X
0
X
1
X
2
X
3
X
4
X
5
X
6
X
10
X
7
X
8
X
9
Fig. 2. Structure graph for decomposition
ζ
(eq. (2))
Proof.
By construction, an irreducible axiomdecomposition is tree-structured, so let
X
0
denote
the top-level literal. Assume the proposition to be false: Let
C
be a minimal conflict and
let the corresponding structure graph be disconnected, having two non-empty connectivity
components
C
1
and
C
2
(
C
=
C
1
∪
C
2
). Let
S
,
S
1
and
S
2
be standard forms of
B
,
C
1
and
C
2
,
respectively. Then, by (de Wolf & Nienhuys-Cheng, 1997, theorem 5.20), we have
B∪
|
=
⊥⇐⇒
∪
S
1
∪
⊥
C
S
S
2
.
r
By definition, this is the case if and only if
S
∪
S
1
∪
S
2
{
R
1
,
R
2
}
⊥
.
r
r
Since
C
is a minimal conflict,
C
2
. Hence, we cannot have
both
R
1
and
R
2
derivable from the same connectivity component, say
C
1
, for otherwise
B∪
C
1
is consistent as well as
B∪
∪
{
}
⊥
S
S
1
R
1
,
R
2
r
r
B∪
|
=
⊥
and therefore
by (de Wolf & Nienhuys-Cheng, 1997, theorem 4.39). This would
mean that
C
1
is a smaller conflict set than
C
, contradicting the minimality of
C
. So assume
without loss of generality that
C
1
S
∪
S
1
r
R
1
and
S
∪
S
2
r
R
2
.
(3)
By construction, there must be a sequence
R
1
,
R
2
,...,
R
n
R
1
with
R
i
S
1
or
R
i
a
≡
∈
S
∪
resolvent of
R
p
,
R
q
for
p
,
q
r
R
1
and there must be an
R
j
so
that a (leaf-)literal
L
1
in
S
1
occurs in
R
j
, as no set of interior literals can solely contribute to
the derivation of
R
1
. Hence we must have a path from
X
0
to
X
k
B
<
i
. Since
is consistent,
S
≡
L
1
by our assumptions
on the grammar and the method of construction, for otherwise
X
k
(and therefore
L
1
) would
not occur anywhere during the inference. The same argument applies for the derivation of
R
2
from
B∪
{
}
C
2
, so any inference giving
R
1
,
R
2
necessarily induces paths from
X
0
to the node
R
1
,
R
2
,...,
R
1
R
1
,
R
2
,...,
R
2
X
k
C
1
(without loss of generality), and
C
1
is not connected to
C
2
in the structure graph, so the pat
h
from
X
0
to
X
l
does not exist. This contradicts (3) and completes the proof.
≡
L
1
∈
lit
(
)
and from
X
0
to
X
l
≡
L
2
∈
lit
(
)
.Yet
X
0
∈
Based on the previous result, we can state an interesting criterion that permits further
minimizing conflict sets in terms of literals, even when they are already minimal in terms
of set inclusion.
Search WWH ::
Custom Search