Game Development Reference
In-Depth 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 Sat-Horn, the satisfiability problem for propositional
Horn formulae, is Ptime-complete (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 model-checking games for first-order logic
For a logic L and a domain D of structures, the model-checking problem
asks, given a structure A ∈D and a formula ψ ∈ L , whether it is the
case that
= ψ . Model-checking problems can be reformulated in game-
theoretic terms using appropriate model-checking games. With a sentence ψ ,
a structure
A |
A
(of the same vocabulary as ψ ), we associate a model-checking
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