Game Development Reference
InDepth Information
1. (Indeed if a Horn formula contains no clause of this form, then it is
trivially satisfiable by setting all variables to false.)
It is well known that SatHorn, the satisfiability problem for propositional
Horn formulae, is Ptimecomplete (see Greenlaw et al. [1995]) and solvable
in linear time (Dowling and Gallier [1984], Itai and Makowsky [1987]). Hence
its computational properties are very similar to those of reachability games.
Actually there is a simple way of going back and forth between solving
reachability games and finding satisfying assignments for Horn formulae, so
that the two problems are solved by essentially the same algorithms.
From reachability games to Horn formulae:
Given a finite game graph
G
=
(
V,V
0
,V
1
,E
), we can construct in linear time a propositional Horn formula
ψ
G
consisting of the clauses
u ← v
for all edges (
u, v
)
∈ E
with
u ∈ V
0
, and
the clauses
u
Z
←
←
v
1
∧···∧
v
m
for all nodes
u
∈
V
1
, where
uE
=
{
v
1
,...,v
m
}
.
It is easy to see that the winning region
W
0
for Player 0 in
G
coincides with
the minimal model for
ψ
G
. Hence
v
∈
W
0
if the Horn formula
ψ
G
∧
(0
←
v
)
is unsatisfiable.
From Horn formulae to reachability games:
With a Horn formula
ψ
=
i∈I
C
i
with propositional variables
X
1
,...,X
n
and Horn clauses
C
i
of the form
Z
i
G
ψ
as follows. The positions of
Player 0 are the initial position 0 and the propositional variables
X
1
,...,X
n
,
and the positions of Player 1 are the clauses
C
i
of
ψ
. Player 0 can move from
a position
X
to any clause
C
i
with head
X
, and Player 1 can move from a
clause
C
i
to any variable occurring in the body of
C
i
. Formally,
G
ψ
=(
V,E
),
V
=
V
0
∪ V
1
with
V
0
=
{
0
}∪{X
1
,...,X
n
}
,
V
1
=
{C
i
:
i ∈ I}
, and
←
X
i
1
∧···
X
i
m
we associate a game
E
=
{
(
X, C
)
∈
V
0
×
V
1
:
X
= head(
C
)
}∪
{
(
C, X
)
∈
V
1
×
V
0
:
X
∈
body(
C
)
}
.
Player 0 has a winning strategy for
=
X
.
In particular,
ψ
is unsatisfiable if, and only if, Player 0 wins from position 0.
G
ψ
from position
X
if, and only if,
ψ

4.3.2 modelchecking games for firstorder logic
For a logic
L
and a domain
D
of structures, the
modelchecking problem
asks, given a structure A
∈D
and a formula
ψ ∈ L
, whether it is the
case that
=
ψ
. Modelchecking problems can be reformulated in game
theoretic terms using appropriate modelchecking games. With a sentence
ψ
,
a structure
A

A
(of the same vocabulary as
ψ
), we associate a
modelchecking
game
G
,ψ
). It is played by two players,
Verifier
and
Falsifier
. Verifier
(also called Player 0) tries to prove that
(
A
A

=
ψ
, whereas Falsifier (also called
Search Nedrilad ::
Custom Search