Information Technology Reference
In-Depth Information
(iv) Lines 5-6. A variable is selected according to the power-law distribution with the
parameter τ
(Equation 1). Its value is then flipped.
(v) Lines 7-8.
Sbest
is related to the current assignment with the minimum cost
(Equation 4). The current assignment is then updated.
(vi) Line 9. The optimization loop is executed for
MaxSteps
iterations.
(vii)Line 10. There is no guaranty that the algorithm finds a model to the problem if
one exists. τ-EO-SAT is incomplete.
4
-EO for ISAT
{
}
Let
V
=
x
,
2
x
,...,
x
be a set of Boolean variables and
ϕ
a set of clauses over a
1
P
subset of variables
X
⊆
V
.
ϕ
is found to be satisfiable and has a model
S
. Deter-
P
mine the satisfiability of
ϕ
∪
ϕ
for a given set of clauses
ϕ
over a subset of vari-
P
S
S
ables
X
′
⊆
V
. We use the same classification of clauses of
ϕ
∪
ϕ
as suggested in
P
S
[13] in order to perform minimum local changes on the model of
ϕ
. Let
X
be the
P
ϕ
set of variables that appear in the clauses of
. Let
ϕ
=
ϕ
∪
ϕ
and
ϕ
P
P
1
P
2
ϕ
=
ϕ
∪
ϕ
where :
S
S
1
S
2
{
}
{
}
′
(5)
ϕ
=
C
∈
ϕ
X
∩
X
≠
φ
and
ϕ
=
C
∈
ϕ
X
∩
X
≠
φ
′
P
1
i
P
C
ϕ
P
1
i
P
C
ϕ
i
P
1
i
S
ϕ
=
ϕ
−
ϕ
(6)
P
2
P
P
1
{
}
{
}
′
ϕ
=
C
∈
ϕ
X
∩
X
≠
φ
and
ϕ
=
C
∈
ϕ
X
∩
X
≠
φ
(7)
S
1
i
S
C
ϕ
′
S1
i
S
C
ϕ
i
S
1
i
P
ϕ
=
ϕ
−
ϕ
(8)
S
2
S
S
1
Let us make this point by presenting an example. Let
I
=
ϕ
∪
ϕ
be an ISAT in-
P
S
stance, where
{
}
ϕ
=
x
∨
x
,
x
∨
x
,
x
∨
x
∨
x
,
x
∨
x
,
x
∨
x
P
1
2
2
3
3
4
10
6
8
7
8
{
}
ϕ
=
x
∨
x
,
x
∨
x
,
x
∨
x
,
x
∨
x
∨
x
S
3
5
5
9
10
11
12
13
14
From Equation 5, we have
{
}
′
ϕ
=
x
∨
x
,
x
∨
x
∨
x
P
1
2
3
3
4
10
{
}
ϕ
=
x
∨
x
,
x
∨
x
,
x
∨
x
∨
x
P
1
1
2
2
3
3
4
10
and so from Equation 6, we have
{
}
=ϕ
In the same manner, from Equation 7 we have
x
∨
x
,
x
∨
x
P
2
6
8
7
8
Search WWH ::
Custom Search