Compilation for QCSP
Igor Stéphan

arXiv:1307.4655v1 [] 17 Jul 2013

LERIA, University of Angers, France
email: igor.stephan@info.univ-angers.fr

Abstract. We propose in this article a framework for compilation of
quantified constraint satisfaction problems (QCSP). We establish the
semantics of this formalism by an interpretation to a QCSP. We specify
an algorithm to compile a QCSP embedded into a search algorithm and
based on the inductive semantics of QCSP. We introduce an optimality
property and demonstrate the optimality of the interpretation of the
compiled QCSP.

1

Introduction

A constraint satisfaction problem (CSP) requires a value, selected from a given
finite domain, to be assigned to each variable in the problem, so that all constraints relating the variables are satisfied [14,8]. A quantified constraint satisfaction problem (QCSP) [9,6] is an extension of a constraint satisfaction problem
in which some of the variables are universally quantified (since the remaining
variables are still existentially quantified). In this latter framework, variables
take value in discrete domains. Universally quantified variables may be considered to represent certain kind of uncertainty: a choice of nature or an opponent.
A QCSP can formalize many AI problems including planning under uncertainty
and playing a game against an opponent. In this second application, the goal
of the QCSP is to make a robust plan against the opponent. Whereas finding
a solution of a CSP is generally NP-complete, finding a solution for a QCSP is
generally PSPACE-complete [9].
Most of the recent decision procedure for QCSP [3,5,12,7] are based on a
search algorithm (except [18] which is based on a bottom-up approach and [13]
which is based on a translation to quantified boolean formulas) and off-line procedures (except [2] which is an on-line real-time algorithm based on Monte Carlo
game tree search and [17] which is based on standard game tree search techniques). Such an algorithm chooses a variable, branches on the different values
of the domain, verifies if the subproblems have some solutions and combines,
according to the semantics of the quantifier associated to the variable, those
solutions into a solution to the problem.
Knowledge compilation is considered in many AI applications where quick online responses are expected. In general, a knowledge base is compiled off-line into
a target language which is then used on-line to answer some queries. The goal is
to have a lesser complexity for the query computation of the compiled knowledge

base than for the initial knowledge base. This principle is for example applied in
product configuration where the set of possible configurations is compiled [1].
As far as we know, the problem of compiling a knowledge base represented
as a QCSP has not been treated but only for the related domain of quantified
Boolean formulas [16,11]. Our first contribution is a new formalism as compilation target language: the QCSP base. Our second contribution is a definition of
an optimality property for QCSP bases in order to give a polytime answer to the
next move choice problem [16] which raises the issue of whether one can change
for another solution during the game. Our third contribution is a compilation
algorithm embedded in a search algorithm which is proved to compile a QCSP
in an optimal QCSP base.
This article is organized as follows: Section 2 establishes the necessary preliminaries, section 3 presents our framework and target language for the compilation of QCSP, section 4 specifies an algorithm to compile a QCSP in our target
language, section 5 concludes with a discussion and some further works.

2

Preliminaries

Symbol ∃ stands for existential quantifier and symbol ∀ stands for universal
quantifier. Symbol ∧ stands for logical conjunction, symbol ⊤ stands for what
is always true and symbol ⊥ stands for what is always false. A QCSP is a tuple
(V, rank, quant, D, C): V is a set of n variables, rank is a bijection from V to
[1..n], quant is a mapping from V to {∃, ∀} (quant(v) is the quantifier associated
to the variable v), D is a mapping from V to a set of domains {D(v1 ), . . . , D(vn )}
where, for every variable vi ∈ V, D(vi ) is the finite domain of all the possible
values (D(v) is the domain associated to the variable v), C is a set of contraints.
If vj1 , . . . , vjm are the variables of a constraint cj ∈ C then the relation associated to cj is a subset of the Cartesian product D(vj1 ) × . . . × D(vjm ). In what
follows, we denote for every i ∈ [1..n], qi = quant(vi ) and Di = D(vi ). A QCSP
(V, rank, quant, D, C) on n variables will be denoted as follows to simplify notation:
^
q1 v1 . . . qn vn
cj
cj ∈C

with v1 ∈ D1 , . . . , vn ∈ Dn , rank(vi ) = i, for every i ∈ [1..n] ; q1 v1 . . . qn vn is
the binder.
The QCSP ({x, y, z, t}, rank, quant, {{0, 1, 2}}, C) with

rank = {(1, x), (2, y), (3, z), (4, t)},



quant = {(x, ∃), (y, ∃), (z, ∀), (t, ∃)},
D(x)
= D(y) = D(z) = D(t) = {0, 1, 2} and



C = {(x = (y ∗ z) + t)}
is, for example, denoted : ∃x∃y∀z∃t(x = (y ∗ z) + t) with x, y, z, t ∈ {0, 1, 2}.
In a binder, a maximal homogeneous sequence of quantifiers forms a bloc ;
the first one (and also the outermost) is the leftmost.

The set Ti (Q) with v1 ∈ D1 , . . . , vn ∈ Dn , Q = q1 v1 . . . qn vn for 1 ≤ i ≤ n is
the set of trees such that
– every leaf node is labeled by the symbol ✷ and is at depth i,
– every internal node at depth k, 0 ≤ k < i − 1 is labeled with the variable
vk+1 ,
– every edge linking a node at depth k to one of its children’s nodes is labeled
with an element of Dk ,
– all the labels of the edges linking a node to its children nodes are different.
The following tree is, for example, an element of the set T2 (∃x∃y∀z∃t) with
x, y, z, t ∈ {0, 1, 2} :
x
0

1

y
0 1

2

y
2

y
1

1

2

Let (V, rank, quant, D, C) be a QCSP such that V = {v1 , . . . , vn }, with
v1 ∈ D1 , . . . , vn ∈ Dn , then a scenario is the sequence of the labels val1 , . . . , valn
on the path (v1 , val1 ), . . . , (vn , valn ), vali ∈ Di for every i, 1 ≤ i ≤ n, of a tree
of Tn (q1 v1 . . . qn vn ) and a strategy is a tree of Tn (q1 v1 . . . qn vn ) such that
– every node labeled with an existentially quantified variable has a unique
child node and
– every node labeled with a universally quantified variable whose associated
domain is of size k admits k children nodes.
A scenario val1 , . . . , valn for a QCSP
V C) such that V =
V (V, rank, quant, D,
{v1 , . . . , vn } is a winning scenario if ( 1≤i≤n vi = vali ) ∧ ( cj ∈C cj ) is true ; such
a scenario corresponds to the complete instantiation [v1 ← val1 ], . . . , [vn ← valn ]
; it is a winning scenario if the instantiation satisfies all the constraints. A strategy is a winning strategy if all the scenarios are winning scenarios. If there is no
quantifier, the ✷ strategy is always a winning strategy.
The scenario 0, 0, 2, 0, which corresponds to the complete instantiation [x ←
0], [y ← 0], [z ← 2] and [t ← 0], is a winning scenario, since 0 = (0 ∗ 2) + 0. The
following strategy is a winning strategy
x
0
y
0
0

z
1

t
0

t
0

2
t
0

for the QCSP ∃x∃y∀z∃t(x = (y ∗ z) + t), x, y, z, t ∈ {0, 1, 2} since (0 =
(0 ∗ 0) + 0), (0 = (0 ∗ 1) + 0) and (0 = (0 ∗ 2) + 0).
We can give a more intuitive and recursive decision semantics for QCSP as
follows: A QCSP ∀xQC with x ∈ D admits a winning strategy if and only if, for
every val ∈ D, Q(C ∧ (x = val)) admits a winning strategy and a QCSP ∃xQC
with x ∈ D admits a winning strategy if and only if, for at least one val ∈ D,
Q(C ∧ (x = val)) admits a winning strategy.

3

Base for QCSP

From a complexity point of view and under some classical assumptions, winning
strategies are exponential in space in worst case w.r.t. the number of variables
of the QCSP [10]. But the number of winning strategies may also be exponential
in worst case. A naive way to compile a QCSP would be to store all the winning
strategies in a set but this approach is intractable in practice. For example,
the QCSP ∀x∀y∃z∃t(x = (y ∗ z) + t), x, y, z, t ∈ {0, 1, 2} admits 324 winning
strategies. Another way is to store a tree which contains only the scenarios
present in the winning strategies. This approach is not very useful too from the
knowledge representation point of view since there is no direct access to the
possibilities of an existentially quantified variable except for those of the first
bloc.
We define in this section our formalism as a target language for QCSP compilation: the QCSP base. We also define the semantics of QCSP bases in terms
of QCSP. We introduce a property of optimality for QCSP bases and prove a
very interesting result about optimal QCSP.
3.1

Definitions for QCSP bases

Intuitively, a QCSP base is a set of strategies organized according to a mechanism of guards for every existentially quantified variable and every value of the
domain. Such a guard is a pair of a value and a tree which is the expression of
what have already been played by both opponents.
Definition 1 (QCSP base). A QCSP base is either
– the symbol bl top
– the symbol bl bottom
– a pair hQ | Gi with n > 0, Q = q1 v1 . . . qn vn and G = [Ge1 , . . . , Gem ] a list
such that
• e1 , . . . , em is the set of indexes of the existentially quantified variables1 ;
• every Gek , 1 ≤ k ≤ m is a function with non-empty graph {(val1 7→
T1 ), . . . , (valjk 7→ Tjk )}, val1 , . . . , valjk ∈ D(vek ) and T1 , . . . , Tjk ∈
Tek (Q).
1

u1 , . . . , up is the set of indexes of the universally quantified variables, {e1 , . . . , em } ∪
{u1 , . . . , up } = [1..n], {e1 , . . . , em } ∩ {u1 , . . . , up } = ∅, quant(vei ) = ∃, for every i,
1 ≤ i ≤ n, quant(vui ) = ∀, for every i, 1 ≤ i ≤ p.

A pair (val, T ) ∈ Gek is a guard for the existentially quantified variable vek .
In what follows, the QCSP bases bl top and bl bottom are semantically interpreted as respectively what is always true and what is always false and algorithmically as respectively what admits every strategy as a winning strategy
and what admits no winning strategy at all.
Example 1. The following guard sets Gx , Gy and Gz are guard sets of the QCSP
base B = h∃x∃y∀z∃t | [Gx , Gy , Gt ]i with x, y, z, t ∈ {0, 1, 2}.
Gx = [(0, ✷), (1, ✷), (2, ✷)],
x
0 1

x
2

Gy = [(0,

x

0 1

2

0 1

), (1,

), (2,
x

0

1

y
0

0 1

2

z
0

y
1
z

1

z
2

)]

y
2

1

z

2

z

0

1

2
z

2

1
),

Gt = [(0,
x

x

1
0
z
0 1

2 0

y
0

1

z

(1,
3.2

y
2

1

2

2

y
z
0

z

z
0 1

1

1
z

2

2
z

0

0

), (2,

)

Interpretation

The semantics of a QCSP base is expressed by an interpretation to the QCSP.
First of all, we interpret the trees of the guards of the QCSP bases as tuples of
values.
Definition 2 (interpretation of a tree). The interpretation of a tree T of a
guard (val, T ) according to a value val is the set
I val (T ) = {(val, e1 , . . . , en )|e1 . . . en a branch of a tree T }.

In particular, I val (✷) = {val}. The interpretation of a set G of guards (value,
tree) is by extension :
[
I val (T ).
I(G) =
(val,T )∈G

Example 2. (Example 1 continued.) The interpretation of the tree T extracted
from the set of guards Gt :
x

0

1

y
0
z
0 1

y
2

1

z
0

y
1
z

1

z
2

2

z

0

1

2

2
z
1

according to the value 0 is the set
I 0 (T ) = {(0, 0, 0, 0), (0, 0, 0, 1), (0, 0, 0, 2),
(0, 0, 1, 0), (0, 0, 2, 0), (0, 1, 1, 1),
(0, 2, 1, 2), (0, 2, 2, 1)}.
and
I(Gt ) = {(0, 0, 0, 0), (0, 0, 0, 1), (0, 0, 0, 2),
(0, 0, 1, 0), (0, 0, 2, 0), (0, 1, 1, 1), (0, 2, 1, 2),
(0, 2, 2, 1), (1, 1, 0, 0), (1, 1, 0, 1), (1, 1, 0, 2),
(1, 1, 1, 0), (1, 1, 2, 0), (1, 2, 1, 1), (2, 2, 0, 0),
(2, 2, 0, 1), (2, 2, 0, 2), (2, 2, 1, 0), (2, 2, 2, 0)}
One can remark that for all (valt , valx , valy , valz ) ∈ I(Gt ), the instantiation
[t ← valt ][x ← valx ][y ← valy ][z ← valz ] satisfies the constraint (x = (y ∗ z) + t).
We now define the interpretation of a QCSP base.
Definition 3 (interpretation of a QCSP base). The interpretation function
(·)∗ of a QCSP base to a QCSP is defined as follows (Q = q1 v1 . . . qn vn ) :
(bl top)∗ = ⊤
(bl bottom)∗ = ⊥
(hQV| [Ge1 , . . . , Gem ]i)∗ =
Q ei ∈[e1 ,...,em ] ((vek , v1 , . . . , vek −1 ) ∈ I(Gek ))
The interpretation of a QCSP base is a QCSP but only on table constraints.
Example 3. (Examples 1 and 2 continued.)
(B)∗ = ∃x∃y∀z∃t((x ∈ I(Gx )) ∧ ((y, x) ∈ I(Gy )) ∧ ((t, x, y, z) ∈ I(Gt )))
with x, y, z, t ∈ {0, 1, 2}, I(Gx ) = {0, 1, 2} and I(Gy ) = {0, 1, 2}2.

3.3

Properties of QCSP bases

To a given QCSP, many different QCSP bases may be such that their interpretations have exactly the same set of winning strategies as that QCSP. We define
this property as the compatibility property.
Definition 4 (compatibility of a QCSP base). A QCSP base is compatible
with a QCSP if its interpretation has exactly the same winning strategy.
In what follows, we will see that the set of compatible QCSP bases may be
seen as a good candidate as a target for a compilation language.
Example 4. (Examples 1, 2 and 3 continued.) The QCSP base B is compatible
with the QCSP ∃x∃y∀z∃t(x = (y∗z)+t) with x, y, z, t ∈ {0, 1, 2}. If, for example,
the pair (2, ✷) of Gx is discarded then the resulting QCSP base is no more
compatible with the QCSP since two of the four winning strategies are lost.
The following theorem establishes immediately the completeness of the QCSP
base formalism w.r.t. QCSP.
Theorem 1 (completeness). For every QCSP there exists a compatible base.
When a QCSP represents a finite two-player game, one of the most important
issues for the existential player, at each turn during the game, is the following:
“What do I have to play to be certain to win the game?” If a winning strategy
has been already computed before the game begins, the player has only to follow
it. But if the uncertainty was not completely known and if the current winning
strategy can not be applied anymore, the existential player has to compute again
a new strategy and has to pay also the complete algorithmic price.
Definition 5 (next move choice problem). The next move choice problem
is defined as follows.
V
– Instance : A QCSP q1 v1 . . . qn vn c∈C c with v1 ∈ D1 , . . . , vn ∈ Dn and
a sequence of instantiations [v1 ← val1 ], . . . , [vi ← vali ] obtained from a
winning strategy for a QCSP with quant(vi ) = ∃ and val1 ∈ D1 , . . . , vali ∈
Di .
– Query : Is there any winning strategy for a QCSP
^
qi+1 vi+1 . . . qn vn
c ∧ (v1 = val1 ) ∧ (vi−1 = vali−1 ) ∧ (vi = vali′ )
c∈C

with vi+1 ∈ Di+1 , . . . , vn ∈ Dn , vali′ ∈ Di , vali′ 6= vali ?
Clearly enough the next move
V choice problem is still a PSPACE-complete
problem since qi+1 vi+1 . . . qn vn c∈C c∧(v1 = val1 )∧(vi−1 = vali−1 )∧(vi = vali′ )
with vi+1 ∈ Di+1 , . . . , vn ∈ Dn , vali′ ∈ Di , vali′ 6= vali is a QCSP.
We introduce a new property for a QCSP base which guarantees that the
next move choice problem is no more PSPACE-complete but polytime w.r.t. the
size of the QCSP base. A QCSP base is optimal if all the guards associated to
the moves played by the existential player are verified then this player is sure to
follow a winning strategy.

Definition 6 (optimality). Let B = hq1 v1 . . . qn vn | [Ge1 , . . . , Gem ]i be a QCSP
base and (B)∗ = q1 v1 . . . qn vn C with v1 ∈ D1 , . . . , vn ∈ Dn . This base is optimal
if the following property is verified. For every i, i ∈ [1 . . . m], let Ci be the set
of constraints {(vek = valek )|1 ≤ k < i} such that (valek , vale1 , . . . , valek−1 ) ∈
I valek (aek ), (valek , aek ) ∈ Gek .
Then for every guard (val, a) ∈ Gei , (val,Vvale1 , . . . , valei−1 ) ∈ I val (a) if and
only if qei +1 vei +1 . . . qn vn (C ∧ (vei = val) ∧ c∈Ci c) admits a winning strategy.
The underlying order of this notion of optimality is the number of winning
scenarios which are not a branch of any winning strategy. In case of the interpretation of an optimal base this number is zero.
opt
and Gopt
are guard sets for
Example 5. The following guard sets Gopt
x , Gy
t
opt
opt
opt
opt
the QCSP base B
= h∃x∃y∀z∃t | [Gx , Gy , Gt ]i which is optimal and
compatible with the QCSP : ∃x∃y∀z∃t(x = (y ∗ z) + t) with x, y, z, t ∈ {0, 1, 2}.

Gopt
= [(0, ✷), (1, ✷), (2, ✷)]
x

x

x

0 1

2

2

= [(0, T0y =
Gopt
y

), (1, T1y =

)]

x
2

0
y

y
1

0
z

z

0 1
Gopt
t

=

[(0, T0t

2

2
),

=
x

x
y

z
0 1

y

z
2

1

0

1

0

(1, T1t =

2

2

1
y

z
0 1

1
), (2, T2t =

z
2

0
)]

Fig. 1. Guard sets for an optimal QCSP base.
We explicit hereafter the optimality of the QCSP base but we use the QCSP
constraint (x = (y ∗ z) + t) instead of the table constraints in order to simplify.

– i = 1 (i.e. vei = x) then Ci = ∅ and for every K ∈ {0, 1, 2}, K ∈ I K (✷) =
{K} and ∃y∀z∃t(x = (y ∗ z) + t) ∧ (x = K), with y, z, t ∈ {0, 1, 2}, admits a
winning strategy.
– i = 2 (i.e. vei = y) then
y
0
• for every K ∈ {0, 1, 2} (K, ✷) ∈ Gopt
x , I (T0 ) = {(0, 0), (0, 1), (0, 2)} and
y
0
for every K ∈ {0, 1, 2}, (0, K) ∈ I (T0 ) and ∀z∃t(x = (y ∗ z) + t) ∧ (y =
0) ∧ (x = K), with z, t ∈ {0, 1, 2}, admits a winning strategy ;
y
y
1
1
• (1, ✷) ∈ Gopt
x , I (T1 ) = {(1, 1)} and (1, 1) ∈ I (T1 ) and ∀z∃t(x =
(y ∗ z) + t) ∧ (y = 1) ∧ (x = 1), with z, t ∈ {0, 1, 2}, admits winning
strategy ; (1, 0) 6∈ I 1 (T1y ) and ∀z∃t(x = (y ∗ z) + t) ∧ (y = 1) ∧ (x = 0),
with z, t ∈ {0, 1, 2}, does not admit a winning strategy ; (1, 2) 6∈ I 1 (T1y )
and ∀z∃t(x = (y ∗ z) + t) ∧ (y = 1) ∧ (x = 2), with z, t ∈ {0, 1, 2}, does
not admit a winning strategy ;
• for y = 2, the is no pair (2, T2y ) ∈ Gy and ∃x∀z∃t(x = (y∗z)+t)∧(y = 2),
with x, z, t ∈ {0, 1, 2}, does not admit a winning strategy.
– i = 3 (i.e. vei = t) then (we only treat the case t = 0, the others are similar)
y
y
opt
1
0
t
• (2, ✷) ∈ Gopt
x , (1, T1 ) ∈ Gy with (1, 2) ∈ I (T1 ) and (0, 2, 1, 2) ∈ I (T0 )
and (x = (y ∗ z) + t) ∧ (x = 2) ∧ (y = 1) ∧ (z = 2) ∧ (t = 0) admits a
winning strategy ; it is similar for (0, 0, 0, 0), (0, 0, 0, 1) and (0, 0, 0, 2) ;
• for all the other cases (0, valx , valy , valz ) 6∈ I 0 (T0t ) and (x = (y ∗ z) + t) ∧
(x = valx ) ∧ (y = valy ) ∧ (z = valz ) ∧ (t = 0) does not admit a winning
strategy.
The most important property of optimal QCSP base is that the next move
choice problem for the interpretation of compatible optimal base with a QCSP
is no more PSPACE-complete but polytime.
Theorem 2 (next move choice problem). The next move decision problem
for the interpretation of an optimal base is polytime in the size of the base.

4

Compilation of a QCSP to an optimal QCSP base

We present in this section an algorithm based on a search algorithm and establish
that the result of the application of this algorithm is an optimal QCSP base
compatible with the initial QCSP. Algorithm 1 rec comp computes a compatible
QCSP base from a QCSP following the inductive definition of the semantics of
the QCSP. This algorithm first computes a fix-point for the set of constraints
and returns bl bottom if a contradiction is detected. If it is not the case and the
binder is not empty then bl top is returned. Otherwise for every value val of
the domain of the outermost variable x of the binder, the constraint (x = val)
is added to the constraint store and the algorithm is recursively called. If the
variable is universally quantified and at least one subproblem returns bl bottom
then bl bottom is returned. If the variable is existentially quantified and all the
subproblems return bl bottom then bl bottom is returned. In any other cases,
operators ⊕∃ or ⊕∀ are called to combine the resulting QCSP bases together.

Algorithm 1 rec comp
In: Q : a binder of a QCSP
In: C : a set of constraints of a QCSP
Out: a QCSP base or bl top or bl bottom
if reach f ixpoint(C) = f ailure then
return bl bottom
end if
if empty(Q) then return bl top end if
qxD ← head(Q); listV alBase ← []; d ← D
while !empty(d) do
val ← head(d); d ← tail(d)
base ← rec comp(tail(Q), C ∪ {x = val})
if base = bl bottom&q = ∀ then
return bl bottom
end if
listV alBase ← [(val, base)|listV alBase]
end while
if empty(listV alBase) then
return bl bottom
end if
if q = ∃ then
return ⊕∃ (xD , Q, listV alBase)
else
return ⊕∀ (xD , Q, listV alBase)
end if

Operators ⊕∀ and ⊕∃ specified respectively by the algorithms 2 and 3 work
as follows. First we describe the ⊕∀ operator. Function constants(l) checks if
the list of pairs as argument l does not contain only bl top or bl bottom for
second element. If the check constants(l) is verified, it is necessarily only a list
of bl top associated with all the values of the domain of the variable in case of an
innermost bloc of universal quantifiers and then bl top is returned. Otherwise,
the operator ⊕ defined hereafter is applied and the result is returned since the
universally quantified variables are not associated to guards. Now we describe the
⊕∃ operator. If the check constants(l) is verified, it is necessarily an innermost
existential quantifier and a QCSP base containing only the values associated
to the bl top is built thanks to the function base case defined by base case(l) =
{(val, ✷)|(val, bl top) ∈ l}. Otherwise, the returned QCSP base is built by adding
to the result of the ⊕ operator the list of the values associated to each of the
QCSP bases thanks to the function f irst values defined by f irst values(l) =
{(val, ✷)|(val, a) ∈ l}.
The ⊕ operator works as follows. The decompose function extracts from the
list lvb of pairs (value, QCSP bases), for the outermost existentially quantified
variable y of the binder, a pair constituted of a list of pairs (val, list of guards))
and a list of pairs (val, remaining of the guards). The compose function builds
for y its set of guards by distributing the trees for the different values. Functions

Algorithm 2 ⊕∃
In: xD : a variable and its domain
In: Q : a binder
In: l : a list of pairs (value, QCSP base)
Out: a QCSP base
if constants(l) then
return h∃xD Q | case base(l)i
else
return h∃xD Q | [f irst values(l)| ⊕ (x, l)]i
end if

Algorithm 3 ⊕∀
In: xD : a variable and its domain
In: Q : a binder
In: l : a list of pairs (value, QCSP base)
Out: a QCSP base or bl top
if constants(l) then
return bl top
else
return h∀xD Q | ⊕ (x, l)i
end if

f irst and second give access to respectively the first and the second position of
a pair.
Algorithm 4 ⊕
In: x : a variable
In: lvb : a list of pairs (value, QCSP base)
Out: a list of guards
lg ← []
lvg ← extract guards(lvb)
while empty(lvg) do
dec y ← decompose(lvg)
lg ← [compose(x, f irst(dec y)|lg]
lvg ← second(dec y)
end while
return lg

The following example shows how the rec comp algorithm works.
Example 6. We compute for all valx , valy ∈ {0, 1, 2} the QCSP base Bvalx valy
as the result of the following call :
rec comp(∀z∃t, {(x = (y ∗ z) + t), (x = valx ), (y = valy )})
with z, t ∈ {0, 1, 2}.

val valy

We obtain the QCSP bases (according to Tvaltx

):

z
0 1

2

B00 = h∀z∃t| [[(0, T000 =

)]]i

z
0 1
B10 = h∀z∃t|

[[(1, T110

2
)]]i

=

z
0 1

2

B20 = h∀z∃t| [[(2, T220 =

)]]i

z

z

2
B21 = h∀z∃t | [[(0, T021 =

z

1
), (1, T121 =

0
), (2, T221 =

)]]i

of for any other combination, Bvalx valy = bl bottom.
The following example shows how the trees are shared by the ⊕ operator and
also the distribution of the trees.
Example 7. The operator ⊕∃ is applied during the execution of the call
rec comp(∃y∀z∃t, {(x = (y ∗ z) + t), (x = 2)})
with y, z, t ∈ {0, 1, 2}, to the QCSP bases B20 , B21 and B22 which represent compatible QCSP bases with QCSP, respectively, ∀z∃t((x = (y ∗ z) + t) ∧ (x = 2) ∧ (y = 0)),
∀z∃t((x = (y ∗ z) + t) ∧ (x = 2) ∧ (y = 1)), ∀z∃t((x = (y ∗ z) + t) ∧ (x = 2) ∧ (y = 2)).
⊕∃ (y, ∀z∃t, [(0, B20 ), (1, B21 ), (2, B22 )])
y

= h∃y∀z∃t | [[(0, ✷), (1, ✷)], [(0,
= B2

1
T021

y

), (1,

1
T121

y
0
), (2,

T220

1
T221

)]]i

which is a compatible QCSP base with the QCSP ∃y∀z∃t((x = (y ∗ z) + t) ∧ (x = 2))
with y, z, t ∈ {0, 1, 2}.

The following example shows how the existential player can play with an
optimal QCSP base instead of only one winning strategy how the optimal QCSP
base gives a direct access to the possibilities for a given existentially quantified
variable.
Example 8. (Previous examples continued.) Let the following QCSP be the expression of a very simple two-player game:
∃x∃y∀z∃t(x = (y ∗ z) + t), x, y, z, t ∈ {0, 1, 2}
Let us suppose that an existential player only knows the following winning
strategy:
x
2
y
1
z
0

2

t
2

t
1

t
0

For his first move, he decides to play (x = 2). Now, following its winning
strategy, he is supposed to play (y = 1). Let us suppose that it is no more
possible because of an unexpected reason. He can not follow its winning strategy
anymore. If he follows the compatible but not optimal base of Example 1 he
will follows one of the two other choices thinking that he still has a chance.
If he wants to be sure, he will have to pay the full computational price for
the QCSP ∀z∃t((x = (y ∗ z) + t) ∧ (x = 2) ∧ (y = 0)), z, t ∈ {0, 1, 2} and
∀z∃t((x = (y ∗ z) + t) ∧ (x = 2) ∧ (y = 2)), z, t ∈ {0, 1, 2}. If he follows its
compatible and optimal QCSP base of Example 5, he knows that he has already
lost.
The following theorem establishes that the rec comp algorithm not only computes a compatible QCSP base from a QCSP but also that this QCSP base is
optimal.
Theorem 3. Let QC be a QCSP. rec comp(Q, C) return an optimal base and
compatible with the QCSP.

5

Conclusion

We have proposed in this article a framework for the compilation of QCSP:
the QCSP bases. We have defined an algorithm embedded in the state-of-theart search algorithm of QCSP solver to compute a QCSP base from a QCSP.

We have shown that the obtained QCSP base is compatible with the initial
QCSP and optimal in the sense that the construction of any winning strategy is
polytime for the interpreration of a QCSP base.
We have implemented in Prolog the algorithms described in this article
and the programs and examples are downloadable. at the following address
http://www.info.univ-angers.fr/pub/stephan/Research/Download.html. We
plan to integrate it in our QCSP solveur developed in the generic constraint development environment Gecode [15].
When a QCSP solver returns there is or there is no winning strategy, there
is no way to check if the answer is correct while for CSP the associated result
to the decision (a complete instantiation) is easy to check. A certificate for a
QCSP which has a winning strategy is any piece of information that provides
self-supporting evidence of the existence of a winning strategy for that QCSP.
Due to the lack of space, we have not treated certificates for QCSP: our formalism includes QCSP certificates as a particular case. During the execution of
the solver, a QCSP base is generated but only with strategies as guards. The
interpretation of these trees (cf Definition 2) in tuples permits to verify such a
QCSP certificate w.r.t. a QCSP by the resolution of a co-NP-complete problem.
(The complexity is similar to the check of a winning strategy for QBF [4].)
We have proposed a recursive construction of the QCSP base but in practice
it is often more efficient to consider a cooperation between a solver which emits
a trace and a trace analyzer which builds the QCSP base. We have also develop
this approach but due to the lack of space we only give here the main two
important reasons for this cooperation between a solver and a trace analyzer:
If the construction of the QCSP base is embedded into the solver, the memory
management of the solver by means of a backtrack stack will have also to keep
the state of the current QCSP base. We want to take into account modern
architectures with multi-core multithreaded processors.

References
1. J. Amilhastre, H. Fargier, and P. Marquis. Consistency Restoration and Explanations in Dynamic CSPs - Application to Configuration. Artificial Intelligence,
135(1-2):199–234, 2002.
2. S. Baba, Y. Joe, A. Iwasaki, and M. Yokoo. Real-Time Solving of Quantified CSPs
Based on Monte-Carlo Game Tree Search. In Proceedings of the 22nd International
Joint Conference on Artificial Intelligence (IJCAI’11), pages 655–661, 2011.
3. F. Bacchus and K. Stergiou. Solution directed backjumping for QCSP. In Proceedings of the 13th International Conference on Principles and Practice of Constraint
Programming (CP’07), pages 148–163, 2007.
4. M. Benedetti. Extracting Certificates from Quantified Boolean Formulas. In
Proceedings of 9th International Joint Conference on Artificial Intelligence (IJCAI’05), pages 47–53, 2005.
5. M. Benedetti, A. Lallouet, and J. Vautard. Reusing CSP propagators for QCSPs.
In Recent Advances in Constraints, 11th Annual ERCIM International, Workshop
on Constraint Solving and Contraint Logic Programming (CSCLP’06), pages 63–
77, 2006.

6. L. Bordeaux, M. Cadoli, and T. Mancini. CSP Properties for Quantified Constraints: Definitions and Complexity. In Proceedings of the 20th National Conference on Artificial Intelligence (AAAI’05), pages 360–365, 2005.
7. L. Bordeaux and E. Monfroy. Beyond NP: Arc-Consistency for Quantified Constraints. In Proceedings of the 8th International Conference on Principles and
Practice of Constraint Programming (CP’02), pages 371–386, 2002.
8. S.C. Brailsford, C.N. Potts, and B.M. Smith. Constraint staifaction problems:
Agorithms and applications. European Journal of Operational Research, 119:557–
581, 1999.
9. H. Chen. The Computational Complexity of Quantified Constraint Satisfaction,
PhD thesis, Cornell University, 2004.
10. S. Coste-Marquis, D. Le Berre, F. Letombe, and P. Marquis. Complexity Results
for Quantified Boolean Formulae Based on Complete Propositional Languages.
Journal on Satisfiability, Boolean Modeling and Computation, 1:61–88, 2006.
11. H. Fargier and P. Marquis. On the Use of Partially Ordered Decision Graphs in
Knowledge Compilation and Quantified Boolean Formulae. In Proceedings of the
21th National Conference on Artificial Intelligence (AAAI’06), 2006.
12. I. Gent, P. Nightingale, and K. Stergiou. QCSP-solve: A solver for quantified constraint satisfaction problems. In Proceedings of 9th International Joint Conference
on Artificial Intelligence (IJCAI’05), pages 138–143, 2005.
13. I.P. Gent, P. Nightingale, and A. Rowley. Encoding Quantified CSPs as Quantified
Boolean Formulae. In Proceedings of the 16th European Conference on Artificial
Intelligence (ECAI’04), pages 176–180, 2004.
14. A.K. Mackworth. Consistency in networks of relations. In Artificial Intelligence,
volume 8, pages 99–118, 1977.
15. C. Schulte and G. Tack. Views and Iterators for Generic Constraint Implementations. In Proceedings of the 11th International Conference on Principles and
Practice of Constraint Programming (CP’05), pages 817–821, 2005.
16. I. Stéphan and B. Da Mota. A unified framework for Certificate and Compilation
for QBF. In Proceedings of the 3rd Indian Conference on Logic and its Applications,
pages 210–223, 2009.
17. D. Stynes and K.N. Brown. Realtime Online Solving of Quantified CSPs. In
Proceedings of the 15th International Conference on Principles and Practice of
Constraint Programming (CP’09), pages 771–786, 2009.
18. G. Verger and C. Bessière. BlockSolve : une approche bottom-up des QCSP. In
Actes des Deuxièmes Journées Francophones de Programmation par Contraintes
(JFPC’06), pages 337–345, 2006.

