Information Technology Reference
In-Depth Information
Only those
α
i
which are never dominated in this way are used to construct
new nodes in
T
.
Theorem 2.
The tree
T
constructed as above is a GE-tree for the full symmetry
group
G
.
Proof.
We start by showing that no two nodes of this tree are isomorphic under
G
.Let
M
and
N
be two distinct nodes, and suppose that there exists
g ∈ G
such that
. By assumption, we can write all elements of
G
as a product
of a value symmetry and a variable symmetry, so write
g
=
lr
where
l
is a value
symmetry and
r
is a variable symmetry. Suppose (without loss of generality, since
all group elements are invertible) that
Mg
=
N
M
is to the right of
N
in the search tree,
so that we will have found
N
first during search. Then the partial assignment
N
Nr
−
1
:=
is the image of
N
under an element of the variable group, and
contains the same variables as
M
. But this means that in our dominance check,
we will discover that
M
is dominated by an ancestor of
N
, contradicting the
construction of
T
.
Next we show that any full assignment corresponds to at least one leaf of
T
.
Let
be a full assignment, and let
X
1
be the variable at the root of
T
.Then
for some
α
1
∈
A
. Since the downedges from
the root are labelled with orbit representatives of
G
on Dom(
X
1
), there exists
β
1
∈
Dom(
X
1
) the literal (
X
1
=
α
1
)
∈A
Var
such that (
X
1
=
α
1
)
x
1
=(
X
1
=
β
1
)and
β
1
is
the label of a downedge from the root. Thus
Dom(
X
1
)and
x
1
∈ G
Ax
1
contains a node of the tree at
depth 1.
Suppose that
Ax
i
contains a node
N
ofthetreeatdepth
i
, and suppose that
the label at
N
is
X
i
+1
.Notethatsince
A
is a full assignment, we must have
(
X
i
+1
=
α
i
+1
)
Dom(
X
i
+1
). We subdivide into two cases.
If there exists
β
i
+1
in the orbit of
α
i
+1
under
G
∈A
,forsome
α
i
+1
∈
Val
(
)
such that
β
i
+1
is the label
A
Val
(
A
)
of a downedge from
N
, then letting
x
i
+1
∈ G
map
α
i
+1
→ β
i
+1
we see that
Ax
i
x
i
+1
contains a node at depth
i
+1.
Suppose instead that this is not the case. Then some orbit representative
(
X
i
+1
=
Val
(
N
)
, has been selected
by the GE-tree technique but then rejected due to SBDD considerations. This
means that there is a node
β
i
+1
), in the orbit of (
X
i
+1
=
α
i
+1
) under
G
M
at depth
j ≤ i
+ 1, which is to the left of
N
in
T
,
and which dominates
N∪
(
X
i
+1
=
β
i
+1
). Hence there exists an element
g ∈ G
Var
such that (
N∪
(
X
i
+1
=
β
i
+1
))
g
contains
M
.Let
h ∈ G
(
N
)
map (
X
i
+1
=
α
i
+1
)
to (
X
i
+1
=
β
i
+1
). Then
Ax
i
hg
contains
M
. Either it is the case that there is a
node at depth
i
+1 below
M
which can be reached from
Ax
i
hg
using only value
M
to the left of
symmetries, or there exists a node
M
which dominates some
descendant of
Ax
i
hg
. Since this “mapping
to left” operation can only be carried out a finite number of times, at some stage
we must find a node of depth
i
+ 1 which is contained in an image of
M
that is contained in an image of
A
.
We note at this point that the tree
T
described in this theorem is
not
nec-
essarily minimal - the tree constructed by SBDD is not always minimal, so the
same applies to any hybrid technique involving SBDD.
Search WWH ::
Custom Search