I
nte
rna
t
io
na
l J
o
urna
l o
f
E
lect
rica
l a
nd
Co
m
pu
t
er
E
ng
ineering
(
I
J
E
CE
)
Vo
l.
15
,
No
.
3
,
J
u
n
e
20
25
,
p
p
.
3191
~
3
2
0
1
I
SS
N:
2088
-
8
7
0
8
,
DOI
: 1
0
.
1
1
5
9
1
/ijece.
v
15
i
3
.
pp
3
1
9
1
-
3
2
0
1
3191
J
o
ur
na
l ho
m
ep
a
g
e
:
h
ttp
:
//ij
ec
e.
ia
esco
r
e.
co
m
Applica
tion o
f
sa
t
isfia
bility pro
ble
m so
lv
ers for as
se
ss
ing
t
he
streng
th
o
f
has
h a
lg
o
rithms
K
un
bo
la
t
Alg
a
zy
,
K
a
ira
t
Sa
k
a
n,
Andrey
Va
re
nn
ik
o
v
,
Nursu
l
u K
a
pa
lo
v
a
I
n
f
o
r
mat
i
o
n
S
e
c
u
r
i
t
y
L
a
b
o
r
a
t
o
r
y
,
I
n
st
i
t
u
t
e
o
f
I
n
f
o
r
ma
t
i
o
n
a
n
d
C
o
m
p
u
t
a
t
i
o
n
a
l
Te
c
h
n
o
l
o
g
i
e
s,
A
l
ma
t
y
,
R
e
p
u
b
l
i
c
o
f
K
a
z
a
k
h
s
t
a
n
Art
icle
I
nfo
AB
S
T
RAC
T
A
r
ticle
his
to
r
y:
R
ec
eiv
ed
J
u
n
1
1
,
2
0
2
4
R
ev
is
ed
Dec
1
7
,
2
0
2
4
Acc
ep
ted
J
an
1
6
,
2
0
2
5
Th
is
a
rti
c
le
p
re
se
n
ts
a
m
e
th
o
d
o
lo
g
y
f
o
r
a
ss
e
ss
in
g
th
e
st
re
n
g
th
o
f
c
ry
p
to
g
ra
p
h
ic
a
lg
o
rit
h
m
s
a
n
d
p
ro
v
i
d
e
s
e
x
p
e
rime
n
tal
d
a
ta
o
b
tai
n
e
d
fr
o
m
stu
d
y
in
g
t
h
e
c
r
y
p
t
o
g
ra
p
h
ic
str
e
n
g
th
o
f
t
h
e
d
e
v
e
lo
p
e
d
h
a
sh
fu
n
c
ti
o
n
HBC
-
2
5
6
u
sin
g
m
o
d
e
rn
sa
ti
sfia
b
il
it
y
p
r
o
b
lem
(S
AT)
so
l
v
e
rs.
Va
r
io
u
s
S
AT
so
lv
e
rs
imp
lem
e
n
ti
n
g
t
h
e
c
o
n
fli
c
t
-
d
riv
e
n
c
lau
se
lea
rn
in
g
(CDCL)
a
lg
o
rit
h
m
,
b
a
se
d
o
n
th
e
D
a
v
is
-
P
u
t
n
a
m
-
L
o
g
e
m
a
n
n
-
L
o
v
e
lan
d
(DPL
L)
a
lg
o
rit
h
m
,
we
re
u
se
d
t
o
c
o
n
d
u
c
t
t
h
e
c
ry
p
tan
a
ly
sis
o
f
th
e
HBC
-
2
5
6
h
a
sh
fu
n
c
ti
o
n
.
Th
e
m
o
st
e
ffe
c
ti
v
e
wa
s
th
e
p
a
ra
ll
e
l
S
AT
so
lv
e
r
P
a
r
k
issa
t,
a
n
d
th
u
s
it
wa
s
u
se
d
f
o
r
m
o
re
in
-
d
e
p
t
h
re
se
a
rc
h
.
A
se
ries
o
f
e
x
p
e
rime
n
ts
we
re
c
o
n
d
u
c
ted
t
o
d
e
term
in
e
h
o
w
re
sista
n
t
t
h
e
HBC
-
2
5
6
h
a
sh
i
n
g
a
l
g
o
rit
h
m
is
to
p
re
ima
g
e
a
tt
a
c
k
s
fo
r
o
n
e
,
tw
o
,
th
re
e
,
a
n
d
fo
u
r
ro
u
n
d
s.
F
o
r
th
is
p
u
r
p
o
se
,
f
o
u
r
se
ts
o
f
fil
e
s
we
re
p
re
p
a
re
d
u
sin
g
sp
e
c
i
a
l
p
ro
p
o
siti
o
n
a
l
e
n
c
o
d
in
g
to
o
ls,
e
a
c
h
se
t
in
c
lu
d
in
g
3
0
fi
les
in
t
h
e
sta
n
d
a
rd
o
f
c
e
n
ter
fo
r
d
isc
re
te
m
a
th
e
m
a
ti
c
s
a
n
d
th
e
o
re
ti
c
a
l
c
o
m
p
u
ter
sc
ien
c
e
s
(DIM
ACS)
fo
rm
a
t.
Th
e
se
fil
e
s
c
o
n
tain
Bo
o
lea
n
f
o
rm
u
las
i
n
c
o
n
ju
n
c
ti
v
e
n
o
rm
a
l
fo
rm
(CNF)
,
u
se
d
a
s
in
p
u
t
f
o
r
m
o
d
e
rn
S
AT
so
l
v
e
rs.
T
o
o
b
tain
m
o
re
a
c
c
u
ra
te
ti
m
e
m
e
a
su
re
m
e
n
ts,
th
e
sa
m
e
e
x
p
e
rime
n
t
wa
s
re
p
e
a
ted
m
u
lt
ip
l
e
ti
m
e
s,
a
fter
wh
ich
th
e
a
v
e
ra
g
e
ti
m
e
wa
s
d
e
term
in
e
d
.
Th
e
re
su
lt
s
o
f
th
is
stu
d
y
sh
o
w
t
h
a
t
S
AT
so
lv
e
rs
e
n
c
o
u
n
ter
sig
n
ifi
c
a
n
t
d
iff
icu
lt
ies
w
h
e
n
a
t
tem
p
ti
n
g
to
so
l
v
e
t
h
e
p
re
ima
g
e
se
a
rc
h
p
ro
b
lem
fo
r
t
h
e
fu
l
l
-
ro
u
n
d
v
e
rsio
n
o
f
th
e
HBC
-
2
5
6
h
a
sh
f
u
n
c
ti
o
n
,
e
v
e
n
wh
e
n
o
n
l
y
3
0
b
it
s
o
f
th
e
o
ri
g
in
a
l
m
e
ss
a
g
e
a
re
u
n
k
n
o
wn
.
K
ey
w
o
r
d
s
:
B
o
o
lean
f
o
r
m
u
las
C
r
y
p
tan
aly
s
is
Hash
f
u
n
ctio
n
Pro
p
o
s
itio
n
al
en
co
d
in
g
Satis
f
iab
ilit
y
p
r
o
b
lem
T
h
is i
s
a
n
o
p
e
n
a
c
c
e
ss
a
rticle
u
n
d
e
r th
e
CC B
Y
-
SA
li
c
e
n
se
.
C
o
r
r
e
s
p
o
nd
ing
A
uth
o
r
:
Kair
at
Sak
an
I
n
f
o
r
m
atio
n
Secu
r
ity
L
ab
o
r
ato
r
y
,
I
n
s
titu
te
o
f
I
n
f
o
r
m
atio
n
an
d
C
o
m
p
u
tatio
n
al
T
ec
h
n
o
l
o
g
ie
s
2
8
Sh
ev
ch
e
n
k
o
,
Alm
aty
,
0
5
0
0
1
0
,
R
ep
u
b
lic
o
f
Kaz
ak
h
s
tan
E
m
ail:
1
9
k
air
at7
8
@
g
m
ail.
co
m
1.
I
NT
RO
D
UCT
I
O
N
E
n
s
u
r
in
g
co
m
p
u
ter
s
ec
u
r
ity
i
n
lar
g
e
o
p
en
n
etwo
r
k
s
s
u
ch
a
s
th
e
in
ter
n
et
is
o
n
e
o
f
t
h
e
m
o
s
t
p
r
ess
in
g
ar
ea
s
o
f
m
o
d
e
r
n
in
f
o
r
m
atics.
Ho
wev
er
,
p
r
o
v
id
in
g
s
ec
u
r
ity
is
a
ch
alle
n
g
in
g
task
as
it
in
v
o
lv
es
a
d
d
r
ess
in
g
n
u
m
er
o
u
s
tech
n
ical
is
s
u
es
to
g
u
ar
an
tee
th
e
h
i
g
h
est
p
o
s
s
ib
le
lev
el
o
f
r
eliab
ilit
y
to
m
ee
t
th
e
n
ee
d
s
o
f
r
eg
u
lar
u
s
er
s
.
T
h
ese
is
s
u
es
n
ec
ess
itat
e
th
e
u
s
e
o
f
s
p
ec
if
ic
p
r
o
to
co
ls
to
en
s
u
r
e
s
ec
u
r
e
d
ata
ex
c
h
an
g
e
a
n
d
m
o
d
er
n
cr
y
p
to
g
r
ap
h
ic
m
eth
o
d
s
.
E
v
en
wh
en
a
p
r
o
to
co
l
h
as
a
f
o
r
m
al
p
r
o
o
f
o
f
s
ec
u
r
ity
,
it
ca
n
s
till
b
e
co
m
p
r
o
m
is
ed
if
th
e
cr
y
p
to
g
r
ap
h
ic
alg
o
r
ith
m
u
s
ed
f
o
r
its
im
p
lem
en
tatio
n
p
o
s
s
ess
e
s
u
n
d
esira
b
le
alg
eb
r
aic
p
r
o
p
er
ties
.
T
h
u
s
,
o
n
e
o
f
th
e
ess
en
tial
s
tep
s
in
cr
ea
tin
g
a
cr
y
p
to
g
r
ap
h
ic
s
ch
em
e,
alg
o
r
ith
m
,
o
r
p
r
o
to
c
o
l
is
co
n
d
u
ctin
g
a
n
in
itial
cr
y
p
tan
aly
s
is
to
ass
ess
th
e
s
tr
e
n
g
th
o
f
th
e
p
r
o
p
o
s
ed
s
ch
em
e.
Mo
d
er
n
m
eth
o
d
s
s
u
cc
ess
f
u
lly
ap
p
lied
to
th
e
an
aly
s
is
o
f
cr
y
p
to
g
r
a
p
h
ic
alg
o
r
ith
m
s
,
s
u
ch
as
lin
ea
r
cr
y
p
tan
aly
s
is
o
r
d
if
f
er
en
tial
c
r
y
p
tan
aly
s
is
,
r
ely
s
o
lely
o
n
s
tatis
tical
to
o
ls
.
An
o
th
er
a
p
p
r
o
ac
h
f
o
r
an
aly
zin
g
cr
y
p
to
g
r
ap
h
ic
alg
o
r
ith
m
s
to
o
b
tain
m
o
r
e
r
eliab
le
s
ec
u
r
ity
g
u
ar
an
tees
is
p
r
o
p
o
s
itio
n
al
en
c
o
d
in
g
f
o
llo
wed
b
y
th
e
ap
p
licatio
n
o
f
s
atis
f
iab
ilit
y
(
SAT)
s
o
lv
er
s
[
1
]
.
Ma
n
y
p
r
ac
tically
s
ig
n
if
ican
t
p
r
o
b
lem
s
r
elate
d
to
Evaluation Warning : The document was created with Spire.PDF for Python.
I
SS
N
:
2
0
8
8
-
8
7
0
8
I
n
t J E
lec
&
C
o
m
p
E
n
g
,
Vo
l.
15
,
No
.
3
,
J
u
n
e
20
25
:
3
1
9
1
-
3
2
0
1
3192
in
f
o
r
m
atio
n
m
an
a
g
em
en
t
an
d
p
r
o
ce
s
s
in
g
in
d
is
cr
ete
s
y
s
tem
s
ca
n
b
e
ef
f
ec
tiv
ely
r
ed
u
ce
d
to
th
e
s
atis
f
iab
ilit
y
p
r
o
b
lem
s
o
f
B
o
o
lean
f
o
r
m
u
la
s
.
T
h
is
ap
p
lies
t
o
p
r
o
b
lem
s
o
f
s
y
n
th
esis
an
d
v
er
if
icatio
n
i
n
m
icr
o
elec
tr
o
n
ics,
s
o
m
e
th
eo
r
etica
l
p
r
o
g
r
am
m
in
g
is
s
u
es,
in
v
er
s
io
n
p
r
o
b
l
em
s
o
f
d
is
cr
ete
f
u
n
ctio
n
s
,
m
an
ag
em
e
n
t
o
f
co
m
m
u
n
icatio
n
p
r
o
to
co
ls
,
an
d
m
an
y
o
th
er
s
.
A
B
o
o
lean
f
o
r
m
u
la
o
f
v
ar
ia
b
les
is
an
ex
p
r
ess
io
n
c
o
n
s
tr
u
ct
ed
ac
co
r
d
in
g
to
s
p
ec
if
ic
r
u
les
o
v
er
an
alp
h
ab
et
th
at
in
clu
d
es
B
o
o
le
an
v
ar
iab
les
1
,
.
.
.
,
,
p
ar
en
th
eses
,
a
n
d
s
p
ec
ial
s
y
m
b
o
ls
th
at
ar
e
k
n
o
wn
as
B
o
o
lean
(
p
r
o
p
o
s
itio
n
al)
co
n
n
ec
tiv
es.
B
o
o
lean
f
o
r
m
u
las
ar
e
also
r
ef
er
r
ed
to
as
“
p
r
o
p
o
s
itio
n
al
f
o
r
m
u
las
”
o
r
“
f
o
r
m
u
las
o
f
lo
g
ic
alg
eb
r
a
.
”
T
h
er
e
a
r
e
B
o
o
lean
f
o
r
m
u
las
p
r
e
s
en
ted
in
a
s
p
ec
ial
f
o
r
m
k
n
o
w
n
as
n
o
r
m
al
f
o
r
m
s
.
T
h
e
p
r
im
ar
y
o
b
ject
o
f
f
u
r
th
er
co
n
s
id
er
atio
n
will b
e
B
o
o
lean
f
o
r
m
u
las in
c
o
n
ju
n
ctiv
e
n
o
r
m
al
f
o
r
m
(
C
NF)
[
2
]
.
L
et
{
0
,
1
}
b
e
th
e
s
et
o
f
all
wo
r
d
s
o
f
len
g
th
o
v
er
th
e
alp
h
a
b
e
t
{
0
,
1
}
.
I
n
s
ev
er
al
s
o
u
r
ce
s
,
th
e
elem
en
ts
o
f
{
0
,
1
}
ar
e
r
ef
e
r
r
ed
to
as
B
o
o
lean
v
ec
to
r
s
.
An
y
B
o
o
lean
f
o
r
m
u
la
o
f
v
ar
iab
les
d
ef
in
e
a
co
m
p
letely
d
e
f
in
ed
B
o
o
lea
n
f
u
n
ctio
n
:
{
0
,
1
}
→
{
0
,
1
}
.
A
f
o
r
m
u
la
is
ca
lled
s
atis
f
iab
le
if
th
er
e
ex
is
ts
an
ass
ig
n
m
en
t
∈
{
0
,
1
}
o
f
v
alu
es
to
th
e
v
ar
iab
les
in
s
u
ch
th
at
(
)
=
1
.
Su
ch
an
ass
ig
n
m
en
t
is
ca
lled
a
s
atis
f
y
in
g
ass
ig
n
m
en
t
f
o
r
.
I
f
n
o
s
u
ch
ass
ig
n
m
en
t
ex
is
ts
,
is
ca
lled
u
n
s
atis
f
iab
le.
Fo
r
an
y
B
o
o
lean
f
o
r
m
u
la
,
a
cir
cu
it c
an
b
e
co
n
s
tr
u
cted
f
r
o
m
f
u
n
ctio
n
al
elem
en
ts
o
v
er
an
ar
b
itra
r
y
c
o
m
p
lete
b
asis
,
f
o
r
ex
am
p
le,
{
∧
,
¬}
.
Fro
m
th
is
cir
cu
it,
u
s
in
g
T
s
eitin
tr
an
s
f
o
r
m
atio
n
s
,
o
n
e
ca
n
co
n
s
tr
u
ct
a
C
NF
(
)
th
at
is
s
atis
f
iab
le
if
a
n
d
o
n
ly
if
is
s
ati
s
f
iab
le.
T
h
e
f
o
r
m
u
la
(
)
is
g
en
er
ally
a
f
o
r
m
u
la
with
m
o
r
e
v
ar
iab
les
th
an
.
Ho
wev
er
,
im
p
o
r
tan
tly
,
th
e
t
r
an
s
itio
n
f
r
o
m
to
(
)
is
p
er
f
o
r
m
ed
in
p
o
l
y
n
o
m
ial
tim
e
r
elativ
e
t
o
th
e
len
g
th
o
f
th
e
b
in
ar
y
r
ep
r
esen
tatio
n
o
f
.
Giv
en
th
is
,
e
v
er
y
wh
e
r
e
b
el
o
w,
th
e
B
o
o
lean
s
atis
f
iab
ilit
y
p
r
o
b
le
m
will
r
ef
er
to
th
e
p
r
o
b
lem
o
f
s
atis
f
iab
ilit
y
o
f
an
y
C
NF:
th
at
i
s
,
g
iv
en
an
ar
b
itr
ar
y
C
NF
,
th
e
q
u
esti
o
n
is
to
d
eter
m
in
e
wh
eth
er
is
s
atis
f
iab
le.
SAT
is
a
class
ic
al
NP
-
co
m
p
lete
p
r
o
b
lem
[
3
]
.
T
h
u
s
,
if
≠
,
th
e
n
SAT
ca
n
n
o
t
b
e
s
o
lv
ed
in
p
o
ly
n
o
m
ial
tim
e
(
r
elativ
e
to
t
h
e
s
ize
o
f
th
e
C
NF)
in
th
e
g
en
er
al
ca
s
e.
Nev
er
th
eless
,
th
e
last
2
0
y
ea
r
s
h
av
e
s
ee
n
s
ig
n
if
ican
t
p
r
o
g
r
ess
in
th
e
d
ev
elo
p
m
en
t
o
f
SAT
-
s
o
lv
in
g
alg
o
r
ith
m
s
,
ac
h
iev
in
g
im
p
r
ess
iv
e
r
esu
lts
o
n
ex
ten
s
iv
e
class
es o
f
s
o
-
ca
lled
in
d
u
s
tr
ial
b
en
c
h
m
ar
k
s
[
4
]
,
[
5
]
.
On
e
o
f
th
e
m
o
s
t
im
p
o
r
tan
t
class
es
o
f
lo
g
ical
eq
u
atio
n
s
is
f
o
r
m
ed
b
y
eq
u
atio
n
s
in
th
e
f
o
r
m
o
f
C
NF
=
1
,
wh
er
e
1
d
en
o
tes
th
e
tr
u
e
v
alu
e.
T
h
e
p
r
o
b
lem
s
o
f
f
in
d
in
g
s
o
lu
tio
n
s
to
th
is
class
o
f
eq
u
atio
n
s
b
elo
n
g
to
th
e
s
o
-
ca
lled
SAT
p
r
o
b
lem
s
.
Sp
ec
ial
s
o
f
twar
e
to
o
ls
ca
lle
d
SAT
s
o
lv
er
s
ar
e
u
s
ed
to
s
o
l
v
e
SAT
p
r
o
b
lem
s
.
Fo
r
s
o
m
e
ca
s
es,
SAT
s
o
lv
er
s
allo
w
f
in
d
in
g
a
s
atis
f
y
in
g
ass
ig
n
m
en
t
f
o
r
th
e
C
NF,
i.e
.
,
a
s
et
o
f
v
ar
iab
le
v
alu
es
th
at
ev
alu
ates
th
e
C
NF
to
“
tr
u
e.
”
Fro
m
th
is
ass
ig
n
m
en
t,
th
e
d
esire
d
s
ec
r
et
k
e
y
ca
n
b
e
e
f
f
icien
tly
o
b
tain
ed
.
T
h
is
ap
p
r
o
ac
h
is
ca
lled
SAT
cr
y
p
tan
aly
s
is
.
I
n
th
e
f
ield
o
f
cr
y
p
tan
aly
s
is
,
SAT
s
o
lv
er
s
ca
n
b
e
ap
p
lied
t
o
a
v
ar
iety
o
f
task
s
[
6
]
.
T
h
ey
ar
e
u
s
ed
to
s
ea
r
ch
f
o
r
a
k
e
y
u
s
in
g
a
cip
h
er
tex
t
-
o
n
ly
attac
k
,
o
r
t
o
s
ea
r
ch
f
o
r
a
k
ey
u
s
in
g
a
k
n
o
wn
-
p
lain
tex
t
attac
k
.
Ad
d
itio
n
ally
,
SAT
s
o
lv
er
s
ar
e
em
p
lo
y
ed
t
o
p
r
o
v
e
th
at
a
ci
p
h
er
is
f
aith
f
u
l,
m
ea
n
i
n
g
th
e
s
am
e
cip
h
er
tex
t c
an
n
o
t
b
e
g
e
n
er
ated
u
s
in
g
d
if
f
e
r
en
t
k
ey
s
,
wh
ich
i
m
p
lies
th
e
a
b
s
en
ce
o
f
a
u
n
iv
er
s
al
k
ey
ca
p
ab
le
o
f
d
ec
r
y
p
tin
g
cip
h
er
tex
t
e
n
cr
y
p
ted
with
an
y
o
th
er
k
ey
.
T
h
ey
also
d
em
o
n
s
tr
ate
th
at
a
cip
h
e
r
is
n
o
t
clo
s
ed
,
wh
ich
m
ea
n
s
th
a
t
f
o
r
a
n
y
two
k
e
y
s
,
th
er
e
d
o
es
n
o
t
ex
is
t
a
th
i
r
d
k
ey
s
u
ch
t
h
at
d
o
u
b
le
e
n
cr
y
p
tio
n
with
t
h
e
f
ir
s
t
two
k
ey
s
is
eq
u
iv
alen
t
to
e
n
cr
y
p
tio
n
with
th
e
th
ir
d
k
e
y
.
Fu
r
t
h
er
m
o
r
e,
S
AT
s
o
lv
er
s
ca
n
p
r
o
v
e
th
at
a
c
ip
h
er
d
o
es
n
o
t
h
a
v
e
wea
k
k
ey
s
,
s
p
ec
if
ically
s
h
o
win
g
th
at
n
o
k
ey
s
ex
is
t
f
o
r
wh
i
ch
d
o
u
b
le
en
c
r
y
p
tio
n
is
eq
u
iv
alen
t
to
s
eq
u
en
tial
en
cr
y
p
tio
n
an
d
d
ec
r
y
p
tio
n
o
p
er
atio
n
s
.
L
astl
y
,
SAT
s
o
lv
e
r
s
ar
e
u
s
ed
to
ev
alu
ate
th
e
s
tr
en
g
th
o
f
h
ash
in
g
alg
o
r
ith
m
s
b
y
s
ea
r
ch
in
g
f
o
r
c
o
llis
io
n
s
,
f
ir
s
t o
r
s
ec
o
n
d
p
r
ei
m
a
g
es,
an
d
o
t
h
er
v
u
ln
er
ab
ilit
ies.
Scien
tific
s
tu
d
ies
o
n
th
e
ap
p
li
ca
tio
n
o
f
SAT
s
o
lv
er
s
f
o
r
an
al
y
zin
g
c
r
y
p
to
g
r
ap
h
ic
h
ash
f
u
n
c
tio
n
s
h
av
e
d
em
o
n
s
tr
ated
v
ar
io
u
s
a
p
p
r
o
ac
h
es
an
d
th
eir
ef
f
ec
tiv
en
ess
.
T
h
ese
wo
r
k
s
ex
p
l
o
r
e
b
o
th
th
e
th
eo
r
etica
l
asp
ec
ts
an
d
th
e
p
r
ac
tical
ef
f
icien
cy
o
f
ap
p
ly
i
n
g
SAT
s
o
l
v
er
s
in
th
is
f
ield
.
R
esear
ch
er
s
h
a
v
e
s
h
o
w
n
h
o
w
SAT
s
o
lv
er
s
ca
n
b
e
u
tili
ze
d
to
id
e
n
tify
v
u
ln
er
ab
ilit
ies
in
h
ash
f
u
n
ctio
n
s
,
s
u
ch
as
f
i
n
d
in
g
co
llis
io
n
s
o
r
p
r
e
-
im
a
g
es.
Mo
r
eo
v
er
,
ad
v
an
ce
m
en
ts
in
SAT
s
o
lv
er
alg
o
r
ith
m
s
h
av
e
s
ig
n
if
ican
tly
im
p
r
o
v
ed
t
h
eir
p
e
r
f
o
r
m
a
n
ce
,
m
ak
in
g
th
em
a
p
o
wer
f
u
l to
o
l f
o
r
ev
alu
atin
g
th
e
s
ec
u
r
ity
o
f
m
o
d
er
n
c
r
y
p
to
g
r
ap
h
ic
h
ash
f
u
n
ctio
n
s
.
I
n
th
e
s
tu
d
y
[
7
]
,
SAT
s
o
lv
er
s
wer
e
u
s
ed
to
f
in
d
c
o
llis
io
n
s
in
th
e
SHA
-
2
5
6
h
ash
f
u
n
ctio
n
b
ased
o
n
s
o
-
ca
lled
“
s
em
i
-
f
r
ee
-
s
tar
t
”
c
o
llis
io
n
s
.
Au
th
o
r
s
in
te
g
r
ated
th
e
p
r
o
g
r
am
m
atic
SAT+
C
AS
p
ar
ad
ig
m
with
d
if
f
er
en
tial
cr
y
p
tan
aly
s
is
m
eth
o
d
s
p
r
ev
i
o
u
s
ly
em
p
lo
y
ed
in
co
llis
io
n
attac
k
s
o
n
SHA
-
2
5
6
.
Alth
o
u
g
h
th
ese
attac
k
s
ar
e
s
till
f
ar
f
r
o
m
f
in
d
in
g
co
llis
io
n
s
f
o
r
th
e
f
u
ll
v
er
s
i
o
n
o
f
SHA
-
2
5
6
,
th
ey
s
h
o
w
p
r
o
g
r
ess
in
ap
p
ly
in
g
SAT
s
o
lv
er
s
f
o
r
an
aly
zin
g
th
e
s
ec
u
r
ity
o
f
h
ash
f
u
n
ctio
n
s
.
Pro
g
r
am
m
a
b
le
SAT
s
o
lv
er
s
f
o
r
cr
y
p
tan
aly
s
is
allo
w
th
e
cu
s
to
m
izatio
n
o
f
th
e
SAT
-
s
o
lv
i
n
g
p
r
o
ce
s
s
f
o
r
s
p
ec
if
ic
cr
y
p
to
g
r
a
p
h
ic
tas
k
s
,
m
ak
in
g
th
em
m
o
r
e
f
le
x
ib
l
e
an
d
ef
f
ec
tiv
e
f
o
r
an
al
y
zin
g
h
ash
f
u
n
ctio
n
s
[
8
]
.
T
h
ey
en
a
b
le
th
e
co
n
s
id
er
ati
o
n
o
f
cr
y
p
to
g
r
ap
h
ic
o
p
er
ati
o
n
s
'
ch
ar
ac
ter
is
tics
an
d
ap
p
l
y
th
em
d
u
r
in
g
th
e
p
r
o
p
a
g
atio
n
a
n
d
co
n
f
lict
an
a
ly
s
is
p
r
o
ce
s
s
es.
T
h
e
au
th
o
r
s
en
h
an
ce
t
h
e
p
r
o
p
ag
ati
o
n
an
d
co
n
f
lict
a
n
aly
s
is
m
ec
h
an
is
m
s
o
f
co
n
f
lict
-
d
r
iv
e
n
clau
s
e
lear
n
in
g
(
C
DC
L
)
s
o
lv
er
s
b
y
in
co
r
p
o
r
atin
g
s
p
ec
ialized
alg
o
r
ith
m
s
tailo
r
ed
to
t
h
e
cr
y
p
to
g
r
ap
h
ic
p
r
im
itiv
es
u
n
d
er
e
x
am
in
atio
n
.
T
h
is
m
eth
o
d
p
r
o
v
es
to
b
e
h
ig
h
ly
ef
f
ec
tiv
e,
p
ar
ticu
lar
ly
in
t
h
e
d
if
f
er
en
tia
l
p
ath
an
aly
s
is
an
d
alg
e
b
r
aic
f
au
lt
d
etec
tio
n
o
f
h
ash
f
u
n
c
tio
n
s
.
Pre
lim
in
ar
y
Evaluation Warning : The document was created with Spire.PDF for Python.
I
n
t J E
lec
&
C
o
m
p
E
n
g
I
SS
N:
2088
-
8
7
0
8
A
p
p
lica
tio
n
o
f
s
a
tis
fia
b
ilit
y
p
r
o
b
lem
s
o
lvers
fo
r
a
s
s
ess
in
g
th
e
s
tr
en
g
th
o
f
…
(
K
u
n
b
o
la
t A
l
g
a
z
y
)
3193
r
esu
lts
h
ig
h
lig
h
t
th
e
p
o
ten
tial
o
f
th
is
ap
p
r
o
ac
h
,
co
n
f
ir
m
in
g
it
as
a
s
u
b
s
tan
tial
ad
v
an
ce
m
en
t
co
m
p
ar
e
d
to
tr
ad
itio
n
al
B
lack
b
o
x
SAT
-
b
ased
cr
y
p
ta
n
aly
s
is
tech
n
iq
u
es.
L
in
g
elin
g
is
a
h
ig
h
ly
o
p
tim
ized
SAT
s
o
lv
er
th
at
h
as
b
ee
n
u
s
ed
s
u
cc
ess
f
u
lly
in
v
a
r
io
u
s
SAT
co
m
p
etitio
n
s
.
I
t
h
as
b
ee
n
e
x
p
an
d
ed
in
t
o
two
p
a
r
allel
v
ar
ian
ts
:
Pli
n
g
elin
g
an
d
T
r
ee
n
g
elin
g
.
I
n
s
tu
d
y
[
9
]
,
two
s
o
lv
er
s
,
Pli
n
g
elin
g
an
d
T
r
ee
n
g
elin
g
,
ar
e
d
escr
ib
ed
,
b
o
th
o
f
wh
ich
s
u
p
p
o
r
t
p
a
r
allel
an
d
d
is
tr
ib
u
ted
co
m
p
u
tin
g
.
Pli
n
g
elin
g
d
iv
id
es
t
h
e
task
a
m
o
n
g
m
u
ltip
le
th
r
ea
d
s
o
n
a
s
in
g
le
p
r
o
ce
s
s
o
r
,
wh
ile
T
r
ee
n
g
elin
g
d
is
tr
ib
u
tes
th
e
wo
r
k
ac
r
o
s
s
s
ev
er
al
n
o
d
es in
a
d
is
tr
ib
u
ted
s
y
s
tem
.
W
h
ile
SAT
s
o
lv
er
s
r
ep
r
ese
n
t
a
p
o
wer
f
u
l
to
o
l
f
o
r
s
o
lv
in
g
ce
r
tain
class
es
o
f
p
r
o
b
l
em
s
,
th
eir
ap
p
licatio
n
in
cr
y
p
to
g
r
ap
h
y
i
s
lim
ited
d
u
e
to
th
e
co
m
p
lex
i
ty
,
s
ca
le,
an
d
s
p
ec
if
icity
o
f
c
r
y
p
to
g
r
ap
h
ic
task
s
.
Su
cc
ess
f
u
l
u
s
e
o
f
SAT
s
o
lv
e
r
s
in
cr
y
p
to
g
r
a
p
h
y
r
eq
u
ir
es
a
d
ee
p
u
n
d
er
s
tan
d
in
g
o
f
b
o
t
h
th
e
cr
y
p
to
g
r
ap
h
ic
p
r
im
itiv
es
th
em
s
elv
es
an
d
th
e
m
eth
o
d
s
f
o
r
t
r
an
s
f
o
r
m
i
n
g
t
h
ese
p
r
o
b
lem
s
in
to
a
s
o
lv
a
b
le
f
o
r
m
f
o
r
SAT
s
o
lv
er
s
.
T
h
e
m
ain
lim
itatio
n
s
in
ap
p
l
y
in
g
SAT
s
o
lv
e
r
s
in
clu
d
e
asp
e
cts
s
u
ch
as
ex
p
o
n
e
n
tial
co
m
p
lex
ity
,
ex
ce
s
s
iv
ely
lar
g
e
an
d
co
m
p
le
x
B
o
o
lean
f
o
r
m
u
las,
an
d
t
h
e
ch
allen
g
i
n
g
s
ca
lab
ilit
y
o
f
s
im
p
lifie
d
v
e
r
s
io
n
s
o
f
cr
y
p
to
g
r
ap
h
ic
alg
o
r
ith
m
s
to
f
u
ll
-
r
o
u
n
d
v
er
s
io
n
s
.
Ov
er
co
m
in
g
th
ese
lim
itatio
n
s
in
s
o
lv
in
g
cr
y
p
to
g
r
ap
h
ic
task
s
with
SAT
s
o
lv
er
s
r
eq
u
ir
es
a
co
m
p
r
eh
e
n
s
iv
e
ap
p
r
o
ac
h
,
in
clu
d
i
n
g
al
g
o
r
ith
m
o
p
tim
izatio
n
,
th
e
d
e
v
elo
p
m
en
t
o
f
n
ew
m
eth
o
d
s
,
a
n
d
th
e
ap
p
licatio
n
o
f
v
ar
io
u
s
s
tr
ateg
ies.
On
e
wa
y
to
o
v
er
co
m
e
th
ese
lim
itatio
n
s
is
th
r
o
u
g
h
th
e
u
s
e
o
f
p
ar
allel
co
m
p
u
tin
g
.
T
h
e
u
s
e
o
f
p
a
r
allel
o
r
d
is
tr
ib
u
te
d
co
m
p
u
tin
g
i
n
SAT
s
o
lv
er
s
is
esp
ec
ially
b
en
ef
icial
wh
en
d
ea
lin
g
with
lar
g
e
f
o
r
m
u
las,
as
it
allo
ws
d
if
f
er
en
t
p
ar
ts
o
f
th
e
task
to
b
e
p
r
o
ce
s
s
ed
s
im
u
ltan
eo
u
s
ly
,
s
ig
n
if
ican
tly
im
p
r
o
v
i
n
g
th
e
ef
f
icien
cy
o
f
s
o
lv
in
g
p
r
o
b
lem
s
.
B
ased
o
n
th
is
,
th
e
S
AT
s
o
lv
er
ex
p
er
im
en
ts
in
th
is
r
esear
ch
wer
e
co
n
d
u
cted
o
n
t
h
e
HP E
n
ter
p
r
is
e
DL
3
8
0
Gen
1
0
/2
Xeo
n
Go
l
d
s
er
v
er
.
SAT
s
o
lv
er
s
ar
e
p
o
wer
f
u
l
to
o
l
s
f
o
r
ev
alu
atin
g
th
e
cr
y
p
to
g
r
a
p
h
ic
s
tr
en
g
th
o
f
h
ash
f
u
n
ctio
n
s
.
W
ith
th
e
co
n
tin
u
o
u
s
g
r
o
wth
o
f
co
m
p
u
t
atio
n
al
ca
p
ab
ilit
ies,
r
esear
ch
is
o
n
g
o
in
g
to
e
n
h
an
ce
t
h
e
ef
f
ic
ien
cy
o
f
s
o
lv
er
s
an
d
ad
ap
t
th
em
f
o
r
an
al
y
zin
g
m
o
d
er
n
cr
y
p
to
g
r
a
p
h
ic
h
ash
f
u
n
ct
io
n
s
.
T
h
e
s
cien
tific
co
m
m
u
n
it
y
ex
p
lo
r
es
v
ar
io
u
s
ap
p
r
o
ac
h
es
an
d
SAT
s
o
lv
er
s
to
id
en
tify
v
u
ln
e
r
ab
ilit
ies
s
u
ch
as
co
llis
io
n
s
,
f
ir
s
t
-
p
r
eim
ag
e,
an
d
s
ec
o
n
d
-
p
r
eim
ag
e
attac
k
s
.
T
h
e
ess
en
c
e
o
f
t
h
is
r
esear
ch
lies
in
ass
ess
in
g
th
e
cr
y
p
t
o
g
r
a
p
h
ic
s
tr
e
n
g
th
o
f
th
e
n
ewly
d
ev
elo
p
e
d
h
ash
f
u
n
ctio
n
HB
C
-
2
5
6
u
s
in
g
s
tate
-
of
-
th
e
-
ar
t
SAT
s
o
lv
er
s
,
as
th
e
d
ev
elo
p
m
en
t
o
f
a
n
y
h
ash
f
u
n
ctio
n
m
u
s
t
b
e
ac
co
m
p
a
n
ie
d
b
y
a
th
o
r
o
u
g
h
s
ec
u
r
ity
a
n
a
ly
s
is
,
in
clu
d
in
g
m
o
d
elin
g
p
o
t
en
tial
attac
k
s
with
SAT
s
o
lv
er
s
.
T
o
ad
d
r
ess
th
is
is
s
u
e,
th
e
s
tu
d
y
c
o
n
d
u
cted
a
p
r
ac
tical
c
r
y
p
tan
aly
s
is
o
f
t
h
e
cr
y
p
to
g
r
a
p
h
ic
h
ash
f
u
n
ctio
n
HB
C
-
2
5
6
.
A
s
er
ies
o
f
ex
p
e
r
im
en
ts
wer
e
ca
r
r
ied
o
u
t
to
ev
alu
ate
th
e
r
esil
ien
ce
o
f
th
e
HB
C
-
2
5
6
h
ash
in
g
al
g
o
r
ith
m
ag
ain
s
t
p
r
ei
m
ag
e
attac
k
s
.
T
h
is
ar
ticle
p
r
es
en
ts
an
e
v
alu
atio
n
o
f
th
e
p
er
f
o
r
m
an
ce
o
f
p
ar
allel
an
d
s
eq
u
en
tial
SAT
s
o
lv
er
s
i
n
s
o
lv
in
g
p
r
eim
ag
e
s
ea
r
ch
p
r
o
b
lem
s
f
o
r
th
e
HB
C
-
2
5
6
h
ash
in
g
alg
o
r
ith
m
.
T
h
e
co
n
tr
ib
u
tio
n
s
o
f
th
is
wo
r
k
ar
e
as f
o
llo
ws:
−
A
b
r
ief
o
v
er
v
iew
o
f
ex
is
tin
g
m
eth
o
d
s
an
d
ap
p
r
o
ac
h
es
f
o
r
c
h
ec
k
in
g
th
e
s
atis
f
iab
ilit
y
o
f
a
B
o
o
lean
f
u
n
ctio
n
r
ep
r
esen
ted
in
C
NF a
n
d
f
in
d
in
g
its
v
alu
e
s
et
is
p
r
o
v
id
e
d
;
−
A
co
m
p
ar
ativ
e
an
aly
s
is
o
f
th
e
ef
f
ec
tiv
en
ess
o
f
th
e
SAT
s
o
l
v
er
s
L
in
g
elin
g
,
C
aDiCaL
,
Kis
s
at,
Pli
n
g
elin
g
,
T
r
ee
n
g
elin
g
,
an
d
Par
k
is
s
at
is
c
o
n
d
u
cte
d
u
s
in
g
th
e
HB
C
-
2
5
6
h
ash
f
u
n
ctio
n
as a
n
ex
a
m
p
le;
−
Usi
n
g
Par
k
is
s
at,
wh
ich
d
em
o
n
s
tr
ated
th
e
b
est
r
esu
lts
in
th
e
co
m
p
ar
ativ
e
a
n
aly
s
is
,
th
e
h
ig
h
cr
y
p
t
o
g
r
a
p
h
ic
s
tr
en
g
th
o
f
t
h
e
HB
C
-
2
5
6
h
ash
f
u
n
ctio
n
is
p
r
o
v
e
n
.
2.
M
E
T
H
O
D
T
h
e
f
o
llo
win
g
m
eth
o
d
s
wer
e
em
p
lo
y
ed
d
u
r
i
n
g
th
e
r
esear
ch
:
i)
p
r
o
p
o
s
itio
n
al
en
co
d
i
n
g
to
tr
an
s
f
o
r
m
cr
y
p
to
g
r
ap
h
ic
al
g
o
r
ith
m
s
in
t
o
B
o
o
lean
f
o
r
m
u
las
a
n
d
ii)
s
o
lu
tio
n
s
ea
r
ch
f
o
r
th
e
s
atis
f
iab
ilit
y
p
r
o
b
lem
o
f
B
o
o
lean
f
o
r
m
u
las
u
s
in
g
ef
f
ici
en
t
SAT
s
o
lv
er
s
.
T
h
e
u
s
e
o
f
SAT
s
o
lv
er
s
in
alg
eb
r
aic
cr
y
p
tan
aly
s
is
p
r
o
v
id
es
a
p
o
wer
f
u
l
to
o
l
f
o
r
s
o
lv
in
g
c
o
m
p
lex
s
y
s
tem
s
o
f
eq
u
atio
n
s
,
m
ak
in
g
th
is
ap
p
r
o
ac
h
p
ar
tic
u
lar
ly
ef
f
ec
tiv
e
f
o
r
an
aly
zin
g
cr
y
p
to
g
r
ap
h
ic
s
y
s
tem
s
.
T
h
e
ad
v
a
n
tag
e
o
f
alg
e
b
r
aic
cr
y
p
ta
n
aly
s
is
lies
in
its
v
er
s
atility
,
as
th
is
ap
p
r
o
ac
h
ca
n
b
e
a
p
p
lied
t
o
an
y
cip
h
er
th
at
ca
n
b
e
ex
p
r
ess
ed
in
alg
eb
r
aic
f
o
r
m
,
i
n
clu
d
in
g
s
y
m
m
etr
ic
cip
h
er
s
,
asy
m
m
etr
ic
s
ch
em
es,
ellip
tic
cu
r
v
e
-
b
ased
s
ch
em
es,
an
d
h
ash
f
u
n
ctio
n
s
,
wh
er
ea
s
d
if
f
er
en
tial
an
d
lin
ea
r
cr
y
p
tan
aly
s
is
ar
e
g
en
er
ally
l
im
ited
to
s
y
m
m
et
r
ic
b
lo
c
k
cip
h
er
s
an
d
th
eir
ef
f
ec
tiv
e
n
e
s
s
d
ep
en
d
s
o
n
th
e
s
p
ec
if
ics
o
f
th
e
alg
o
r
ith
m
.
Ho
wev
er
,
t
h
e
a
p
p
licatio
n
o
f
SAT
s
o
lv
er
s
to
cr
y
p
to
g
r
a
p
h
ic
p
r
o
b
lem
s
r
e
q
u
ir
es
s
ig
n
if
ican
t
co
m
p
u
tatio
n
al
r
eso
u
r
ce
s
,
lim
itin
g
th
eir
p
r
ac
tic
al
u
s
e
in
s
o
m
e
ca
s
es.
T
h
er
ef
o
r
e,
in
ter
m
s
o
f
p
er
f
o
r
m
an
ce
an
d
ef
f
icien
cy
,
th
e
m
ain
f
o
c
u
s
will b
e
o
n
s
elec
tin
g
th
e
s
p
ec
if
ic
SAT
s
o
lv
er
.
2
.
1
.
P
r
o
po
s
it
io
na
l e
nco
din
g
t
o
t
ra
ns
f
o
r
m
cr
y
pto
g
ra
ph
ic
a
lg
o
rit
hm
s
into
B
o
o
lea
n f
o
r
m
ula
s
Sin
ce
m
an
u
al
en
co
d
in
g
is
i
m
p
r
ac
tical,
cr
y
p
to
g
r
ap
h
ic
al
g
o
r
ith
m
s
ar
e
ty
p
ically
tr
an
s
f
o
r
m
ed
in
to
B
o
o
lean
f
o
r
m
u
las
u
s
in
g
s
p
ec
ialized
to
o
ls
.
T
h
ese
to
o
ls
en
ab
le
th
e
ex
p
r
ess
io
n
o
f
cr
y
p
to
g
r
a
p
h
ic
alg
o
r
ith
m
s
in
h
ig
h
-
lev
el
p
r
o
g
r
am
m
in
g
lan
g
u
ag
es,
f
o
llo
wed
b
y
th
e
c
o
n
v
er
s
io
n
o
f
t
h
e
r
esu
ltin
g
p
r
o
g
r
a
m
in
to
th
e
co
r
r
esp
o
n
d
in
g
B
o
o
lean
f
o
r
m
u
la
in
C
NF.
T
h
e
r
esu
ltin
g
f
o
r
m
u
la
is
th
en
s
av
ed
in
a
f
ile
with
th
e
s
tan
d
ar
d
DI
MA
C
S f
o
r
m
at,
m
ak
in
g
it c
o
m
p
atib
le
f
o
r
u
s
e
as in
p
u
t d
at
a
b
y
m
o
d
er
n
SAT
s
o
lv
er
s
.
Evaluation Warning : The document was created with Spire.PDF for Python.
I
SS
N
:
2
0
8
8
-
8
7
0
8
I
n
t J E
lec
&
C
o
m
p
E
n
g
,
Vo
l.
15
,
No
.
3
,
J
u
n
e
20
25
:
3
1
9
1
-
3
2
0
1
3194
Fo
r
th
e
p
r
ep
ar
atio
n
o
f
ex
p
er
i
m
en
tal
d
ata
in
th
is
p
ap
e
r
,
th
e
T
r
an
s
alg
s
o
f
twar
e
s
u
ite
was
e
m
p
lo
y
ed
as
s
u
ch
a
to
o
l.
T
r
an
s
alg
was
d
ev
elo
p
ed
b
y
t
h
e
Ma
tr
o
s
o
v
I
n
s
titu
te
f
o
r
s
y
s
tem
d
y
n
a
m
ics
an
d
c
o
n
tr
o
l
th
eo
r
y
o
f
th
e
Sib
er
ian
B
r
an
ch
o
f
th
e
R
u
s
s
ian
Aca
d
em
y
o
f
Scien
ce
s
,
lo
ca
ted
in
I
r
k
u
ts
k
[
1
0
]
.
T
h
is
s
u
ite
f
ac
ilit
ates
th
e
co
n
v
er
s
io
n
o
f
ar
b
itra
r
y
alg
o
r
i
th
m
s
in
to
B
o
o
lean
f
o
r
m
u
las.
T
h
ese
alg
o
r
ith
m
s
co
m
p
u
te
ev
er
y
wh
er
e
-
d
ef
in
e
d
d
is
cr
ete
f
u
n
ctio
n
s
,
i.e
.
,
f
u
n
ct
io
n
s
o
f
th
e
f
o
r
m
:
{
0
,
1
}
∗
→
{
0
,
1
}
∗
,
an
d
a
r
e
ex
p
r
ess
ed
u
s
in
g
th
e
s
p
ec
ially
d
esig
n
ed
p
r
o
g
r
a
m
m
in
g
la
n
g
u
a
g
e
T
A
ak
in
to
C
[
1
1
]
.
2
.
2
.
Sea
rc
hin
g
f
o
r
s
o
lutio
ns
t
o
B
o
o
lea
n f
o
r
m
ula
s
a
t
is
f
ia
b
ility
pro
blem
s
us
ing
ef
f
icient
SAT
s
o
lv
er
s
An
y
B
o
o
lean
s
atis
f
iab
ilit
y
p
r
o
b
lem
co
n
s
is
ts
o
f
two
k
ey
s
u
b
task
s
-
ch
ec
k
in
g
th
e
s
atis
f
iab
ilit
y
o
f
a
n
ar
b
itra
r
y
B
o
o
lea
n
f
u
n
ctio
n
r
e
p
r
esen
ted
in
C
NF
an
d
f
in
d
in
g
a
s
et
o
f
v
alu
es
f
o
r
wh
ich
s
u
c
h
a
C
NF
is
s
atis
f
ied
.
T
h
e
f
o
u
n
d
atio
n
o
f
m
o
s
t
SAT
s
o
lv
er
s
is
th
e
Dav
is
-
Pu
tn
am
-
L
o
g
em
an
n
-
L
o
v
elan
d
(
DPLL
)
alg
o
r
ith
m
[
1
2
]
,
[
1
3
]
wh
ich
was
s
p
ec
if
ically
p
r
o
p
o
s
ed
f
o
r
d
ete
r
m
in
in
g
th
e
s
atis
f
iab
ilit
y
o
f
B
o
o
lean
f
o
r
m
u
las
wr
itten
in
C
NF,
i.e
.
,
f
o
r
s
o
lv
in
g
SAT
p
r
o
b
lem
s
.
T
h
e
DPLL
alg
o
r
ith
m
s
er
v
es a
s
th
e
b
asis
f
o
r
m
o
s
t e
f
f
icien
t SAT
s
o
lv
er
s
.
T
h
e
m
ain
id
ea
o
f
th
e
DPLL
alg
o
r
ith
m
is
t
o
ap
p
ly
d
ep
th
-
f
i
r
s
t
s
ea
r
ch
m
eth
o
d
s
an
d
u
tili
z
e
th
e
u
n
it
p
r
o
p
a
g
atio
n
r
u
le.
T
h
e
DPLL
alg
o
r
ith
m
d
i
v
id
es
th
e
s
et
o
f
v
ar
iab
les
o
f
th
e
C
NF
f
o
r
m
u
la
i
n
to
two
s
u
b
s
ets,
A
an
d
B
,
wh
e
r
e
s
u
b
s
et
A
c
o
n
tai
n
s
v
ar
iab
les
with
a
v
alu
e
o
f
“
t
r
u
e
”
an
d
s
u
b
s
et
B
co
n
tain
s
v
a
r
iab
les
with
a
v
al
u
e
o
f
“
f
alse
.
”
At
ea
ch
s
tep
,
an
ar
b
itra
r
y
v
ar
ia
b
le
f
r
o
m
th
e
C
NF
f
o
r
m
u
la
is
ch
o
s
en
,
an
d
it
is
ass
ig
n
ed
a
v
alu
e
o
f
“
tr
u
e
”
(
ad
d
in
g
th
e
v
ar
iab
le
to
s
u
b
s
et
A)
.
T
h
en
th
e
o
r
ig
in
al
f
o
r
m
u
la
is
s
im
p
lifie
d
,
an
d
th
e
s
im
p
lifie
d
p
r
o
b
lem
is
s
o
lv
ed
.
I
f
th
e
s
im
p
lifie
d
C
NF
f
o
r
m
u
la
is
s
ati
s
f
iab
le,
th
en
th
e
v
ar
iab
le
v
alu
e
ch
o
s
en
is
co
r
r
ec
t;
o
th
er
wis
e,
th
e
ch
o
s
en
v
a
r
iab
le
is
ass
ig
n
ed
a
v
alu
e
o
f
“
f
alse,
”
a
n
d
it
is
m
o
v
ed
to
s
u
b
s
et
B
.
T
h
e
p
r
o
b
lem
is
th
en
s
o
lv
e
d
ag
ain
f
o
r
th
e
ch
o
s
en
“
f
alse
”
v
ar
iab
le
v
alu
e.
T
h
u
s
,
eith
er
th
e
co
r
r
ec
t
v
a
r
iab
le
v
alu
e
(
“
tr
u
e
”
o
r
“
f
alse
”
)
will
b
e
f
o
u
n
d
,
o
r
it will b
e
p
r
o
v
en
th
at
th
e
o
r
ig
in
al
f
o
r
m
u
la
is
u
n
s
atis
f
iab
le
[
1
4
]
,
[
1
5
]
.
T
h
e
f
o
u
n
d
atio
n
o
f
th
e
v
ast
m
ajo
r
ity
o
f
m
o
d
e
r
n
co
m
p
lete
SAT
s
o
lv
er
s
,
ef
f
ec
tiv
e
o
n
b
r
o
a
d
class
es
o
f
p
r
ac
tical
test
s
,
is
th
e
co
n
f
lict
-
d
r
iv
en
clau
s
e
lear
n
in
g
(
C
DC
L
)
alg
o
r
ith
m
.
I
n
tu
r
n
,
t
h
is
alg
o
r
i
th
m
is
b
ased
o
n
th
e
DPLL
alg
o
r
ith
m
.
T
h
e
m
ain
d
if
f
er
en
ce
b
etwe
en
th
ese
two
alg
o
r
ith
m
s
is
th
at
C
DC
L
u
s
e
s
m
em
o
r
y
to
s
to
r
e
s
ea
r
ch
h
is
to
r
y
m
o
r
e
p
r
ec
is
ely
,
an
d
in
f
o
r
m
atio
n
ab
o
u
t
d
ea
d
-
e
n
d
b
r
an
c
h
es
o
f
th
e
s
ea
r
ch
tr
ee
is
r
ec
o
r
d
ed
in
th
e
f
o
r
m
o
f
n
ew
c
o
n
s
tr
ain
ts
,
ca
lle
d
co
n
f
lict
clau
s
es
[
1
6
]
–
[
2
0
]
.
T
h
is
allo
ws
f
o
r
s
ig
n
if
ican
tly
d
ee
p
er
b
ac
k
tr
ac
k
in
g
in
s
o
m
e
ca
s
es
th
an
in
DPLL
.
I
n
a
d
d
itio
n
to
c
o
n
v
e
n
tio
n
al
o
r
s
eq
u
e
n
tial
SAT
s
o
lv
er
s
,
p
ar
allel
SAT
s
o
lv
er
s
h
av
e
g
ain
ed
wid
esp
r
ea
d
u
s
e.
T
h
ese
s
o
lv
er
s
ar
e
d
iv
id
ed
in
t
o
th
r
ee
ca
teg
o
r
ies:
p
o
r
tf
o
lio
s
o
lv
er
s
,
d
iv
id
e
-
an
d
-
co
n
q
u
e
r
s
o
lv
er
s
,
an
d
s
o
lv
er
s
b
ased
o
n
p
ar
allel
lo
ca
l sear
ch
.
Po
r
tf
o
lio
s
o
lv
er
s
a
r
e
b
u
ilt
o
n
th
e
u
s
e
o
f
m
u
ltip
le
al
g
o
r
ith
m
s
o
r
d
if
f
er
e
n
t
co
n
f
ig
u
r
ati
o
n
s
o
f
th
e
s
am
e
alg
o
r
ith
m
.
All
s
o
lv
e
r
s
in
th
e
p
ar
allel
p
o
r
tf
o
lio
wo
r
k
o
n
d
if
f
e
r
en
t
p
r
o
ce
s
s
o
r
s
to
s
o
lv
e
t
h
e
s
am
e
p
r
o
b
lem
.
I
f
o
n
e
s
o
lv
er
p
r
o
g
r
am
is
co
m
p
leted
,
th
e
p
o
r
tf
o
lio
s
o
lv
er
r
ep
o
r
ts
wh
eth
er
th
e
p
r
o
b
lem
is
s
atis
f
iab
le
o
r
u
n
s
atis
f
iab
le
ac
co
r
d
in
g
to
th
at
s
o
lv
er
.
All
o
th
er
s
o
lv
er
s
s
to
p
wo
r
k
in
g
.
Div
er
s
if
y
in
g
p
o
r
tf
o
lio
s
b
y
i
n
clu
d
in
g
d
if
f
er
en
t
s
o
lv
er
s
,
ea
ch
o
f
wh
ic
h
p
er
f
o
r
m
s
well
o
n
d
if
f
er
e
n
t
ty
p
es
o
f
p
r
o
b
lem
s
,
en
h
a
n
ce
s
s
o
lv
er
ef
f
icien
cy
.
Ma
n
y
s
o
lv
er
s
u
s
e
r
an
d
o
m
n
u
m
b
er
g
en
er
ato
r
s
in
ter
n
ally
.
Div
e
r
s
if
y
in
g
th
eir
in
itial
v
alu
es
(
s
ee
d
s
)
is
a
s
im
p
le
way
to
d
iv
er
s
if
y
th
e
p
o
r
t
f
o
lio
.
Oth
er
d
iv
er
s
if
icatio
n
s
tr
ateg
ies
in
clu
d
e
en
ab
lin
g
,
d
is
ab
lin
g
,
o
r
d
iv
er
s
if
y
in
g
ce
r
tain
h
eu
r
is
tics
in
th
e
s
eq
u
en
tial so
lv
er
[
2
1
]
,
[
2
2
]
.
Un
lik
e
p
ar
allel
p
o
r
t
f
o
lio
s
,
p
a
r
allel
d
iv
id
e
-
an
d
-
co
n
q
u
er
s
o
l
v
er
s
attem
p
t
to
d
iv
id
e
th
e
s
ea
r
ch
s
p
ac
e
am
o
n
g
in
d
iv
id
u
al
in
s
tan
ce
s
o
f
SAT
s
o
lv
er
s
r
u
n
n
in
g
in
p
a
r
allel
th
r
ea
d
s
.
Ho
wev
er
,
d
u
e
to
t
h
e
u
s
e
o
f
m
eth
o
d
s
s
u
ch
as
u
n
it
p
r
o
p
ag
atio
n
,
af
t
er
p
ar
titi
o
n
in
g
th
e
SAT
p
r
o
b
l
em
in
to
in
d
iv
id
u
al
s
u
b
p
r
o
b
le
m
s
,
th
ey
m
ay
v
ar
y
s
ig
n
if
ican
tly
in
co
m
p
le
x
ity
,
le
ad
in
g
t
o
th
e
ch
allen
g
i
n
g
p
r
o
b
lem
o
f
lo
ad
b
alan
cin
g
.
O
n
e
s
tr
ateg
y
f
o
r
p
ar
allel
lo
ca
l
s
ea
r
ch
to
s
o
lv
e
SAT
in
v
o
lv
es
u
s
in
g
o
p
p
o
s
ite
tr
u
th
v
al
u
es
f
o
r
o
n
e
o
r
m
o
r
e
v
ar
iab
les
(
f
lip
v
ar
iab
les)
in
d
if
f
er
en
t
n
o
d
es
o
f
th
e
co
m
p
u
tin
g
s
y
s
tem
.
T
h
ese
v
ar
iab
les
ar
e
s
elec
ted
u
s
in
g
h
eu
r
is
ti
cs
th
at
attem
p
t
to
d
eter
m
in
e
h
o
w
th
is
ch
an
g
e
ca
n
ex
p
e
d
ite
th
e
SAT
p
r
o
b
l
em
-
s
o
lv
in
g
p
r
o
ce
s
s
b
y
r
ed
u
c
in
g
th
e
n
u
m
b
e
r
o
f
u
n
s
atis
f
ied
clau
s
es.
An
o
th
er
a
p
p
r
o
ac
h
is
to
ap
p
l
y
th
e
af
o
r
em
en
tio
n
ed
p
o
r
tf
o
lio
ap
p
r
o
ac
h
[
2
3
]
,
[
2
4
]
.
Desp
ite
th
e
ab
u
n
d
an
ce
o
f
SA
T
s
o
lv
er
s
o
f
v
ar
io
u
s
ty
p
es
av
ailab
le
to
d
ay
,
a
u
n
iv
er
s
al
s
o
lu
tio
n
th
at
p
er
f
o
r
m
s
eq
u
ally
well
f
o
r
all
task
s
h
as
n
o
t
y
et
b
ee
n
f
o
u
n
d
.
E
ac
h
s
o
lv
er
m
ay
ex
ce
l
at
task
s
th
at
o
th
er
s
s
tr
u
g
g
le
with
wh
ile
p
er
f
o
r
m
in
g
s
ig
n
if
ican
tly
wo
r
s
e
o
n
s
o
m
e
o
t
h
er
task
s
.
I
t
is
p
r
ac
tically
im
p
o
s
s
ib
le
to
p
r
ed
ict
in
ad
v
an
ce
wh
ich
s
o
lv
er
s
h
o
u
ld
b
e
u
s
ed
in
a
g
iv
en
s
itu
atio
n
,
s
o
th
e
ch
o
ice
o
f
s
o
lv
er
th
at
b
est
s
u
it
s
s
o
lv
in
g
a
p
ar
ticu
lar
p
r
o
b
lem
is
d
eter
m
in
ed
ex
p
er
im
e
n
tally
.
2
.
3
.
H
a
s
h f
un
ct
io
n H
B
C
-
256
T
h
e
cr
y
p
t
o
g
r
a
p
h
ic
alg
o
r
ith
m
ch
o
s
en
f
o
r
test
in
g
u
s
in
g
m
o
d
er
n
SAT
s
o
lv
er
s
was
th
e
HB
C
-
2
5
6
d
ata
h
ash
in
g
alg
o
r
ith
m
,
d
ev
elo
p
ed
in
th
e
I
n
f
o
r
m
atio
n
Secu
r
ity
L
ab
o
r
ato
r
y
o
f
th
e
I
n
s
titu
te
o
f
I
n
f
o
r
m
atio
n
an
d
C
o
m
p
u
tatio
n
al
T
ec
h
n
o
lo
g
ies
o
f
th
e
Min
is
tr
y
o
f
Scien
c
e
an
d
Hig
h
e
r
E
d
u
ca
tio
n
o
f
th
e
R
ep
u
b
lic
o
f
Kaz
ak
h
s
tan
.
T
h
e
HB
C
-
2
5
6
h
ash
f
u
n
ctio
n
was
b
u
ilt
u
s
in
g
th
e
Me
r
k
le
-
Dam
g
ar
d
c
o
n
s
tr
u
ct
io
n
with
th
e
wid
e
-
p
ip
e
m
o
d
if
icatio
n
,
wh
ich
is
o
n
e
o
f
th
e
m
o
s
t
co
m
m
o
n
m
o
d
if
icatio
n
s
.
T
o
en
s
u
r
e
o
n
e
-
w
ay
n
ess
,
th
e
Dav
ies
-
Me
y
er
s
ch
em
e
was
em
p
l
o
y
ed
.
T
h
e
alg
o
r
ith
m
HB
C
-
2
5
6
co
n
s
is
ts
o
f
4
r
o
u
n
d
s
,
an
d
th
e
le
n
g
th
o
f
th
e
r
esu
ltin
g
Evaluation Warning : The document was created with Spire.PDF for Python.
I
n
t J E
lec
&
C
o
m
p
E
n
g
I
SS
N:
2088
-
8
7
0
8
A
p
p
lica
tio
n
o
f
s
a
tis
fia
b
ilit
y
p
r
o
b
lem
s
o
lvers
fo
r
a
s
s
ess
in
g
th
e
s
tr
en
g
th
o
f
…
(
K
u
n
b
o
la
t A
l
g
a
z
y
)
3195
h
ash
v
alu
e
is
2
5
6
b
its
.
T
h
e
co
m
p
r
ess
io
n
f
u
n
ctio
n
u
tili
ze
d
in
th
is
alg
o
r
ith
m
is
b
ased
o
n
a
p
r
o
p
r
ietar
y
b
lo
ck
cip
h
er
ca
lled
C
F,
wh
ich
was
d
esig
n
ed
with
co
n
s
id
er
atio
n
o
f
r
e
q
u
ir
em
e
n
ts
f
o
r
en
cr
y
p
tio
n
alg
o
r
ith
m
s
in
s
o
f
twar
e
an
d
h
a
r
d
war
e
im
p
le
m
en
tatio
n
s
[
2
5
]
.
T
h
e
in
p
u
t
a
n
d
o
u
tp
u
t
b
lo
ck
len
g
th
s
o
f
th
e
c
o
m
p
r
ess
io
n
f
u
n
ctio
n
C
F,
as we
ll a
s
th
e
r
o
u
n
d
k
ey
l
en
g
th
,
ar
e
all
1
2
8
b
its
.
T
o
en
h
an
ce
th
e
p
er
f
o
r
m
an
ce
,
th
e
s
tr
u
ctu
r
e
o
f
th
e
HB
C
-
2
5
6
h
ash
in
g
alg
o
r
ith
m
is
d
esig
n
e
d
to
allo
w
th
e
ad
ju
s
tm
en
t
o
f
th
e
n
u
m
b
e
r
o
f
in
p
u
t
b
lo
ck
s
h
ash
ed
s
im
u
ltan
eo
u
s
ly
in
p
ar
allel
s
tr
ea
m
s
.
T
h
is
n
u
m
b
er
is
d
eter
m
in
ed
b
y
th
e
p
ar
am
eter
k
,
wh
ich
r
an
g
es
f
r
o
m
3
to
8
.
T
h
e
v
alu
e
o
f
p
ar
am
ete
r
k
is
s
elec
ted
b
ased
o
n
th
e
v
o
lu
m
e
o
f
d
ata
b
ei
n
g
h
ash
e
d
an
d
th
e
av
ailab
le
c
o
m
p
u
tatio
n
al
r
eso
u
r
ce
s
o
f
th
e
co
m
p
u
t
er
u
s
ed
.
T
h
u
s
,
th
e
p
ar
am
eter
k
d
ef
i
n
es
th
e
len
g
th
L
o
f
th
e
in
p
u
t
b
l
o
ck
f
o
r
th
e
H
B
C
-
2
5
6
h
ash
in
g
alg
o
r
ith
m
,
w
h
er
e
L=1
2
8
×k
b
its
.
T
h
e
s
tr
u
ctu
r
e
of
th
e
h
ash
in
g
al
g
o
r
ith
m
is
s
h
o
wn
in
Fig
u
r
e
1.
T
h
e
HB
C
-
2
5
6
alg
o
r
ith
m
u
n
d
er
co
n
s
id
er
atio
n
,
k
n
o
wn
f
o
r
its
h
ig
h
le
v
el
o
f
s
ec
u
r
ity
,
en
h
an
ce
d
p
er
f
o
r
m
an
ce
,
an
d
s
u
itab
ilit
y
f
o
r
h
ar
d
war
e
im
p
lem
en
tati
o
n
u
s
in
g
p
a
r
allel
co
m
p
u
tati
o
n
s
,
is
ex
ten
s
iv
ely
d
escr
ib
ed
in
[
2
6
]
.
T
h
is
p
a
p
er
p
r
o
v
i
d
es
d
etailed
r
esu
lts
o
f
co
n
d
u
cte
d
r
esear
ch
o
n
a
v
alan
ch
e
ef
f
ec
ts
,
s
tr
ict
av
alan
ch
e
ef
f
ec
ts
,
an
d
s
tatis
tical
s
ec
u
r
ity
.
Ad
d
itio
n
ally
,
wo
r
k
s
[
2
7
]
,
[
2
8
]
p
r
esen
t
co
n
clu
s
io
n
s
o
n
th
e
im
p
r
ac
ticality
o
f
u
s
in
g
m
eth
o
d
s
s
u
ch
as
d
if
f
er
en
tial,
lin
ea
r
,
an
d
alg
eb
r
aic
cr
y
p
tan
aly
s
is
to
f
in
d
co
llis
io
n
s
in
th
e
HB
C
-
2
5
6
f
u
n
ctio
n
.
I
n
o
u
r
ca
s
e,
wh
en
p
r
e
p
ar
in
g
ex
p
er
im
en
tal
d
ata,
we
u
s
ed
th
e
v
a
lu
e
k=
3
.
T
h
u
s
,
th
e
len
g
th
L
o
f
t
h
e
in
p
u
t b
lo
ck
o
f
t
h
e
alg
o
r
ith
m
is
3
8
4
b
its
.
Fig
u
r
e
1
.
T
h
e
s
ch
em
e
of
th
e
H
B
C
-
256
h
ash
in
g
alg
o
r
ith
m
3.
RE
SU
L
T
S AN
D
D
I
SCU
SS
I
O
N
T
h
e
T
r
an
s
alg
tr
a
n
s
lato
r
tak
es
as
in
p
u
t
a
p
r
o
g
r
a
m
th
at
co
m
p
u
tes
a
d
is
cr
ete
f
u
n
ctio
n
,
wr
itten
in
a
s
p
ec
ialized
p
r
o
ce
d
u
r
al
p
r
o
g
r
a
m
m
in
g
lan
g
u
ag
e
(
T
A
lan
g
u
a
g
e)
.
T
h
e
r
esu
lt
o
f
tr
an
s
latin
g
a
T
A
p
r
o
g
r
a
m
is
a
s
y
s
tem
o
f
B
o
o
lean
eq
u
ati
o
n
s
t
h
at
en
co
d
e
th
e
co
m
p
u
tatio
n
p
r
o
ce
s
s
o
f
th
e
co
n
s
id
er
ed
f
u
n
ct
io
n
.
T
h
e
p
h
ases
o
f
tex
t
an
aly
s
is
o
f
th
e
T
A
p
r
o
g
r
a
m
,
co
n
s
tr
u
ctin
g
a
s
y
n
ta
x
tr
ee
,
an
d
tr
av
er
s
in
g
t
h
e
r
esu
ltin
g
tr
e
e
f
o
r
in
ter
p
r
etatio
n
ar
e
im
p
lem
en
ted
i
n
a
s
tan
d
ar
d
m
an
n
er
.
A
n
o
n
-
tr
iv
ial
asp
ec
t o
f
th
e
tr
an
s
latio
n
is
th
e
p
r
o
ce
d
u
r
e
f
o
r
in
ter
p
r
etin
g
th
e
lan
g
u
a
g
e
co
n
s
tr
u
cts,
as
t
h
is
s
tep
is
r
esp
o
n
s
ib
le
f
o
r
g
en
er
atin
g
th
e
s
y
s
tem
o
f
B
o
o
lean
eq
u
atio
n
s
th
at
en
co
d
e
th
e
alg
o
r
ith
m
'
s
ex
ec
u
tio
n
p
r
o
ce
s
s
.
At
th
is
s
tag
e,
n
u
m
er
o
u
s
lo
ca
l
p
r
o
b
lem
s
ar
is
e,
th
e
r
eso
lu
tio
n
o
f
wh
ich
ca
n
s
ig
n
if
ican
tly
af
f
ec
t
b
o
th
th
e
s
ize
an
d
s
tr
u
ctu
r
e
o
f
t
h
e
r
esu
ltin
g
co
d
e.
As
m
en
tio
n
ed
a
b
o
v
e
,
th
e
T
r
an
s
alg
s
o
f
twar
e
s
u
ite
was
u
s
ed
to
tr
an
s
f
o
r
m
th
is
alg
o
r
it
h
m
in
to
a
B
o
o
lean
f
o
r
m
u
la.
I
n
itially
,
u
s
in
g
th
e
s
p
ec
ialized
p
r
o
g
r
am
m
in
g
lan
g
u
ag
e
T
A,
wh
ich
is
p
ar
t
o
f
th
e
T
r
an
s
alg
s
o
f
twar
e
s
u
ite,
a
p
r
o
g
r
am
co
d
e
was
wr
itten
to
im
p
lem
en
t
all
th
e
o
p
er
atio
n
s
p
e
r
f
o
r
m
ed
b
y
th
e
alg
o
r
ith
m
.
T
h
ese
o
p
er
atio
n
s
in
clu
d
e
b
y
te
p
er
m
u
tatio
n
,
b
itwis
e
cy
clic
s
h
if
t,
s
u
b
s
titu
tio
n
p
r
o
ce
d
u
r
e
u
s
in
g
f
o
u
r
1
6
-
b
y
te
S
-
b
o
x
es,
b
y
te
-
wis
e
XOR
o
p
er
atio
n
,
an
d
a
d
d
itio
n
o
f
elem
e
n
ts
f
r
o
m
s
elec
ted
r
o
ws
an
d
c
o
lu
m
n
s
o
f
th
e
m
atr
i
x
.
Evaluation Warning : The document was created with Spire.PDF for Python.
I
SS
N
:
2
0
8
8
-
8
7
0
8
I
n
t J E
lec
&
C
o
m
p
E
n
g
,
Vo
l.
15
,
No
.
3
,
J
u
n
e
20
25
:
3
1
9
1
-
3
2
0
1
3196
T
h
en
,
th
e
te
x
t
o
f
th
is
p
r
o
g
r
a
m
was
p
ass
ed
to
th
e
p
ar
s
in
g
m
o
d
u
le
o
f
th
e
T
r
an
s
alg
s
o
f
twar
e
s
u
ite,
th
e
r
esu
lt
o
f
wh
ich
is
a
s
y
n
tax
tr
ee
d
escr
ib
i
n
g
th
e
in
ter
n
al
r
ep
r
esen
tatio
n
o
f
th
is
p
r
o
g
r
am
.
T
r
av
er
s
al
o
f
th
e
s
y
n
tax
tr
ee
a
n
d
co
n
s
tr
u
ctio
n
o
f
B
o
o
lean
eq
u
a
tio
n
s
ar
e
p
er
f
o
r
m
ed
b
y
th
e
tr
an
s
f
o
r
m
atio
n
m
o
d
u
le.
W
h
en
g
en
er
atin
g
th
e
f
in
al
p
r
o
p
o
s
itio
n
al
co
d
e,
th
e
tr
an
s
it
io
n
to
C
NF
is
ca
r
r
ied
o
u
t
u
s
in
g
T
s
eitin
tr
an
s
f
o
r
m
atio
n
s
[
2
9
]
.
As
a
r
esu
lt
o
f
th
e
p
r
o
p
o
s
itio
n
al
en
co
d
in
g
o
f
th
e
HB
C
-
2
5
6
h
ash
in
g
alg
o
r
ith
m
,
a
B
o
o
lean
f
o
r
m
u
la
in
C
NF
was
o
b
tain
ed
,
co
n
tain
in
g
1
9
6
,
8
6
4
B
o
o
lean
v
ar
iab
les
an
d
co
n
s
is
tin
g
o
f
9
8
6
,
4
8
0
clau
s
es,
ea
ch
o
f
wh
ich
r
ep
r
esen
ts
a
d
is
ju
n
ctio
n
o
f
liter
als.
T
h
e
to
tal
n
u
m
b
er
o
f
liter
als,
i.e
.
,
B
o
o
lean
v
ar
iab
les o
r
th
eir
n
eg
atio
n
s
,
in
clu
d
ed
in
th
ese
clau
s
es,
is
3
,
3
2
1
,
8
8
0
.
T
ab
le
1
s
h
o
ws
th
e
n
u
m
b
er
o
f
B
o
o
lean
v
ar
iab
les,
liter
als,
an
d
clau
s
es
d
ep
en
d
in
g
o
n
th
e
n
u
m
b
er
o
f
r
o
u
n
d
s
o
f
t
h
e
HB
C
-
2
5
6
h
ash
f
u
n
ctio
n
.
T
ab
le
1
.
Nu
m
b
er
o
f
B
o
o
lean
v
ar
iab
les,
liter
als,
an
d
clau
s
es
in
th
e
B
o
o
lean
f
o
r
m
u
la
d
escr
ib
in
g
t
h
e
HB
C
-
2
5
6
h
ash
f
u
n
ctio
n
N
u
mb
e
r
o
f
r
o
u
n
d
s
N
u
mb
e
r
o
f
v
a
r
i
a
b
l
e
s
N
u
mb
e
r
o
f
l
i
t
e
r
a
l
s
N
u
mb
e
r
o
f
c
l
a
u
ses
1
4
7
,
2
3
2
7
9
1
,
4
6
4
2
3
5
,
0
2
4
2
9
7
,
0
2
4
1
,
6
3
3
,
9
1
2
4
8
5
,
1
6
8
3
1
4
6
,
9
4
4
2
,
4
7
7
,
8
9
6
7
3
5
,
8
2
4
4
1
9
6
,
8
6
4
3
,
3
2
1
,
8
8
0
9
8
6
,
4
8
0
On
ce
th
e
p
r
o
p
o
s
itio
n
al
r
ep
r
es
en
tatio
n
o
f
t
h
e
HB
C
-
2
5
6
h
ash
in
g
alg
o
r
ith
m
is
o
b
tain
e
d
,
d
ep
en
d
in
g
o
n
th
e
p
r
o
b
lem
b
ei
n
g
s
o
lv
e
d
,
it
is
n
ec
ess
ar
y
to
ass
ig
n
v
alu
es
to
th
e
in
p
u
t
v
ar
iab
les,
ea
ch
co
r
r
esp
o
n
d
in
g
to
a
s
p
ec
if
ic
b
it
o
f
th
e
in
p
u
t
b
lo
c
k
o
f
th
e
h
ash
ed
m
ess
ag
e,
an
d
th
e
o
u
t
p
u
t
v
ar
ia
b
les,
ea
ch
co
r
r
esp
o
n
d
in
g
t
o
a
s
p
ec
if
ic
b
it
o
f
th
e
h
ash
co
d
e.
Af
ter
th
at,
a
s
er
ies
o
f
test
s
ar
e
p
er
f
o
r
m
ed
u
s
in
g
s
ix
m
o
d
er
n
SAT
s
o
lv
er
s
to
o
b
tain
in
f
o
r
m
atio
n
ab
o
u
t th
e
c
o
m
p
u
tatio
n
r
u
n
tim
e,
m
em
o
r
y
u
s
ag
e,
an
d
o
th
er
e
x
p
er
im
e
n
tal
d
ata.
Dep
en
d
in
g
o
n
wh
eth
er
i
n
p
u
t
an
d
/o
r
o
u
tp
u
t
v
ar
iab
le
v
alu
es
ar
e
s
p
ec
if
ied
,
SAT
s
o
lv
er
s
ca
n
s
o
lv
e
th
e
f
o
llo
win
g
4
task
s
:
a.
I
f
n
eith
e
r
in
p
u
t
v
ar
iab
le
v
alu
es
n
o
r
o
u
tp
u
t
v
ar
iab
le
v
alu
es
ar
e
s
p
ec
if
ie
d
,
r
an
d
o
m
in
p
u
t
v
ar
iab
le
v
alu
es
(
in
p
u
t
m
ess
ag
e)
ar
e
g
en
er
at
ed
,
an
d
th
en
th
e
c
o
r
r
esp
o
n
d
in
g
o
u
tp
u
t
v
ar
iab
le
v
alu
es
(
h
ash
co
d
e)
a
r
e
co
m
p
u
ted
.
b.
I
f
in
p
u
t
v
a
r
iab
le
v
alu
es
(
in
p
u
t
m
ess
ag
e)
an
d
o
u
tp
u
t
v
ar
iab
le
v
alu
es
(
h
ash
co
d
e)
ar
e
s
p
ec
if
ied
,
th
e
task
o
f
h
ash
co
d
e
v
er
if
icatio
n
is
s
o
lv
e
d
.
c.
I
f
o
n
ly
i
n
p
u
t
v
ar
iab
le
v
alu
es
(
in
p
u
t
m
ess
ag
e)
ar
e
s
p
ec
if
ie
d
,
th
e
task
o
f
c
o
m
p
u
tin
g
th
e
v
alu
es
o
f
th
e
co
r
r
esp
o
n
d
in
g
o
u
tp
u
t v
ar
iab
le
s
(
h
ash
co
d
e)
is
s
o
lv
ed
.
d.
I
f
o
n
ly
o
u
t
p
u
t
v
ar
iab
le
v
alu
es
(
h
ash
co
d
e)
ar
e
s
p
ec
if
ied
,
th
e
task
o
f
co
m
p
u
tin
g
th
e
v
alu
es
o
f
th
e
co
r
r
esp
o
n
d
in
g
i
n
p
u
t
v
ar
iab
les
(
in
p
u
t m
ess
ag
e)
is
s
o
lv
ed
.
T
h
e
f
ir
s
t
th
r
ee
task
s
,
f
r
o
m
th
e
p
er
s
p
ec
tiv
e
o
f
SAT
s
o
lv
er
s
,
ar
e
tr
iv
ial
an
d
ca
n
b
e
s
o
lv
ed
in
ju
s
t
a
f
ew
s
ec
o
n
d
s
.
Ho
wev
er
,
th
e
f
o
u
r
t
h
task
(
p
r
e
-
im
ag
e
s
ea
r
ch
)
,
wh
ich
is
o
f
t
h
e
g
r
ea
test
in
t
er
est
in
ter
m
s
o
f
cr
y
p
tan
aly
s
is
,
ca
n
n
o
t
b
e
s
o
lv
ed
in
a
r
ea
s
o
n
ab
le
am
o
u
n
t
o
f
tim
e.
T
h
is
is
n
atu
r
al
b
ec
au
s
e
an
y
h
ash
f
u
n
ctio
n
m
u
s
t
b
e
r
esis
tan
t
to
p
r
e
-
im
ag
e
attac
k
s
.
On
e
o
f
th
e
c
o
m
m
o
n
ly
u
s
ed
tech
n
iq
u
es
wh
en
em
p
l
o
y
in
g
SAT
s
o
lv
er
s
is
Gu
ess
-
an
d
-
Dete
r
m
in
e,
wh
i
ch
in
v
o
lv
es
f
ix
in
g
th
e
v
alu
es
o
f
ce
r
tain
v
ar
iab
les,
s
ig
n
if
ic
an
tly
r
ed
u
cin
g
th
e
o
v
er
all
tim
e
r
eq
u
ir
ed
to
f
in
d
a
s
o
lu
tio
n
to
th
e
cr
y
p
tan
aly
s
is
task
at
h
an
d
.
T
h
er
ef
o
r
e,
we
will
s
im
p
lify
o
u
r
task
b
y
s
p
ec
if
y
i
n
g
,
i
n
ad
d
itio
n
to
t
h
e
o
u
t
p
u
t
v
a
r
iab
le
v
alu
es
(
h
as
h
co
d
e
)
,
th
e
v
alu
es
o
f
ce
r
tain
i
n
p
u
t
v
ar
iab
les,
an
d
th
en
attem
p
t to
f
i
n
d
th
e
v
alu
es
o
f
th
e
r
em
ain
in
g
in
p
u
t
v
ar
iab
l
es u
s
in
g
a
SAT
s
o
lv
er
.
T
h
e
co
m
p
u
tatio
n
s
wer
e
p
er
f
o
r
m
ed
u
n
d
er
t
h
e
co
n
d
itio
n
t
h
at
t
h
e
o
u
t
p
u
t
v
a
r
iab
le
v
alu
es,
r
ep
r
esen
tin
g
a
256
-
b
it
h
ash
v
alu
e,
wer
e
f
u
ll
y
k
n
o
wn
.
I
n
p
u
t
v
ar
iab
le
v
alu
es
r
ep
r
esen
tin
g
a
3
8
4
-
b
it
p
lain
tex
t
b
lo
ck
wer
e
p
r
o
v
id
e
d
,
with
in
itial
b
its
m
is
s
in
g
,
wh
er
e
1
≤
≤
30
.
T
h
e
task
is
to
f
in
d
th
e
v
al
u
es
o
f
th
e
in
p
u
t
v
ar
iab
les
co
r
r
esp
o
n
d
in
g
to
th
e
m
is
s
in
g
b
its
u
s
in
g
SAT
s
o
lv
er
s
an
d
t
h
er
eb
y
f
u
lly
r
ec
o
v
e
r
th
e
o
r
ig
i
n
al
m
ess
ag
e
b
lo
ck
.
Fo
r
ex
p
e
r
im
en
ts
aim
ed
at
test
in
g
th
e
r
esil
ien
ce
o
f
th
e
HB
C
-
2
5
6
alg
o
r
ith
m
ag
ai
n
s
t
th
is
ty
p
e
o
f
attac
k
,
th
r
ee
s
eq
u
en
tial
SAT
s
o
lv
er
s
wer
e
s
elec
ted
:
C
aDi
C
aL
(
1
.
6
.
0
)
,
L
i
n
g
elin
g
(
s
c2
0
2
2
)
,
a
n
d
Kis
s
at
(
1
.
0
.
3
)
,
alo
n
g
with
th
r
ee
p
ar
allel
SAT
s
o
lv
er
s
:
Pli
n
g
elin
g
(
s
c2
0
2
2
)
,
T
r
ee
n
g
elin
g
(
s
c2
0
2
2
)
,
an
d
Par
k
is
s
at
(
1
.
0
.
3
)
[
3
0
]
,
[
3
1
]
.
T
h
ese
s
o
lv
er
s
h
av
e
at
v
a
r
io
u
s
tim
es
ac
h
iev
ed
to
p
r
an
k
in
g
s
in
t
h
e
a
n
n
u
al
SAT
co
m
p
etitio
n
.
T
a
b
le
2
s
h
o
ws
th
e
tim
e
tak
en
to
f
in
d
th
e
m
is
s
in
g
b
its
o
f
th
e
o
r
ig
in
al
m
ess
ag
e
u
s
in
g
t
h
e
af
o
r
e
m
en
tio
n
e
d
SAT
s
o
lv
e
r
s
.
As
ca
n
b
e
s
ee
n
f
r
o
m
th
is
tab
le,
it
is
p
r
ef
er
ab
le
to
u
s
e
p
ar
allel
SAT
s
o
lv
er
s
to
s
o
lv
e
o
u
r
p
r
o
b
lem
.
Am
o
n
g
th
e
p
ar
allel
SAT
s
o
lv
er
s
(
f
o
r
o
u
r
p
r
o
b
lem
)
,
th
e
m
o
s
t
ef
f
icien
t
o
n
e
was
th
e
Par
k
is
s
at
SAT
s
o
lv
er
,
s
o
i
t
will
b
e
u
s
ed
in
f
u
r
th
er
e
x
p
er
i
m
en
ts
.
E
m
p
ty
ce
lls
in
th
e
tab
le
in
d
icate
th
at
th
e
ex
ec
u
tio
n
tim
e
ex
ce
ed
ed
th
e
estab
lis
h
ed
lim
it.
No
w,
we
will
co
n
d
u
ct
a
s
er
ies
o
f
ex
p
e
r
im
en
ts
to
d
eter
m
in
e
t
h
e
r
esis
tan
ce
o
f
th
e
HB
C
-
2
5
6
h
ash
in
g
alg
o
r
ith
m
to
p
r
eim
ag
e
attac
k
s
u
s
in
g
o
n
e,
two
,
th
r
ee
,
an
d
f
o
u
r
r
o
u
n
d
s
o
f
th
e
h
ash
i
n
g
f
u
n
ctio
n
.
T
ab
le
3
p
r
esen
ts
th
e
s
o
lu
tio
n
s
ea
r
ch
tim
e
u
s
in
g
th
e
Par
k
is
s
at
SAT
s
o
lv
er
,
an
d
Fig
u
r
e
2
s
h
o
ws
th
e
d
y
n
am
ics
o
f
th
is
tim
e
d
ep
en
d
i
n
g
o
n
th
e
n
u
m
b
e
r
o
f
u
n
k
n
o
wn
v
ar
ia
b
les f
o
r
f
o
u
r
r
o
u
n
d
s
.
Evaluation Warning : The document was created with Spire.PDF for Python.
I
n
t J E
lec
&
C
o
m
p
E
n
g
I
SS
N:
2088
-
8
7
0
8
A
p
p
lica
tio
n
o
f
s
a
tis
fia
b
ilit
y
p
r
o
b
lem
s
o
lvers
fo
r
a
s
s
ess
in
g
th
e
s
tr
en
g
th
o
f
…
(
K
u
n
b
o
la
t A
l
g
a
z
y
)
3197
T
ab
le
2
.
T
im
e
t
o
f
in
d
th
e
s
p
ec
if
ied
n
u
m
b
er
o
f
p
lain
tex
t
b
its
(
in
s
ec
o
n
d
s
)
N
u
mb
e
r
o
f
u
n
k
n
o
w
n
b
i
t
s
(
n
)
S
A
T
S
o
l
v
e
r
s
S
e
q
u
e
n
t
i
a
l
P
a
r
a
l
l
e
l
C
a
D
i
C
a
L
Li
n
g
e
l
i
n
g
K
i
ss
a
t
P
a
r
k
i
ss
a
t
P
l
i
n
g
e
l
i
n
g
Tr
e
e
n
g
e
l
i
n
g
1
0
.
3
7
8
.
3
0
0
.
5
2
2
.
5
1
1
.
2
0
8
.
5
4
2
0
.
6
4
8
.
5
6
1
.
0
9
4
.
9
2
9
.
1
0
8
.
6
2
3
0
.
7
1
8
.
0
0
1
7
5
.
3
0
4
.
9
6
1
.
3
0
8
.
8
1
4
0
.
7
5
2
1
.
5
6
8
5
9
.
1
6
4
.
8
1
1
2
.
2
0
6
9
.
9
0
5
1
.
1
5
2
3
.
1
8
4
4
0
9
.
9
8
4
.
8
2
4
.
2
0
7
2
.
3
3
6
1
.
6
2
5
3
.
1
8
1
4
9
9
.
5
3
4
.
7
4
3
9
.
8
0
9
2
.
4
0
7
2
.
2
8
-
1
0
0
9
.
5
5
4
.
7
1
6
.
7
0
8
2
.
0
1
8
3
.
1
9
-
1
0
6
9
4
.
7
6
4
.
6
1
1
3
.
5
0
3
6
.
0
3
9
6
.
9
5
-
6
5
0
7
7
.
7
6
4
.
9
9
3
2
.
2
0
3
9
.
4
6
10
1
0
.
8
2
-
1
1
7
6
.
1
7
5
.
2
1
2
.
5
0
1
3
7
.
1
5
11
2
1
.
0
3
-
1
5
8
9
8
2
.
2
6
6
.
2
1
1
3
.
5
0
6
3
.
9
5
12
5
1
.
5
6
-
4
1
8
6
6
.
3
8
7
.
1
5
1
1
.
5
0
8
9
.
5
0
13
3
7
.
0
9
-
2
1
6
1
0
.
3
0
7
.
8
7
1
5
.
7
0
1
7
4
.
9
7
14
5
4
.
3
8
-
8
2
3
3
.
9
8
1
5
.
3
2
3
2
.
4
0
1
8
2
.
3
6
15
3
4
9
.
8
3
-
3
0
1
3
5
.
1
8
1
9
.
4
9
3
3
.
5
0
1
0
8
.
6
3
16
5
3
.
1
4
-
3
9
5
1
.
0
8
2
8
.
6
3
2
2
.
7
0
6
4
6
.
7
8
17
-
-
5
9
3
6
.
5
8
4
3
.
5
1
6
1
.
2
0
-
18
-
-
-
1
3
2
.
5
4
6
1
.
4
0
-
19
-
-
-
1
6
2
.
5
7
2
5
9
.
6
0
-
20
-
-
-
2
2
4
.
3
1
5
4
.
5
0
-
21
-
-
-
4
6
6
.
2
6
1
3
0
9
.
7
0
-
22
-
-
-
9
8
2
.
0
4
1
4
8
0
.
7
0
-
23
-
-
-
2
1
3
6
.
7
5
4
4
8
.
9
0
-
24
-
-
-
2
6
9
1
.
5
4
2
0
4
3
.
5
0
-
25
-
-
-
1
4
6
4
0
.
4
7
5
5
8
2
2
.
0
0
-
26
-
-
-
2
3
3
6
1
.
0
6
2
2
4
7
9
.
3
0
-
27
-
-
-
7
2
8
8
2
.
6
8
-
-
28
-
-
-
9
5
3
2
0
.
1
9
-
-
29
-
-
-
1
8
0
6
6
0
.
1
1
-
-
30
-
-
-
3
1
5
6
7
4
.
7
6
-
-
T
ab
le
3
.
So
lu
tio
n
s
ea
r
ch
tim
e
u
s
in
g
th
e
Par
k
is
s
at
SAT
s
o
lv
er
(
in
s
ec
o
n
d
s
)
N
u
mb
e
r
o
f
u
n
k
n
o
w
n
b
i
t
s
(
n
)
S
o
l
u
t
i
o
n
s
e
a
r
c
h
t
i
me
1
r
o
u
n
d
2
r
o
u
n
d
s
3
r
o
u
n
d
s
4
r
o
u
n
d
s
1
2
.
1
6
2
.
1
8
2
.
4
8
2
.
5
1
2
1
.
7
3
2
.
8
2
3
.
7
8
4
.
9
2
3
1
.
8
0
2
.
8
4
3
.
8
5
4
.
9
6
4
1
.
7
6
2
.
7
2
3
.
8
5
4
.
8
1
5
1
.
7
5
2
.
8
1
3
.
7
3
4
.
8
6
1
.
7
1
2
.
7
1
3
.
9
2
4
.
7
4
7
1
.
7
6
2
.
7
4
3
.
7
9
4
.
7
8
1
.
7
5
2
.
6
9
3
.
9
5
4
.
6
1
9
1
.
7
3
2
.
8
0
4
.
2
7
4
.
9
9
10
1
.
7
4
2
.
7
0
5
.
2
8
5
.
2
11
1
.
7
6
2
.
8
8
4
.
8
4
6
.
2
1
12
1
.
7
3
2
.
6
5
6
.
0
1
7
.
1
5
13
1
.
5
5
2
.
9
3
6
.
4
6
7
.
8
7
14
1
.
8
5
4
.
1
8
7
.
9
1
1
5
.
3
2
15
1
.
9
9
4
.
5
8
1
0
.
4
3
1
9
.
4
9
16
2
.
5
1
4
.
9
2
1
1
.
4
4
2
8
.
6
3
17
4
.
1
9
9
.
2
5
2
6
.
1
1
4
3
.
5
1
18
6
.
1
9
1
0
.
5
5
3
8
.
8
3
1
3
2
.
5
4
19
1
1
.
9
8
1
2
.
8
5
7
0
.
1
6
1
6
2
.
5
7
20
3
6
.
4
5
2
5
.
1
8
1
6
8
.
7
3
2
2
4
.
3
1
21
4
2
.
9
2
6
7
.
7
9
3
2
0
.
0
2
4
6
6
.
2
6
22
4
7
.
5
8
1
1
3
.
7
6
5
1
4
.
4
4
9
8
2
.
0
4
23
7
7
.
7
7
3
4
7
.
7
1
1
,
2
5
7
.
4
6
2
1
3
6
.
7
5
24
3
8
9
.
8
5
7
4
9
.
3
5
1
,
3
2
9
.
3
9
2
6
9
1
.
5
4
25
6
9
4
.
8
8
1
,
1
0
0
.
2
6
3
,
8
4
8
.
1
7
1
4
6
4
0
.
4
7
26
1
,
6
3
2
.
6
6
2
,
0
3
8
.
3
5
6
,
2
7
8
.
9
1
2
3
3
6
1
.
0
6
27
2
,
4
8
9
.
2
1
4
,
2
6
9
.
4
7
2
0
,
4
8
8
.
2
5
7
2
8
8
2
.
6
8
28
4
,
9
9
7
.
6
6
9
,
9
8
4
.
8
0
7
6
,
0
4
7
.
9
4
9
5
3
2
0
.
1
9
29
1
9
,
3
0
4
.
9
5
2
7
,
8
4
2
.
2
2
8
7
,
1
0
1
.
2
2
1
8
0
6
6
0
.
1
1
30
5
2
,
0
6
2
.
8
5
6
3
,
3
9
8
.
3
5
1
7
4
,
2
7
6
.
9
7
3
1
5
6
7
4
.
7
6
Evaluation Warning : The document was created with Spire.PDF for Python.
I
SS
N
:
2
0
8
8
-
8
7
0
8
I
n
t J E
lec
&
C
o
m
p
E
n
g
,
Vo
l.
15
,
No
.
3
,
J
u
n
e
20
25
:
3
1
9
1
-
3
2
0
1
3198
I
t
is
n
ec
ess
ar
y
to
n
o
te
th
e
f
o
ll
o
win
g
n
u
an
ce
.
W
h
en
r
u
n
n
in
g
th
e
s
am
e
SAT
s
o
lv
er
m
u
ltip
le
tim
es
with
th
e
s
am
e
in
p
u
t
a
n
d
o
u
tp
u
t
d
a
ta,
we
o
b
tain
d
i
f
f
er
en
t
tim
es
ea
ch
tim
e.
T
h
is
is
b
ec
au
s
e,
a
t
ea
ch
s
tep
o
f
th
e
alg
o
r
ith
m
f
o
r
s
o
l
v
in
g
t
h
e
B
o
o
lean
eq
u
atio
n
,
th
e
s
elec
tio
n
o
f
th
e
n
e
x
t
v
a
r
iab
le
f
o
r
s
u
b
s
eq
u
en
t
ass
ig
n
m
en
t
o
f
th
e
v
alu
e
“t
r
u
e”
o
r
“f
alse”
is
m
ad
e
u
s
in
g
a
r
an
d
o
m
n
u
m
b
er
g
en
e
r
ato
r
.
I
f
th
e
v
ar
ia
b
le
i
s
“lu
ck
ily
”
ch
o
s
en
,
m
ea
n
in
g
th
e
v
alu
e
ch
o
s
en
f
o
r
it
is
p
ar
t
o
f
th
e
s
o
lu
tio
n
,
th
is
p
o
s
itiv
ely
af
f
ec
ts
th
e
s
ea
r
ch
tim
e.
Oth
er
wis
e,
it
will b
e
n
ec
ess
ar
y
to
r
etu
r
n
to
th
is
v
ar
iab
le
an
d
ass
ig
n
it th
e
o
p
p
o
s
ite
v
alu
e,
an
d
th
e
n
r
ep
ea
t
th
e
s
o
lu
tio
n
s
ea
r
ch
p
r
o
ce
d
u
r
e
(
a
b
ac
k
tr
ac
k
in
g
m
e
ch
an
is
m
)
.
Fo
r
ex
am
p
le,
s
ea
r
c
h
in
g
f
o
r
th
e
v
alu
es
o
f
2
5
u
n
k
n
o
wn
v
ar
iab
les
u
s
in
g
th
e
Par
k
is
s
at
SAT
s
o
lv
er
ca
n
tak
e
f
r
o
m
4
9
m
in
u
tes to
1
5
h
o
u
r
s
,
wh
er
e
th
ey
a
r
e
s
h
o
wn
i
n
T
ab
le
4
.
T
o
o
b
tain
a
r
ea
lis
tic
ass
e
s
s
m
e
n
t o
f
tim
e,
it is
n
ec
ess
ar
y
to
r
e
p
ea
t th
e
s
am
e
ex
p
er
im
e
n
t m
u
lt
ip
le
tim
es,
f
o
r
ex
a
m
p
le,
1
0
tim
es,
an
d
th
en
f
in
d
th
e
av
e
r
ag
e
tim
e
s
p
e
n
t.
I
n
o
u
r
ca
s
e,
th
e
av
er
a
g
e
tim
e
to
f
in
d
a
s
o
lu
tio
n
was
2
3
,
3
6
1
.
0
6
s
ec
o
n
d
s
,
o
r
6
h
o
u
r
s
,
2
9
m
i
n
u
tes,
an
d
2
1
.
0
6
s
e
co
n
d
s
.
As
ev
i
d
en
t
f
r
o
m
T
ab
le
3
an
d
th
e
g
r
ap
h
in
Fig
u
r
e
2
,
with
an
in
cr
ea
s
e
in
th
e
n
u
m
b
e
r
o
f
u
n
k
n
o
wn
b
its
(
s
tar
tin
g
f
r
o
m
2
5
an
d
a
b
o
v
e
)
,
th
e
tim
e
r
eq
u
ir
ed
to
s
o
lv
e
th
e
p
r
o
b
lem
s
h
a
r
p
ly
in
c
r
ea
s
es.
I
t
to
o
k
o
v
er
8
7
h
o
u
r
s
u
s
in
g
a
co
m
p
u
ter
with
two
5
6
-
co
r
e
p
r
o
ce
s
s
o
r
s
to
f
in
d
th
e
p
r
eim
a
g
e
o
f
th
e
m
e
s
s
ag
e,
ass
u
m
in
g
th
at
3
0
u
n
k
n
o
wn
b
its
wer
e
p
r
esen
t
wh
ile
th
e
v
alu
es
o
f
th
e
r
em
ain
in
g
3
5
4
b
its
wer
e
f
ix
e
d
.
T
h
e
ex
p
e
r
im
en
ts
wer
e
co
n
d
u
cted
o
n
a
c
o
m
p
u
te
r
with
two
5
6
-
co
r
e
AM
D
E
PYC
7
6
6
3
p
r
o
ce
s
s
o
r
s
r
u
n
n
in
g
at
2
.
0
GHz
ea
ch
(
to
tal
o
f
1
1
2
c
o
r
es)
a
n
d
1
2
8
GB
o
f
R
A
M,
o
p
e
r
atin
g
o
n
th
e
L
in
u
x
Ub
u
n
tu
2
2
.
0
4
.
3
L
T
S o
p
er
atin
g
s
y
s
tem
.
Fig
u
r
e
2
.
Dy
n
am
ics o
f
s
o
lu
tio
n
s
ea
r
ch
tim
e
u
s
in
g
t
h
e
Par
k
is
s
at
SAT
s
o
lv
er
T
ab
le
4
.
Sear
ch
tim
e
f
o
r
v
alu
e
s
o
f
2
5
u
n
k
n
o
wn
B
o
o
lea
n
v
ar
i
ab
les
A
t
t
e
m
p
t
n
u
m
b
e
r
S
e
a
r
c
h
t
i
me
(
h
,
m
,
s)
(
sec
o
n
d
s)
A
t
t
e
m
p
t
#
1
2
h
5
2
m
2
1
.
4
2
s
1
0
,
3
4
1
.
4
2
A
t
t
e
m
p
t
#
2
5
h
2
2
m
0
0
.
0
7
s
1
9
,
3
2
0
.
0
7
A
t
t
e
m
p
t
#
3
2
h
3
5
m
5
1
.
1
7
s
9
,
3
5
1
.
1
7
A
t
t
e
m
p
t
#
4
7
h
3
9
m
4
9
.
8
5
s
2
7
,
5
8
9
.
8
5
A
t
t
e
m
p
t
#
5
49
m
3
0
.
0
7
s
2
,
9
7
0
.
0
7
A
t
t
e
m
p
t
#
6
1
h
5
6
m
1
2
.
9
3
s
6
,
9
7
2
.
9
3
A
t
t
e
m
p
t
#
7
15
h
0
8
m
0
7
.
9
8
s
5
4
,
4
8
7
.
9
8
A
t
t
e
m
p
t
#
8
13
h
5
2
m
3
0
.
5
7
s
4
9
,
9
5
0
.
5
7
A
t
t
e
m
p
t
#
9
3
h
2
5
m
1
5
.
6
4
s
1
2
,
3
1
5
.
6
4
A
t
t
e
m
p
t
#
1
0
11
h
1
1
m
5
0
.
5
5
s
4
0
,
3
1
0
.
5
5
4.
CO
NCLU
SI
O
N
T
h
e
s
tu
d
y
u
n
d
er
to
o
k
a
p
r
ac
ti
ca
l
cr
y
p
tan
al
y
s
is
o
f
th
e
c
r
y
p
t
o
g
r
ap
h
ic
h
ash
f
u
n
ctio
n
HB
C
-
2
5
6
.
T
h
e
4
-
r
o
u
n
d
co
m
p
r
ess
io
n
f
u
n
ctio
n
was
d
escr
ib
ed
in
th
e
f
o
r
m
o
f
an
eq
u
atio
n
in
C
NF
=
1
f
o
r
m
at
u
s
in
g
9
8
6
,
4
8
0
clau
s
es,
ea
ch
o
f
wh
ich
r
ep
r
esen
ts
a
co
n
ju
n
ctio
n
o
f
liter
als an
d
1
9
6
,
8
6
4
B
o
o
lean
v
ar
iab
les.
T
h
e
s
o
lu
tio
n
to
th
is
eq
u
atio
n
was o
b
tain
e
d
u
s
in
g
th
e
SAT
s
o
lv
er
Par
k
is
s
at.
T
h
e
r
esu
lts
o
f
t
h
e
ex
p
er
im
en
ta
l
s
tu
d
ies
s
h
o
w
th
at
f
o
r
th
e
f
u
ll
HB
C
-
2
5
6
h
ash
f
u
n
ctio
n
co
n
s
i
s
tin
g
o
f
4
r
o
u
n
d
s
,
th
e
SAT
s
o
lv
er
s
tr
u
g
g
les
to
s
o
lv
e
th
e
p
r
o
b
lem
ev
e
n
wh
en
o
n
ly
3
0
b
its
o
f
th
e
o
r
ig
in
al
m
ess
ag
e
ar
e
u
n
k
n
o
wn
.
Sin
ce
f
in
d
in
g
th
e
p
r
eim
ag
e
r
eq
u
ir
es
d
eter
m
in
i
n
g
all
3
8
4
b
its
o
f
th
e
o
r
ig
in
al
m
ess
ag
e
b
lo
ck
,
th
is
task
is
p
r
ac
tically
in
f
e
asib
le
with
in
a
r
ea
s
o
n
ab
le
tim
e
f
r
a
m
e.
T
h
er
ef
o
r
e,
it
ca
n
b
e
c
o
n
clu
d
e
d
th
at
th
e
HB
C
-
2
5
6
alg
o
r
ith
m
is
r
esis
tan
t to
p
r
eim
ag
e
attac
k
s
u
s
in
g
th
is
m
eth
o
d
.
Evaluation Warning : The document was created with Spire.PDF for Python.
I
n
t J E
lec
&
C
o
m
p
E
n
g
I
SS
N:
2088
-
8
7
0
8
A
p
p
lica
tio
n
o
f
s
a
tis
fia
b
ilit
y
p
r
o
b
lem
s
o
lvers
fo
r
a
s
s
ess
in
g
th
e
s
tr
en
g
th
o
f
…
(
K
u
n
b
o
la
t A
l
g
a
z
y
)
3199
A
lim
itatio
n
o
f
SAT
s
o
lv
er
s
is
th
eir
b
r
u
te
-
f
o
r
ce
n
atu
r
e,
a
n
d
t
h
e
p
r
o
b
lem
o
f
r
ed
u
cin
g
th
e
s
e
ar
ch
s
p
ac
e
is
f
u
n
d
am
en
tal
to
th
ese
m
eth
o
d
s
.
A
s
o
lu
tio
n
m
ig
h
t
n
o
t
b
e
f
o
u
n
d
with
in
an
ac
ce
p
tab
le
tim
e
f
r
am
e,
m
ak
in
g
it
p
r
ac
tically
im
p
o
s
s
ib
le
to
p
r
o
v
i
d
e
a
th
eo
r
etica
l
esti
m
ate
o
f
th
e
p
o
s
s
ib
ilit
y
o
f
f
in
d
in
g
a
p
r
ei
m
ag
e.
T
h
er
ef
o
r
e,
as
a
f
u
tu
r
e
r
esear
c
h
d
ir
ec
tio
n
,
i
t
s
h
o
u
ld
b
e
n
o
te
d
th
at
o
th
e
r
ty
p
es
o
f
c
r
y
p
ta
n
aly
s
es
an
d
th
eir
co
m
b
in
atio
n
s
,
in
clu
d
in
g
th
e
co
m
b
i
n
atio
n
o
f
d
if
f
er
en
tial
a
n
d
alg
eb
r
aic
cr
y
p
tan
aly
s
is
,
will
b
e
ex
p
lo
r
e
d
to
o
b
tain
a
th
eo
r
etica
l
esti
m
ate
o
f
th
e
s
tr
en
g
th
o
f
th
e
co
n
s
id
er
ed
h
ash
f
u
n
cti
o
n
.
F
UNDING
I
NF
O
R
M
A
T
I
O
N
T
h
e
r
esear
ch
wo
r
k
was
f
u
n
d
e
d
b
y
th
e
Min
is
tr
y
o
f
Scien
ce
a
n
d
Hig
h
er
E
d
u
ca
tio
n
o
f
Kaz
a
k
h
s
tan
an
d
ca
r
r
ied
o
u
t
with
in
th
e
f
r
am
e
wo
r
k
o
f
th
e
p
r
o
ject
B
R
2
4
9
9
3
0
5
2
“De
v
elo
p
m
e
n
t
an
d
s
tu
d
y
o
f
c
r
y
p
t
o
g
r
ap
h
ic
alg
o
r
ith
m
s
f
o
r
in
f
o
r
m
atio
n
p
r
o
tectio
n
in
r
eso
u
r
ce
-
co
n
s
tr
ain
ed
s
y
s
tem
s
an
d
ev
alu
atio
n
o
f
t
h
eir
s
tr
en
g
th
”
at
th
e
I
n
s
titu
te
o
f
I
n
f
o
r
m
atio
n
an
d
C
o
m
p
u
tatio
n
al
T
e
ch
n
o
l
o
g
ies.
AUTHO
R
CO
NT
RI
B
UT
I
O
NS ST
A
T
E
M
E
N
T
T
h
is
jo
u
r
n
al
u
s
es
th
e
C
o
n
tr
ib
u
to
r
R
o
les
T
ax
o
n
o
m
y
(
C
R
ed
iT)
to
r
ec
o
g
n
ize
in
d
iv
id
u
al
au
th
o
r
co
n
tr
ib
u
tio
n
s
,
r
ed
u
ce
au
th
o
r
s
h
ip
d
is
p
u
tes,
an
d
f
ac
ilit
ate
co
llab
o
r
atio
n
.
Na
m
e
of
A
u
t
h
o
r
C
M
So
Va
Fo
I
R
D
O
E
Vi
Su
P
Fu
Ku
n
b
o
lat
Alg
az
y
✓
✓
✓
✓
✓
✓
Kair
at
Sak
an
✓
✓
✓
✓
✓
An
d
r
ey
Var
e
n
n
ik
o
v
✓
✓
✓
✓
✓
✓
Nu
r
s
u
lu
Kap
alo
v
a
✓
✓
✓
✓
✓
C
:
C
o
n
c
e
p
t
u
a
l
i
z
a
t
i
o
n
M
:
M
e
t
h
o
d
o
l
o
g
y
So
:
So
f
t
w
a
r
e
Va
:
Va
l
i
d
a
t
i
o
n
Fo
:
Fo
r
mal
a
n
a
l
y
s
i
s
I
:
I
n
v
e
s
t
i
g
a
t
i
o
n
R
:
R
e
so
u
r
c
e
s
D
:
D
a
t
a
C
u
r
a
t
i
o
n
O
:
W
r
i
t
i
n
g
-
O
r
i
g
i
n
a
l
D
r
a
f
t
E
:
W
r
i
t
i
n
g
-
R
e
v
i
e
w
&
E
d
i
t
i
n
g
Vi
:
Vi
su
a
l
i
z
a
t
i
o
n
Su
:
Su
p
e
r
v
i
s
i
o
n
P
:
P
r
o
j
e
c
t
a
d
mi
n
i
st
r
a
t
i
o
n
Fu
:
Fu
n
d
i
n
g
a
c
q
u
i
si
t
i
o
n
CO
NF
L
I
C
T
O
F
I
N
T
E
R
E
S
T
ST
A
T
E
M
E
NT
Au
th
o
r
s
s
tate
n
o
co
n
f
lict o
f
in
t
er
est.
DATA AV
AI
L
AB
I
L
I
T
Y
−
T
h
e
d
a
t
a
t
h
a
t
s
u
p
p
o
r
t
t
h
e
f
i
n
d
i
n
g
s
o
f
t
h
i
s
s
t
u
d
y
a
r
e
a
v
a
il
a
b
l
e
o
n
r
e
q
u
e
s
t
f
r
o
m
t
h
e
c
o
r
r
e
s
p
o
n
d
in
g
a
u
t
h
o
r
,
K
S
.
−
Der
iv
ed
d
ata
s
u
p
p
o
r
tin
g
th
e
f
in
d
in
g
s
o
f
th
is
s
tu
d
y
ar
e
a
v
ai
lab
le
f
r
o
m
t
h
e
co
r
r
esp
o
n
d
in
g
au
th
o
r
,
KS
,
on
r
eq
u
est.
−
T
h
e
d
ata
th
at
s
u
p
p
o
r
t
th
e
f
in
d
in
g
s
o
f
th
is
s
tu
d
y
ar
e
av
ailab
le
f
r
o
m
th
e
co
r
r
esp
o
n
d
i
n
g
a
u
th
o
r
,
KS,
u
p
o
n
r
ea
s
o
n
ab
le
r
eq
u
est.
RE
F
E
R
E
NC
E
S
[
1
]
F
.
M
a
ssa
c
c
i
a
n
d
L.
M
a
r
r
a
r
o
,
“
L
o
g
i
c
a
l
c
r
y
p
t
a
n
a
l
y
s
i
s
a
s
a
S
A
T
p
r
o
b
l
e
m
:
e
n
c
o
d
i
n
g
a
n
d
a
n
a
l
y
si
s
o
f
t
h
e
U
.
S
.
d
a
t
a
e
n
c
r
y
p
t
i
o
n
st
a
n
d
a
r
d
,
”
J
o
u
r
n
a
l
o
f
A
u
t
o
m
a
t
e
d
R
e
a
s
o
n
i
n
g
,
v
o
l
.
2
4
,
n
o
.
1
–
2
,
p
p
.
1
6
5
–
2
0
3
,
2
0
0
0
,
d
o
i
:
1
0
.
1
0
2
3
/
a
:
1
0
0
6
3
2
6
7
2
3
0
0
2
.
[
2
]
K
.
H
u
a
n
d
Z.
C
h
u
,
“
A
n
e
f
f
i
c
i
e
n
t
c
i
r
c
u
i
t
-
b
a
se
d
S
A
T
s
o
l
v
e
r
a
n
d
i
t
s
a
p
p
l
i
c
a
t
i
o
n
i
n
l
o
g
i
c
e
q
u
i
v
a
l
e
n
c
e
c
h
e
c
k
i
n
g
,
”
Mi
c
r
o
e
l
e
c
t
r
o
n
i
c
s
J
o
u
rn
a
l
,
v
o
l
.
1
4
2
,
p
.
1
0
6
0
0
5
,
D
e
c
.
2
0
2
3
,
d
o
i
:
1
0
.
1
0
1
6
/
j
.
m
e
j
o
.
2
0
2
3
.
1
0
6
0
0
5
.
[
3
]
K
.
B
u
ñ
o
a
n
d
H
.
A
d
o
r
n
a
,
“
S
o
l
v
i
n
g
3
-
S
A
T
i
n
d
i
st
r
i
b
u
t
e
d
P
sy
s
t
e
ms
w
i
t
h
s
t
r
i
n
g
o
b
j
e
c
t
s,
”
T
h
e
o
re
t
i
c
a
l
C
o
m
p
u
t
e
r
S
c
i
e
n
c
e
,
v
o
l
.
9
6
4
,
p
.
1
1
3
9
7
6
,
J
u
l
.
2
0
2
3
,
d
o
i
:
1
0
.
1
0
1
6
/
j
.
t
c
s.2
0
2
3
.
1
1
3
9
7
6
.
[
4
]
C
.
M
.
L
i
,
F
.
X
i
a
o
,
M
.
L
u
o
,
F
.
M
a
n
y
à
,
Z.
L
ü
,
a
n
d
Y
.
Li
,
“
C
l
a
u
s
e
v
i
v
i
f
i
c
a
t
i
o
n
b
y
u
n
i
t
p
r
o
p
a
g
a
t
i
o
n
i
n
C
D
C
L
S
A
T
s
o
l
v
e
r
s,”
Ar
t
i
f
i
c
i
a
l
I
n
t
e
l
l
i
g
e
n
c
e
,
v
o
l
.
2
7
9
,
p
.
1
0
3
1
9
7
,
F
e
b
.
2
0
2
0
,
d
o
i
:
1
0
.
1
0
1
6
/
j
.
a
r
t
i
n
t
.
2
0
1
9
.
1
0
3
1
9
7
.
[
5
]
L.
C
h
e
n
g
a
n
d
L.
F
e
n
g
,
“
M
o
d
e
l
a
b
s
t
r
a
c
t
i
o
n
f
o
r
d
i
s
c
r
e
t
e
-
e
v
e
n
t
s
y
st
e
ms
u
si
n
g
a
S
A
T
s
o
l
v
e
r
,
”
I
E
EE
Ac
c
e
ss
,
v
o
l
.
1
1
,
p
p
.
1
7
3
3
4
–
1
7
3
4
7
,
2
0
2
3
,
d
o
i
:
1
0
.
1
1
0
9
/
A
C
C
ESS
.
2
0
2
3
.
3
2
4
6
1
2
3
.
[
6
]
A
.
E.
J.
H
y
v
ä
r
i
n
e
n
a
n
d
N
.
M
a
n
t
h
e
y
,
“
D
e
si
g
n
i
n
g
sc
a
l
a
b
l
e
p
a
r
a
l
l
e
l
S
A
T
so
l
v
e
r
s,”
i
n
L
e
c
t
u
r
e
N
o
t
e
s
i
n
C
o
m
p
u
t
e
r
S
c
i
e
n
c
e
(
i
n
c
l
u
d
i
n
g
su
b
s
e
ri
e
s
L
e
c
t
u
re
N
o
t
e
s
i
n
Ar
t
i
f
i
c
i
a
l
I
n
t
e
l
l
i
g
e
n
c
e
a
n
d
L
e
c
t
u
r
e
N
o
t
e
s
i
n
Bi
o
i
n
f
o
rm
a
t
i
c
s)
,
v
o
l
.
7
3
1
7
LN
C
S
,
S
p
r
i
n
g
e
r
B
e
r
l
i
n
H
e
i
d
e
l
b
e
r
g
,
2
0
1
2
,
p
p
.
2
1
4
–
2
2
7
,
d
o
i
:
1
0
.
1
0
0
7
/
9
7
8
-
3
-
6
4
2
-
3
1
6
1
2
-
8
_
1
7
.
[
7
]
N
.
A
l
a
m
g
i
r
,
S
.
N
e
j
a
t
i
,
a
n
d
C
.
B
r
i
g
h
t
,
“
S
H
A
-
2
5
6
C
o
l
l
i
si
o
n
A
t
t
a
c
k
w
i
t
h
P
r
o
g
r
a
m
mat
i
c
S
A
T
,
”
C
EU
R
W
o
rks
h
o
p
Pro
c
e
e
d
i
n
g
s
,
v
o
l
.
3
7
1
7
,
p
p
.
9
1
–
1
1
0
,
2
0
2
4
.
[
8
]
S
.
N
e
j
a
t
i
a
n
d
V
.
G
a
n
e
s
h
,
“
C
D
C
L(
C
r
y
p
t
o
)
S
A
T
s
o
l
v
e
r
s
f
o
r
c
r
y
p
t
a
n
a
l
y
s
i
s,”
C
AS
C
O
N
2
0
1
9
P
ro
c
e
e
d
i
n
g
s
-
C
o
n
f
e
r
e
n
c
e
o
f
t
h
e
C
e
n
t
r
e
f
o
r
Ad
v
a
n
c
e
d
S
t
u
d
i
e
s
o
n
C
o
l
l
a
b
o
ra
t
i
v
e
Re
s
e
a
r
c
h
-
Pro
c
e
e
d
i
n
g
s
o
f
t
h
e
2
9
t
h
An
n
u
a
l
I
n
t
e
r
n
a
t
i
o
n
a
l
C
o
n
f
e
re
n
c
e
o
n
C
o
m
p
u
t
e
r
S
c
i
e
n
c
e
a
n
d
S
o
f
t
w
a
re
E
n
g
i
n
e
e
r
i
n
g
,
p
p
.
3
1
1
–
3
1
6
,
2
0
2
0
.
Evaluation Warning : The document was created with Spire.PDF for Python.
I
SS
N
:
2
0
8
8
-
8
7
0
8
I
n
t J E
lec
&
C
o
m
p
E
n
g
,
Vo
l.
15
,
No
.
3
,
J
u
n
e
20
25
:
3
1
9
1
-
3
2
0
1
3200
[
9
]
A
.
B
i
e
r
e
,
“
L
i
n
g
e
l
i
n
g
,
P
l
i
n
g
e
l
i
n
g
a
n
d
Tr
e
e
n
g
e
l
i
n
g
e
n
t
e
r
i
n
g
t
h
e
S
A
T
c
o
m
p
e
t
i
t
i
o
n
2
0
1
3
,
”
i
n
Pro
c
e
e
d
i
n
g
s
o
f
S
AT
C
o
m
p
e
t
i
t
i
o
n
2
0
1
3
,
2
0
1
3
,
p
p
.
5
1
–
52
.
[
1
0
]
I
.
O
t
p
u
s
c
h
e
n
n
i
k
o
v
,
A
.
S
e
me
n
o
v
,
I
.
G
r
i
b
a
n
o
v
a
,
O
.
Za
i
k
i
n
,
a
n
d
S
.
K
o
c
h
e
ma
z
o
v
,
“
E
n
c
o
d
i
n
g
c
r
y
p
t
o
g
r
a
p
h
i
c
f
u
n
c
t
i
o
n
s
t
o
S
A
T
u
si
n
g
TR
A
N
S
A
LG
s
y
st
e
m,
”
F
ro
n
t
i
e
rs
i
n
A
rt
i
f
i
c
i
a
l
I
n
t
e
l
l
i
g
e
n
c
e
a
n
d
A
p
p
l
i
c
a
t
i
o
n
s
,
v
o
l
.
2
8
5
,
p
p
.
1
5
9
4
–
1
5
9
5
,
2
0
1
6
,
d
o
i
:
1
0
.
3
2
3
3
/
9
7
8
-
1
-
6
1
4
9
9
-
6
7
2
-
9
-
1
5
9
4
.
[
1
1
]
S
.
C
a
i
,
X
.
Z
h
a
n
g
,
M
.
F
l
e
u
r
y
,
a
n
d
A
.
B
i
e
r
e
,
“
B
e
t
t
e
r
d
e
c
i
s
i
o
n
h
e
u
r
i
s
t
i
c
s
i
n
C
D
C
L
t
h
r
o
u
g
h
l
o
c
a
l
s
e
a
r
c
h
a
n
d
t
a
r
g
e
t
p
h
a
ses,
”
J
o
u
rn
a
l
o
f
Art
i
f
i
c
i
a
l
I
n
t
e
l
l
i
g
e
n
c
e
Re
s
e
a
rc
h
,
v
o
l
.
7
4
,
p
p
.
1
5
1
5
–
1
5
6
3
,
A
u
g
.
2
0
2
2
,
d
o
i
:
1
0
.
1
6
1
3
/
JA
I
R
.
1
.
1
3
6
6
6
.
[
1
2
]
C
.
B
r
i
g
h
t
,
I
.
K
o
t
si
r
e
a
s,
a
n
d
V
.
G
a
n
e
sh
,
“
A
p
p
l
y
i
n
g
c
o
mp
u
t
e
r
a
l
g
e
b
r
a
s
y
s
t
e
ms
w
i
t
h
S
A
T
s
o
l
v
e
r
s
t
o
t
h
e
W
i
l
l
i
a
mso
n
c
o
n
j
e
c
t
u
r
e
,
”
J
o
u
rn
a
l
o
f
S
y
m
b
o
l
i
c
C
o
m
p
u
t
a
t
i
o
n
,
v
o
l
.
1
0
0
,
p
p
.
1
8
7
–
2
0
9
,
S
e
p
.
2
0
2
0
,
d
o
i
:
1
0
.
1
0
1
6
/
j
.
j
sc
.
2
0
1
9
.
0
7
.
0
2
4
.
[
1
3
]
D
.
Lo
v
e
l
a
n
d
,
A
.
S
a
b
h
a
r
w
a
l
,
a
n
d
B
.
S
e
l
ma
n
,
“
D
P
LL
:
T
h
e
c
o
r
e
o
f
m
o
d
e
r
n
s
a
t
i
sf
i
a
b
i
l
i
t
y
so
l
v
e
r
s,”
i
n
O
u
t
s
t
a
n
d
i
n
g
C
o
n
t
r
i
b
u
t
i
o
n
s
t
o
L
o
g
i
c
,
v
o
l
.
1
0
,
S
p
r
i
n
g
e
r
I
n
t
e
r
n
a
t
i
o
n
a
l
P
u
b
l
i
s
h
i
n
g
,
2
0
1
6
,
p
p
.
3
1
5
–
3
3
5
,
d
o
i
:
1
0
.
1
0
0
7
/
9
7
8
-
3
-
3
1
9
-
4
1
8
4
2
-
1
_
1
2
.
[
1
4
]
E.
M
a
r
o
,
“
M
o
d
e
l
i
n
g
o
f
a
l
g
e
b
r
a
i
c
a
n
a
l
y
si
s
o
f
P
R
ES
EN
T
c
i
p
h
e
r
b
y
S
A
T
so
l
v
e
r
s,
”
I
O
P
C
o
n
f
e
r
e
n
c
e
S
e
r
i
e
s:
Ma
t
e
r
i
a
l
s
S
c
i
e
n
c
e
a
n
d
En
g
i
n
e
e
ri
n
g
,
v
o
l
.
7
3
4
,
n
o
.
1
,
p
.
1
2
1
0
1
,
Ja
n
.
2
0
2
0
,
d
o
i
:
1
0
.
1
0
8
8
/
1
7
5
7
-
8
9
9
X
/
7
3
4
/
1
/
0
1
2
1
0
1
.
[
1
5
]
E.
M
a
r
o
,
“
A
l
g
e
b
r
a
i
c
a
n
a
l
y
s
i
s
o
f
S
M
4
c
i
p
h
e
r
u
s
i
n
g
S
a
g
e
M
a
t
h
,
”
I
O
P
C
o
n
f
e
re
n
c
e
S
e
ri
e
s:
M
a
t
e
ri
a
l
s
S
c
i
e
n
c
e
a
n
d
E
n
g
i
n
e
e
ri
n
g
,
v
o
l
.
1
0
4
7
,
n
o
.
1
,
p
.
1
2
0
8
6
,
F
e
b
.
2
0
2
1
,
d
o
i
:
1
0
.
1
0
8
8
/
1
7
5
7
-
8
9
9
X
/
1
0
4
7
/
1
/
0
1
2
0
8
6
.
[
1
6
]
C
.
A
n
s
ó
t
e
g
u
i
,
M
.
L.
B
o
n
e
t
,
J
.
G
i
r
á
l
d
e
z
-
C
r
u
,
J.
L
e
v
y
,
a
n
d
L.
S
i
m
o
n
,
“
C
o
m
mu
n
i
t
y
st
r
u
c
t
u
r
e
i
n
i
n
d
u
s
t
r
i
a
l
S
A
T
i
n
st
a
n
c
e
s
,
”
J
o
u
r
n
a
l
o
f
Art
i
f
i
c
i
a
l
I
n
t
e
l
l
i
g
e
n
c
e
Re
s
e
a
rc
h
,
v
o
l
.
6
6
,
p
p
.
4
4
3
–
4
7
2
,
O
c
t
.
2
0
1
9
,
d
o
i
:
1
0
.
1
6
1
3
/
j
a
i
r
.
1
.
1
1
7
4
1
.
[
1
7
]
P
.
M
.
B
i
t
t
n
e
r
,
T.
Th
ü
m
,
a
n
d
I
.
S
c
h
a
e
f
e
r
,
“
S
A
T
e
n
c
o
d
i
n
g
s
o
f
t
h
e
a
t
-
mo
s
t
-
k
c
o
n
st
r
a
i
n
t
:
a
c
a
s
e
s
t
u
d
y
o
n
c
o
n
f
i
g
u
r
i
n
g
u
n
i
v
e
r
si
t
y
c
o
u
r
ses,
”
i
n
L
e
c
t
u
re
N
o
t
e
s
i
n
C
o
m
p
u
t
e
r
S
c
i
e
n
c
e
(
i
n
c
l
u
d
i
n
g
s
u
b
s
e
ri
e
s
L
e
c
t
u
re
N
o
t
e
s
i
n
Ar
t
i
f
i
c
i
a
l
I
n
t
e
l
l
i
g
e
n
c
e
a
n
d
L
e
c
t
u
r
e
N
o
t
e
s
i
n
Bi
o
i
n
f
o
rm
a
t
i
c
s)
,
v
o
l
.
1
1
7
2
4
LN
C
S
,
S
p
r
i
n
g
e
r
I
n
t
e
r
n
a
t
i
o
n
a
l
P
u
b
l
i
sh
i
n
g
,
2
0
1
9
,
p
p
.
1
2
7
–
1
4
4
,
d
o
i
:
1
0
.
1
0
0
7
/
9
7
8
-
3
-
030
-
3
0
4
4
6
-
1
_
7
.
[
1
8
]
J.
H
.
Li
a
n
g
,
V
.
G
a
n
e
sh
,
P
.
P
o
u
p
a
r
t
,
a
n
d
K
.
C
z
a
r
n
e
c
k
i
,
“
L
e
a
r
n
i
n
g
r
a
t
e
b
a
sed
b
r
a
n
c
h
i
n
g
h
e
u
r
i
st
i
c
f
o
r
S
A
T
so
l
v
e
r
s,
”
i
n
L
e
c
t
u
r
e
N
o
t
e
s
i
n
C
o
m
p
u
t
e
r
S
c
i
e
n
c
e
(
i
n
c
l
u
d
i
n
g
s
u
b
ser
i
e
s
L
e
c
t
u
r
e
N
o
t
e
s
i
n
Art
i
f
i
c
i
a
l
I
n
t
e
l
l
i
g
e
n
c
e
a
n
d
L
e
c
t
u
re
N
o
t
e
s
i
n
Bi
o
i
n
f
o
rm
a
t
i
c
s)
,
v
o
l
.
9
7
1
0
,
S
p
r
i
n
g
e
r
I
n
t
e
r
n
a
t
i
o
n
a
l
P
u
b
l
i
sh
i
n
g
,
2
0
1
6
,
p
p
.
1
2
3
–
140
,
d
o
i
:
1
0
.
1
0
0
7
/
9
7
8
-
3
-
3
1
9
-
4
0
9
7
0
-
2
_
9
.
[
1
9
]
R
.
G
.
B
i
y
a
s
h
e
v
,
A
.
S
mo
l
a
r
z
,
K
.
T.
A
l
g
a
z
y
,
a
n
d
A
.
K
h
o
m
p
y
sh
,
“
En
c
r
y
p
t
i
o
n
a
l
g
o
r
i
t
h
m
‘
Q
A
M
A
L
N
P
N
S
’
b
a
se
d
o
n
a
n
o
n
p
o
s
i
t
i
o
n
a
l
p
o
l
y
n
o
mi
a
l
n
o
t
a
t
i
o
n
,
”
J
o
u
rn
a
l
o
f
Ma
t
h
e
m
a
t
i
c
s,
M
e
c
h
a
n
i
c
s
a
n
d
C
o
m
p
u
t
e
r
S
c
i
e
n
c
e
,
v
o
l
.
1
0
5
,
n
o
.
1
,
A
p
r
.
2
0
2
0
,
d
o
i
:
1
0
.
2
6
5
7
7
/
j
mm
c
s.
2
0
2
0
.
v
1
0
5
.
i
1
.
1
7
.
[
2
0
]
M
.
J.
H
.
H
e
u
l
e
,
O
.
K
u
l
l
m
a
n
n
,
S
.
W
i
e
r
i
n
g
a
,
a
n
d
A
.
B
i
e
r
e
,
“
C
u
b
e
a
n
d
c
o
n
q
u
e
r
:
G
u
i
d
i
n
g
C
D
C
L
S
A
T
so
l
v
e
r
s
b
y
l
o
o
k
a
h
e
a
d
s,”
i
n
L
e
c
t
u
re
N
o
t
e
s
i
n
C
o
m
p
u
t
e
r
S
c
i
e
n
c
e
(
i
n
c
l
u
d
i
n
g
s
u
b
ser
i
e
s
L
e
c
t
u
r
e
N
o
t
e
s
i
n
Art
i
f
i
c
i
a
l
I
n
t
e
l
l
i
g
e
n
c
e
a
n
d
L
e
c
t
u
re
N
o
t
e
s
i
n
Bi
o
i
n
f
o
rm
a
t
i
c
s)
,
v
o
l
.
7
2
6
1
LN
C
S
,
S
p
r
i
n
g
e
r
B
e
r
l
i
n
H
e
i
d
e
l
b
e
r
g
,
2
0
1
2
,
p
p
.
5
0
–
65
,
d
o
i
:
1
0
.
1
0
0
7
/
9
7
8
-
3
-
6
4
2
-
3
4
1
8
8
-
5
_
8
.
[
2
1
]
S
.
E.
K
o
c
h
e
m
a
z
o
v
a
n
d
O
.
S
.
Za
i
k
i
n
,
“
T
o
w
a
r
d
s
b
e
t
t
e
r
S
A
T
e
n
c
o
d
i
n
g
s
f
o
r
h
a
s
h
f
u
n
c
t
i
o
n
i
n
v
e
r
s
i
o
n
p
r
o
b
l
e
ms
,
”
i
n
2
0
2
4
4
7
t
h
I
C
T
a
n
d
El
e
c
t
r
o
n
i
c
s
C
o
n
v
e
n
t
i
o
n
,
MIPRO
2
0
2
4
-
Pr
o
c
e
e
d
i
n
g
s
,
M
a
y
2
0
2
4
,
p
p
.
2
5
–
30
,
d
o
i
:
1
0
.
1
1
0
9
/
M
I
P
R
O
6
0
9
6
3
.
2
0
2
4
.
1
0
5
6
9
1
9
3
.
[
2
2
]
R
.
G
.
B
i
y
a
sh
e
v
,
S
.
E.
N
y
ss
a
n
b
a
y
e
v
a
,
a
n
d
Y
.
Y
.
B
e
g
i
m
b
a
y
e
v
a
,
“
D
e
v
e
l
o
p
m
e
n
t
o
f
t
h
e
m
o
d
e
l
o
f
p
r
o
t
e
c
t
e
d
c
r
o
ss
-
b
o
r
d
e
r
i
n
f
o
r
m
a
t
i
o
n
i
n
t
e
r
a
c
t
i
o
n
,
”
O
p
e
n
E
n
g
i
n
e
e
ri
n
g
,
v
o
l
.
6
,
n
o
.
1
,
p
p
.
1
9
9
–
2
0
5
,
A
u
g
.
2
0
1
6
,
d
o
i
:
1
0
.
1
5
1
5
/
e
n
g
-
2
0
1
6
-
0
0
2
5
.
[
2
3
]
S
.
A
l
o
u
n
e
h
,
S
.
A
b
e
d
,
M
.
H
.
A
l
S
h
a
y
e
j
i
,
a
n
d
R
.
M
e
sl
e
h
,
“
A
c
o
mp
r
e
h
e
n
s
i
v
e
st
u
d
y
a
n
d
a
n
a
l
y
si
s
o
n
S
A
T
-
so
l
v
e
r
s:
a
d
v
a
n
c
e
s,
u
sa
g
e
s
a
n
d
a
c
h
i
e
v
e
me
n
t
s
,
”
Art
i
f
i
c
i
a
l
I
n
t
e
l
l
i
g
e
n
c
e
Re
v
i
e
w
,
v
o
l
.
5
2
,
n
o
.
4
,
p
p
.
2
5
7
5
–
2
6
0
1
,
M
a
r
.
2
0
1
9
,
d
o
i
:
1
0
.
1
0
0
7
/
s
1
0
4
6
2
-
0
1
8
-
9
6
2
8
-
0.
[
2
4
]
S
.
A
b
e
d
,
A
.
A
s
h
k
a
n
a
n
,
W
.
M
a
n
s
o
o
r
,
a
n
d
A
.
G
a
w
a
n
m
e
h
,
“
En
h
a
n
c
e
d
S
A
T
so
l
v
e
r
s
b
a
se
d
h
a
s
h
i
n
g
m
e
t
h
o
d
f
o
r
b
i
t
c
o
i
n
m
i
n
i
n
g
,
”
i
n
Ad
v
a
n
c
e
s
i
n
I
n
t
e
l
l
i
g
e
n
t
S
y
s
t
e
m
s
a
n
d
C
o
m
p
u
t
i
n
g
,
v
o
l
.
1
1
3
4
,
S
p
r
i
n
g
e
r
I
n
t
e
r
n
a
t
i
o
n
a
l
P
u
b
l
i
sh
i
n
g
,
2
0
2
0
,
p
p
.
1
9
1
–
1
9
8
,
d
o
i
:
1
0
.
1
0
0
7
/
9
7
8
-
3
-
0
3
0
-
4
3
0
2
0
-
7
_
2
6
.
[
2
5
]
N
.
A
.
K
a
p
a
l
o
v
a
,
K
.
S
.
S
a
k
a
n
,
A
.
H
a
u
men
,
a
n
d
S
u
l
e
i
me
n
o
v
,
“
R
e
q
u
i
r
e
m
e
n
t
s
f
o
r
sy
mm
e
t
r
i
c
b
l
o
c
k
e
n
c
r
y
p
t
i
o
n
a
l
g
o
r
i
t
h
ms
d
e
v
e
l
o
p
e
d
f
o
r
s
o
f
t
w
a
r
e
a
n
d
h
a
r
d
w
a
r
e
i
mp
l
e
m
e
n
t
a
t
i
o
n
,
”
K
a
z
N
U
Bu
l
l
e
t
i
n
.
Ma
t
h
e
m
a
t
i
c
s,
Me
c
h
a
n
i
c
s,
C
o
m
p
u
t
e
r
S
c
i
e
n
c
e
S
e
ri
e
s
,
v
o
l
.
1
1
2
,
n
o
.
4
,
p
p
.
1
3
4
–
1
4
7
,
D
e
c
.
2
0
2
1
,
d
o
i
:
1
0
.
2
6
5
7
7
/
J
M
M
C
S
.
2
0
2
1
.
v
1
1
2
.
i
4
.
1
2
.
[
2
6
]
K
.
S
a
k
a
n
,
S
.
N
y
ssa
n
b
a
y
e
v
a
,
N
.
K
a
p
a
l
o
v
a
,
K
.
A
l
g
a
z
y
,
A
.
K
h
o
m
p
y
s
h
,
a
n
d
D
.
D
y
u
s
e
n
b
a
y
e
v
,
“
D
e
v
e
l
o
p
me
n
t
a
n
d
a
n
a
l
y
si
s
o
f
t
h
e
n
e
w
h
a
s
h
i
n
g
a
l
g
o
r
i
t
h
m
b
a
se
d
o
n
b
l
o
c
k
c
i
p
h
e
r
,
”
E
a
st
e
rn
-
Eu
r
o
p
e
a
n
J
o
u
r
n
a
l
o
f
E
n
t
e
rp
r
i
se
T
e
c
h
n
o
l
o
g
i
e
s
,
v
o
l
.
2
,
n
o
.
9
–
1
1
6
,
p
p
.
6
0
–
7
3
,
A
p
r
.
2
0
2
2
,
d
o
i
:
1
0
.
1
5
5
8
7
/
1
7
2
9
-
4
0
6
1
.
2
0
2
2
.
2
5
2
0
6
0
.
[
2
7
]
K
.
A
l
g
a
z
y
,
K
.
S
a
k
a
n
,
N
.
K
a
p
a
l
o
v
a
,
S
.
N
y
ssa
n
b
a
y
e
v
a
,
a
n
d
D
.
D
y
u
se
n
b
a
y
e
v
,
“
D
i
f
f
e
r
e
n
t
i
a
l
a
n
a
l
y
si
s
o
f
a
c
r
y
p
t
o
g
r
a
p
h
i
c
h
a
s
h
i
n
g
a
l
g
o
r
i
t
h
m H
B
C
-
2
5
6
,
”
A
p
p
l
i
e
d
S
c
i
e
n
c
e
s (S
w
i
t
zer
l
a
n
d
)
,
v
o
l
.
1
2
,
n
o
.
1
9
,
p
.
1
0
1
7
3
,
O
c
t
.
2
0
2
2
,
d
o
i
:
1
0
.
3
3
9
0
/
a
p
p
1
2
1
9
1
0
1
7
3
.
[
2
8
]
K
.
A
l
g
a
z
y
,
K
.
S
a
k
a
n
,
a
n
d
N
.
K
a
p
a
l
o
v
a
,
“
Ev
a
l
u
a
t
i
o
n
o
f
t
h
e
st
r
e
n
g
t
h
a
n
d
p
e
r
f
o
r
man
c
e
o
f
a
n
e
w
h
a
sh
i
n
g
a
l
g
o
r
i
t
h
m
b
a
s
e
d
o
n
a
b
l
o
c
k
c
i
p
h
e
r
,
”
I
n
t
e
r
n
a
t
i
o
n
a
l
J
o
u
rn
a
l
o
f
E
l
e
c
t
ri
c
a
l
a
n
d
C
o
m
p
u
t
e
r
E
n
g
i
n
e
e
ri
n
g
,
v
o
l
.
1
3
,
n
o
.
3
,
p
p
.
3
1
2
4
–
3
1
3
0
,
Ju
n
.
2
0
2
3
,
d
o
i
:
1
0
.
1
1
5
9
1
/
i
j
e
c
e
.
v
1
3
i
3
.
p
p
3
1
2
4
-
3
1
3
0
.
[
2
9
]
E
.
K
u
i
t
e
r
,
S
.
K
r
i
e
t
e
r
,
C
.
S
u
n
d
e
r
m
a
n
n
,
T
.
T
h
ü
m
,
a
n
d
G
.
S
a
a
k
e
,
“
T
s
e
i
t
i
n
o
r
n
o
t
T
s
e
i
t
i
n
?
T
h
e
i
m
p
a
c
t
o
f
C
N
F
t
r
a
n
s
f
o
r
m
a
t
i
o
n
s
o
n
f
e
a
t
u
r
e
-
m
o
d
e
l
a
n
a
l
y
s
e
s
,
”
i
n
A
C
M
I
n
t
e
r
n
a
t
i
o
n
a
l
C
o
n
f
e
r
e
n
c
e
P
r
o
c
e
e
d
i
n
g
S
e
r
i
e
s
,
O
c
t
.
2
0
2
2
,
p
p
.
1
–
13
,
d
o
i
:
1
0
.
1
1
4
5
/
3
5
5
1
3
4
9
.
3
5
5
6
9
3
8
.
[
3
0
]
D
.
M
i
c
h
a
e
l
s
o
n
,
D
.
S
c
h
r
e
i
b
e
r
,
M
.
J
.
H
.
H
e
u
l
e
,
B
.
K
i
e
s
l
-
R
e
i
t
e
r
,
a
n
d
M
.
W
.
W
h
a
l
e
n
,
“
U
n
s
a
t
i
s
f
i
a
b
i
l
i
t
y
p
r
o
o
f
s
f
o
r
d
i
s
t
r
i
b
u
t
e
d
c
l
a
u
s
e
-
s
h
a
r
i
n
g
S
A
T
s
o
l
v
e
r
s
,
”
i
n
L
e
c
t
u
r
e
N
o
t
e
s
i
n
C
o
m
p
u
t
e
r
S
c
i
e
n
c
e
(
i
n
c
l
u
d
i
n
g
s
u
b
s
e
r
i
e
s
L
e
c
t
u
r
e
N
o
t
e
s
i
n
A
r
t
i
f
i
c
i
a
l
I
n
t
e
l
l
i
g
e
n
c
e
a
n
d
L
e
c
t
u
r
e
N
o
t
e
s
i
n
B
i
o
i
n
f
o
r
m
a
t
i
c
s
)
,
v
o
l
.
1
3
9
9
3
,
S
p
r
i
n
g
e
r
N
a
t
u
r
e
S
w
i
t
z
e
r
l
a
n
d
,
2
0
2
3
,
p
p
.
3
4
8
–
3
6
6
,
d
o
i
:
1
0
.
1
0
0
7
/
9
7
8
-
3
-
0
3
1
-
3
0
8
2
3
-
9
_
1
8
.
[
3
1
]
L.
Le
F
r
i
o
u
x
,
S
.
B
a
a
r
i
r
,
J.
S
o
p
e
n
a
,
a
n
d
F
.
K
o
r
d
o
n
,
“
P
a
I
n
l
e
S
S
:
a
f
r
a
me
w
o
r
k
f
o
r
p
a
r
a
l
l
e
l
S
A
T
so
l
v
i
n
g
,
”
i
n
L
e
c
t
u
re
N
o
t
e
s
i
n
C
o
m
p
u
t
e
r
S
c
i
e
n
c
e
(
i
n
c
l
u
d
i
n
g
s
u
b
seri
e
s
L
e
c
t
u
r
e
N
o
t
e
s
i
n
Art
i
f
i
c
i
a
l
I
n
t
e
l
l
i
g
e
n
c
e
a
n
d
L
e
c
t
u
r
e
N
o
t
e
s
i
n
Bi
o
i
n
f
o
rm
a
t
i
c
s)
,
v
o
l
.
1
0
4
9
1
LN
C
S
,
S
p
r
i
n
g
e
r
I
n
t
e
r
n
a
t
i
o
n
a
l
P
u
b
l
i
s
h
i
n
g
,
2
0
1
7
,
p
p
.
2
3
3
–
2
5
0
,
d
o
i
:
1
0
.
1
0
0
7
/
9
7
8
-
3
-
3
1
9
-
6
6
2
6
3
-
3
_
1
5
.
B
I
O
G
RAP
H
I
E
S O
F
AUTH
O
RS
K
u
n
b
o
l
a
t
Al
g
a
z
y
re
c
e
iv
e
d
a
m
a
ste
r
d
e
g
re
e
i
n
m
a
th
e
m
a
ti
c
s
fro
m
Al
-
F
a
ra
b
i
Ka
z
a
k
h
Na
ti
o
n
a
l
Un
i
v
e
rsity
in
2
0
0
1
a
n
d
a
P
h
.
D.
d
e
g
re
e
in
i
n
f
o
rm
a
ti
o
n
se
c
u
rit
y
sy
ste
m
s,
Alm
a
ty
,
Ka
z
a
k
h
sta
n
,
in
2
0
2
1
.
In
2
0
0
1
-
2
0
1
4
h
e
w
o
rk
e
d
i
n
in
th
e
field
o
f
in
f
o
rm
a
ti
o
n
p
ro
tec
ti
o
n
in
th
e
sta
te
str
u
c
tu
re
.
Be
twe
e
n
2
0
1
4
a
n
d
2
0
1
6
,
h
e
wo
rk
e
d
a
s
a
tea
c
h
e
r
a
t
t
h
e
De
p
a
rtme
n
t
o
f
M
a
th
e
m
a
ti
c
s
a
t
S
a
tb
a
y
e
v
Un
i
v
e
rsity
.
C
u
rre
n
tl
y
,
h
e
is
re
se
a
rc
h
e
r
in
th
e
lab
o
ra
to
r
y
“
in
f
o
rm
a
ti
o
n
se
c
u
rit
y
”
a
t
th
e
In
st
it
u
te
o
f
I
n
fo
rm
a
ti
o
n
a
n
d
C
o
m
p
u
t
in
g
Tec
h
n
o
l
o
g
y
.
His
re
se
a
rc
h
in
tere
sts
in
c
lu
d
e
c
r
y
p
t
o
g
ra
p
h
y
,
c
ry
p
tan
a
ly
sis
,
d
e
v
e
lo
p
m
e
n
t
a
n
d
r
e
se
a
rc
h
in
t
h
e
field
o
f
in
f
o
rm
a
ti
o
n
p
r
o
tec
ti
o
n
.
H
e
c
a
n
b
e
c
o
n
tac
ted
a
t
e
m
a
il
:
k
u
n
b
o
lat@m
a
il
.
ru
.
Evaluation Warning : The document was created with Spire.PDF for Python.