QCSP Made Practical by Virtue of Restricted Quantification

1 Introduction

We extend the QCSP (Quantified Constraint Satisfaction Problem) framework by introducing a new language, called QCSP+. Such extension is motivated by the difficulties we experienced in modelling and solving most non-trivial problems as plain QCSPs. So, let us start by describing (Q)CSP, in order to point out some of its modeling weaknesses.

A CSP is a search problem established by giving a set of variables ranging over finite domains, and a conjunction of constraints mentioning such variables. For example, given x ∈ {1, 2, 3}, y ∈ {3, 4}, and z ∈ {4, 5, 6}, the CSP

is solved by selecting (if possible) one value for each variable in so as to satisfy the three constraints at once. For example, x = 1, y = 4, z = 5 is a valid solution, while x = 2, y = 4, z=6 is not. CSP formulations are naturally suited to model real-world problems, and countless applications exist indeed.

For the sake of this paper, a CSP problem is best viewed as a decision problem in which all the variables are quantified existentially (i.e. the existence of one single consistent assignment suffices to answer the problem positively):

The seemengly inconsequential amendment of making quantifiers explicit leads us to play in an entirely new field [Bordeaux and Monfroy, 2002]: What if (some of) the variables are quantified universally? For example, what means for

∗This author is supported by "Le STUDIUM R©" (France).

to be true? The most intuitive way of entering the new scenario is by thinking of it as a game between two players. One player is associated to the existential quantifier-we call him the ∃-player-the other is related to the universal quantifier: the ∀-player. The goal of the ∃-player is to satisfy each constraint, hence to satisfy the whole CSP. The goal of the ∀- player is to violate at least one constraint, thus overcoming the opponent's effort. The two players play against each other in turn, for a finite and fixed number of rounds. The moves they do consist in assigning values to variables. Which variables get assigned at each step is statically decided by the left-to-right order in the prefix of the problem (in our example, the prefix is "∃x ∈ {1, 2, 3}∀y ∈ {3, 4}∃z ∈ {4, 5, 6}").

In (1), the ∃-player plays first, and he is given the chance to choose a value for x. Then, it is time for the ∀-player to assign a value to the variable y. Finally, the ∃-player assigns z and the game terminates: The satisfaction of the set of constraints is evaluated. We say that such quantified CSP (QCSP) is true if the ∃-player has a winning strategy-i.e. if he can manage to satisfy every constraint whatever the universal opponent does-and is false otherwise. For example, (1) is true, while it becomes false if we change the prefix to ∀x∃y∀z. As opposed to the purely existential CSP case, the order of quantifiers is important: By flipping y and z in (1) we play under the prefix ∃x∃z∀y, and the existential player looses the game.

QCSP is widely believed to be strictly more "powerful" than CSP: An entire hierarchy of QCSP problems exists for which no equivalent CSP formulation can be written "compactly" (QCSP is PSPACE-complete, CSP is NP-complete). Some of these problems are openly perceived as games by humans (i.e. board games), while in others the underlying game structure is camouflaged (see Section 2).

Despite the expectation engendered by the strength of the language, we find in the literature no single account of a realworld model 1 actually solved by a QCSP solver. Why?

A partial explanation is that QCSP solvers are in their infancy and miss most (quantified) constraint propagators, i.e. forward inference rules that are vital to cut the search space.

1 By real-world model we mean any model designed to capture the pre-existing and human-intelligible semantics of some problem-e.g. the ones in Section 2-as opposed to randommodels that obey merely syntactical generation patterns.

This limitation discourages or prevents people from investing in the production of realistic models. However, we have recently built a full-fledged QCSP solver [Benedetti et al., 2006b], which manages several constraints. Even so, models of many "natural" cases stay surprisingly difficult to devise.

To pinpoint the problem, let us take a step back to QCSP as a game between ∃ and ∀, and let us observe that with games almost invariably come rules: Some choices could be precluded as a function of previous choices by the same player or by the opponent. An elementary example is the prohibition in most board games to play in a cell already occupied by someone. In the QCSP game, this means that players cannot in general assign variables in arbitrary ways. The set of legal choices is dynamically restricted over a game life-span in relation to the moves already occurred, so to comply with an underlying game discipline. The observance of such discipline is precisely what plain QCSPs find difficult to enforce.

No support for dynamic ranges of variables is provided by the prefix: In (1) z ranges over {4, 5, 6} whichever the values chosen for x and y. So, we have to embed the game discipline in the constraints. It is a matter of stating that if a player chooses a forbidden value (or combination of values) he looses immediately. Such threat is promptly posed to the ∃-player: We consider the membership of the move to the set of legal moves as just an additional constraint. If the ∃-player cheats, he makes such constraint false, he looses the game.

No similar expedient can be used against the ∀-player: The game is a loss for him when all the constraints are satisfied, a thing which simply cannot be imposed by just conjuncting whatever additional constraint. Rather, to solve such ∀- discipline problem we should slightly modify the whole formalization. This reformulation-based approach has been presented in [Ans´otegui et al., 2005] for the case of two-players QBF games but, for the reasons discussed in Section 4, it comes out to be an unsatisfactory remedy to our problem. So, let us introduce a different solution, based on handling the game rules explicitly. As we shall see shortly, QCSP is not enough to plainly state the new formalization as it lacks support for disjunctions between constraint sets. Consider the following problem (in which rules are provisionally absent)

Let uppercase letters denote sets of variables rather than a single variable (domains are not shown). Suppose the legal opening moves for ∀-player are characterized by a set of constraints (a CSP) L∀1(X1), i.e. an assignment to the variables in X1 is a legal opening move iff it is a solution to L∀1 in the classical CSP sense. Next, ∃-player's reply at second step is constrained by some CSP L∃1(X1, Y1): Once the choices over X1 from ∀-player's side are known, an assigment over Y1 is to be considered only if it solves L∃1. Likewise, rules L∀2(X1, Y1,X2) and L∃2(X1, Y1,X2, Y2) are provided. To capture this scenario, we introduce restricted quantifiers qX[L], with q ∈ {∃, ∀}: They quantify over X yet only span over those assignments to X which comply with the CSP-based rule L. With this compact notation, our example is written:

which reads "for all the assignments to X1 such that L∀1 holds, exists an assignment to Y2 such that L∃1 holds and for all...". We can reshape the above formula as a prenex QCSP as we realize that the "such that" connective stays for a conjunction when ∃-player is involved, and for an implication when ∀-player is concerned. So, we actually ask whether

or, in an equivalent prenex formwith explicit disjunction, if

Statement (4) shows that the most natural way to express restricted quantifiers would be to extend the language to handle disjunctions. But, a shift to general non-conjunctive CSPs would hamper the critical opportunity to inherit the huge amount of propagators already implemented for the purely conjunctive case. We would fall back into the inability to exercise CSP tools on real problems, by having a nice formalism with just a proof-of-concept or no implementation at all.

Our solution is to design a limited disjunctive extension of the QCSP formalism, which is (i) enough to express all the disjunctions originating from the use of restricted (universal) quantifications, but is (ii) still capable of inheriting and exercising the reasoning core of standard (Q)CSP solvers.

From a FOL perspective, the syntactic shape of the problems we introduce-the QCSP+ problems, generalizing Example (3-4)-is a chain of nested alternated quantifications with restrictions (depicted aside). This language is cognitively adequate to represent game-withrules scenarios (modeler's viewpoint, Section 2), and at the same time is amenable to be decided by reusing existing technology (solver's viewpoint, Section 3). Indeed, each restriction rule is a standard CSP, inside which the usual propagation procedures can be capitalized. What is to be designed is (i) an external search-guiding mechanism that evaluates the truth value of the alternated chain of CSPs as a function of the truth value of the leaves, and (ii) an inter-leaf propagation scheme that reconciles the separate CSPs and makes them share information in a sound way. As a final note, let us observe that the "game-with-rules" scenario we target is definitely not a marginal modeling case. On the contrary, the usage of

restricted quantifiers is so natural (see Section 2) that one ends up wondering which non-trivial problems can be modeled as plain QCSPs! The relation between our approach and recent contributions in the close field of QBF decision procedures is discussed in Section 4. The implementation of a full-fledged solver and experiments on quantified models are presented in Section 5. In Section 6 we summarize our contributions and present directions for future work.

2 Motivating Examples

The concepts involved in the modeling of the following common problems are naturally captured as a conjunction of constraints. However, the questions we ask require universal quantifiers and disjunctions in exactly the QCSP+ style.

Problem 1 Suppose some (partial) ordering ⪯ is established to rank the solutions of a given CSP P. While a CSP is not enough to compactly characterize the best solutions of P w.r.t. ⪯, QCSP+ gives to the problem an elegant one-move game formulation: ∃X[P(X)]. ∀Y [P(Y )]. Y ⪯ X.

In the following example [Cadoli et al., 1997], solutions to the CSP represent sets, and the ⊆ relation creates preferences.

Example 1 (Strategic Companies) We are given a collection C of companies, a set G of goods, and a relation Prod⊆ C×G to specify which goods each company produces. Companies have reciprocal financial participations, and a subset C′ ⊆C that owns more than 50% of some c∈C is said to be a controlling set for c. A company may have many controlling sets. They all are represented by a relation Contr⊆2C ×C. A set of companies S⊆C is "production-preserving"-written PP(S)-if it (i) covers all the goods in G, i.e. by cumulating the goods g such that 〈c, g〉 ∈Prod and c ∈S we obtain G; and (ii) is closed under the controlling relation, i.e., for each 〈C′ , c〉 ∈ Contr, if C′ ⊆ S then c ∈ S. A strategic set is any subset-minimal production-preserving set (i.e. the PP property is lost in each proper subset of a strategic set). A company x∈C is not strategic (intuition: it can be sold with no impact on either the overall portfolio of goods or the controlled companies) if it belongs to no strategic set, i.e. if

The Prod and Contr relations as defined above can be easily expressed in propositional logic. We adopted such restricted version to enable a direct comparison with boolean reasoners (Section 5). More realistic models-mentioning explicit amounts of goods, capacity of production and percentage of participations-still fit nicely in the CSP vocabulary, but they lay outside the natural reach of propositional logic.

Problem 2 (Game strategy) Let a set of variables Xi describe the state at step i of a system evolving after the alternate moves of two opponents p∀ and p∃, selected out of a finite set of possibilities. A game is defined by a 4-tuple 〈PA, SSA, G, I〉 of CSPs: A move M in a state X is only possible when the precondition axiom PA(X,M) is satisfied and leads to a new state X′ defined by the successor state axiom SSA(X,X′ ,M). Initial and winning conditions are recognized by I(X) and G(P,X) respectively (with P ∈ {p∀, p∃}). Let ∀ denote ∃ and vice-versa. The first player p∃ wins the game in at most k rounds if ∃X0[I(X0)].WS(∃, 1), where

The next example shows QCSP+ escaping the intricacies of game formalization we find in e.g. [Gent and Rowley, 2003].

Example 2 (Connect n×m-k) Let B=(bij)∈{0, p∀, p∃}n×m be a matrix of variables representing the board state in a generalized Connect-4 game (played on a n×m board in the attempt to align k signs). The existence of a winning strategy for the first player is modeled by posing PA(B, x) := bnx ̸=0, where x∈[1..m] is the column of the current move, and using

as SSA(B,B′ , x), where P ∈ {p∀, p∃} is the current player. The initial condition I(B) is ∧ijbij =0. The G CSP is a conjunction of allDifferent constraints excluding each alignment.

Problem 3 (Conformant Scheduling) Consider n tasks of duration δ1 . . . δn requiring an amount of resource r1 . . . rn, and subject to the ordering constraints O⊆[1..n]×[1..n], where 〈i, j〉 ∈ O means that task i must end before task j starts. We want to schedule the tasks so that (i) we finish by time T, (ii) we comply with O, and (iii) the instantaneous resource consumption never exceeds a fixed capacity R. A global constraint cumulative(R, t1, δ1, r1, . . . , tn, δn, rn) is provided by most CSP solvers to check the latter condition. We have a degree of uncertainty about the actual resources required by each task. An hostile environment can impact on them, subject to certain constraints EM(r1, . . . , rn). Is it possible to devise an adversary-safe schedule?

Example 3 Consider three tasks to be completed within time T = 4 and without surpassing a capacity R = 5, with δ1 =1, δ2 =2, δ3 =3, r1 =3, r2 =2, and r3 =1. Task 1 has to finish before Task 2 starts. We seek an attack-safe schedule,

under the assumption that the environment can add one unit of cost to up to two tasks. The picture aside shows that the optimal schedule (A) is subject to critical

attacks, the linear schedule (B) exceeds T, while the solution (C) to the our QCSP+ instance meets all the requirements.

3 Formalizing and Deciding QCSP+

Let V be a set of variables and D = (Dv)v∈V the family of their domains (hereafter we tacitly assume an underlying global version of V and D). For W ⊆ V , we denote by DW the set Πv∈WDv of tuples on W. The projection of a tuple t (or a set of tuples T) on a variable v (or a set of variables W) is denoted by t|v (or T |W ). A constraint is a couple c=(W, T ) with W ⊆ V and T ⊆ DW (W and T are noted var(c) and sol(c)). A CSP is a set of constraints. For a CSP C, we note by var(C)= Sc∈C var(c) its variables and by sol(C) =⋊⋉c∈C sol(c) its solutions, where-for any W, U ⊆ V , A ⊆ DW , and B ⊆ DU -it is A ⋊⋉ B = {t∈DW∪U | t|W∈A∧ t|U∈B}. We name range over W ⊆ V any function R with domain W that associates to each v ∈ W a subset R(v) ⊆ Dv.

Definition 1 (Restricted quantifier) A restricted quantifier is a 4-tuple Q = (q,W, R, C) where q ∈ {∃, ∀}, W is a set of variables, R is a range over W, and C is a CSP.

Definition 2 (QCSP+) A QCSP+ with free variables F is a couple (QS,G), where the quantification structure QS is a finite (possibly empty) sequence [Q1, . . . ,Qn] of restricted quantifiers Qi = (qi, Vi, Ri, Ci) for which it holds that

• ∀i, j ∈ [1..n], Vi ∩ F = ∅ and i ̸= j ⇒ Vi ∩ Vj = ∅
• var(Ci) ⊆ Wi ∪ F with Wi = Sj≤i Vj

and G is a CSP, called goal, with var(G) ⊆ Wn ∪ F . If F = ∅ the QCSP+ problem is said to be closed.

Consistently with the examples already presented, we compactly denote such QCSP+ by writing:

Only two closed QCSP+ with an empty quantification structure exists: ([ ],⊤) and ([ ],⊥), where ⊤ denotes the empty CSP, and ⊥ stands for any CSP which contains an empty constraint. Given a QCSP+ problem P = ([(q1, V1,R1,C1), . . . , (qn, Vn,Rn,Cn)],G) with free variables F, the result of assigning the value a∈Dv to a variable v∈F, written P[v=a], is defined as P =([(q1, V1,R1,C1[v= a]), . . . , (qn, Vn, Rn, Cn[v = a])], G[v = a]), where the assignment to a CSP is in turn obtained by collecting the result of the assignments to each constraint: Given a constraint c = (W, T), it is c[v = a] = c if v /∈ W. Otherwise, it is c′ = c[v = a] = (W ′ , T ′ ) where W ′ =W \ {v} and T ′ ={t′ ∈ DW ′ | ∃t ∈ DW , t|W ′ =t′ ∧ t|v=a}. This notion extends naturally to tuple-assignments [W = t], with W ⊆ V , t∈DW . For any W ⊆ V , t ∈ DW , and any range R over W, let us write t∈WR to mean ∀v ∈ W t|v ∈ R(v).

Definition 3 (Evaluation of a QCSP+) Any closed QCSP+ (QS, G) evaluates to a value in {true,false} as follows.

base case. eval(([ ],⊤))=true and eval(([ ],⊥))=false.

inductive case. Let it be QS = [(q,W,R,C) | QS ′ ]. It is eval((QS,G)) = true iff: (i) q = ∀ and for all t ∈WR such that t∈sol(C), it is eval((QS ′ ,G)[W=t]) = true, or (ii) q=∃ and there exists t∈WR such that t∈sol(C) and eval((QS ′ , G)[W=t]) = true.

The decision procedure we implement closely mimics the definition of eval, and is based on a classical depth-first recursive search of the and/or tree associated to a quantification structure. As in CSP solvers, a form of forward-inference (called propagation) is of key importance to prune the search space, and is exercised in each search node. What is peculiar to QCSP+ is exactly the way this propagation operates, and the way it builds on top of standard CSP propagation.

We model a CSP propagation scheme as parametric function propP (·)-where the parameter P is a CSP-whose domain and co-domain are the families of ranges over var(P). The result R′ =propP (R) of a propagation over R is meant to contract the range of each variable (hence to reduce the branching factor of the search) while preserving the solutions of P. This means that for any variable v ∈ var(P) it is R′ (v) ⊆ R(v), but at the same time for each solution t ∈ sol(P), if t|v ∈ R(v) then t|v ∈ R′ (v). Propagation is computed by a chaotic iteration as the greatest common fixpoint of the domain-reduction operators associated to each constraint c ∈ P, where the operator for c prunes values that fail a local consistency check against c [Apt, 1999].

If R1 is a range over W1 and R2 is a range over W2 (W1 ∩ W2 = ∅), we define R = R1 ⊔ R2 as R(v)=R1(v) if v ∈ W1 and R(v)=R2(v) if v ∈ W2. We note projections of ranges onto sub-domains by |, so e.g. R|W1 = R1 and R|W2 = R2.

The analogous of propagation in QCSP+ is as follows.

Definition 4 (Cascade Propagation) Given a propagation scheme prop, a QCSP+ problem P, and a range RF for the free variables F of P, the QCSP+ problem cascade(P) obtained by cascade propagation from P is defined as follows.

base case. It is cascade(([],G)) = ([],⊥) if, for any v ∈ F, we have R′ (v) = ∅, where R′ = propG(RF ). Otherwise, cascade(([], G)) = ([], G).

inductive case. Let it be P = ([(q,W,R,C)|QS],G) and R′ = propC(RF ⊔ R). If for any v ∈ F ∪ W it is R′ (v) = ∅, then cascade(P) = ([],⊤) if q = ∀, and cascade(P)=([],⊥) if q=∃. Otherwise (no empty range in R′ ), it is cascade(P) = ([(q,W,R′ |W,C)|QS ′ ],G′ ) where (QS ′ ,G′ )=cascade((QS,G)) is computed using the new range R′ for the free variables F ∪W of (QS, G).

The intuition is that propagation at the level of each restricted quantifier (q,W,R,C) is the "authoritative" source of information about the new ranges of W. Conversely, for variables in var(C)\W a private temporary version of the ranges is employed where all the prunings realized by dominating scopes are cumulated. Such collective result flows through the chain of authoritative propagations to boost them, then vanishes.

The alternated structure of QCSP+ endows cascade propagation with an intrinsic advantage over the usual quantified arc-consistency of QCSP: It turns the global consistency check for values in universal domains into a local property, decidable at the level of single constraints in the CSP rule of restricted quantifiers. This way, we expunge values from both universal and existential domains, symmetrically, by just (re)using quantification-unaware CSP propagators.

We call validity preserving any mapping op : QCSP + → QCSP + such that ∀P ∈ QCSP +, eval(P) = eval(op(P)), and we say that op is a contractor if ∀P = (QS,G) ∈ QCSP +, P ′ = (QS ′ ,G′ ) =op(P) it is (i) |QS ′ | ≤ |QS|, (ii) var(P ′ ) ⊆ var(P), and (iii) for every (q,W,R,C) ∈ QS, (q′ ,W ′ ,R′ ,C′ ) ∈ QS ′ , if v ∈W ∩W ′ then R′ (v) ⊆ R(v).

Theorem 1 Cascade propagation is a validity-preserving contractor for QCSP+ problems.

The above property guarantees soundness and termination of the decision procedure, which performs cascade propagation at each search node. For details see [Benedetti et al., 2006a].

4 Discussion and RelatedWorks

Concerns about the unsuitability of QCSP to model real cases have not been raised so far 2 : Current random models do not clash with the issues addressed in this paper. QCSP+ has been designed in fact to provide crucial benefits in the upcoming development of more realistic models.

The existence of a "∀-discipline" issue in quantified conjunctive languages has been recently identified by the QBF community [Ans´otegui et al., 2005]. A static version of the same question has been discussed for the case of QBF encodings of multi-valued QCSP variables whose boolean mapping needs to avoid "illegal" combinations [Gent et al., 2004].

This problem impacts on QCSP remarkably more than on QBF: The latter does not bother at all with the modeler's viewpoint, as it is not required for a human to write or understand a QBF specification. Such QBF is obtained through a computer-assisted compilation which starts from some higher-level language and terminates in a process called CNF-ization. This consists in casting the meaning of any structured formula into a CNF by conjuncting the clausebased local meaning of each sub-formula through the help of auxiliary variables [Plaisted and Greenbaum, 1986]. A natural workaround to the discipline problem comes out of this mechanism: We reduce to a conjunctive matrix the entire meaning of e.g., (4). This trick has since ever been adoptedoften tacitly-in QBF models, and is the reason why a library of real-world instances exists [Giunchiglia et al., 2001].

2 Such weakness is being quickly realized, as witnessed by the independent proposal of a framework focusing on simplifying the QCSP modeling of two-player games [Bessiere and Verger, 2006].

A more structured QBF encoding technique-applied to two-player games-has been proposed in [Ans´otegui et al., 2005], where indicator variables are introduced to connect in a suited QBF the SAT-PLAN propositional encoding of preconditions, effects, etc [Kautz and Selman, 1992]. However, this approach is shown to lead search-based solvers to explore artificially enlarged search spaces, an effect which can be mitigated either by employing encodings tuned to trigger a synergy between top-down search and boolean inference mechanisms, or by feeding the solver with information on the special role of indicator variables. More recently, DNF representations for boolean constraints have been adopted to reduce the search space [Sabharwal et al., 2006; Zhang, 2006].

These approaches involve intricate details, or do not introduce explicitly a language/semantics. They demand searchbased solvers, or exploit boolean-only concepts (e.g. DNF), or focus on (human-level) games rather than on the general issue of modeling concepts through quantified constraints.

Conversely, restricted quantification is a fairly general and neat solution, inspired by analogous forms of quantification found in other modeling languages under the name of qualified (Description Logic), or bounded (Logic Programming), or restricted quantification (Logic and Semantics Theory).

Restricted quantifiers-which allow us to reuse propagation technology and are not exclusively designed for searchbased reasoners-can be fully "back ported" to the realm of QBF, where they yield the QBF+ language, defined as the restriction of QCSP+ to boolean variables and clausal constraints. QBF+ will be studied in a forthcoming paper, but a first application is presented in the next section.

The QBF-inspired techniques mentioned above can be interpreted as workarounds to bypass restricted quantifiers in QBF. While first evidences suggest (cfr. next section) that restricted quantifiers may be equally rewarding in QBF, their introduction in QCSP is supported by compelling arguments, as major obstacles prevent us from adapting other solutions: First, the modeler should be made responsible for capturing the semantics of the alternating structure in (4). This threatens one of the fundamental assumptions of (Q)CSP: Models have to be human-writable and readable. Second, QCSP constraints cannot undergo arbitrary syntactic manipulations as clauses do. To illustrate the problem, let us consider the QCSP+ formula ∃X[C1(X)]∀Y [C2(X, Y )].C3(X, Y ). One way to attain a QCSP version of this formula would be to define a (single) constraint over X ∪ Y whose meaning is C1(X) ∧ (C2(X, Y ) ∨ C3(X, Y )), to be processed by a quantified extension of the GAC-scheme [Nightingale, 2005]. Though heavily demanding (in space or time, depending on the technique employed), this is still feasible for small, explicitly defined table constraints. Yet no viable solution exists if the C1-3 are (as they usually happen to be) sets of possibly arithmetic/global constraints. Another option is to use the reified version of each constraint [Bordeaux, 2005]. The reified version of C(X) is an always consistent constraint C′ (X, y), where y ∈ {0, 1}, which is satisfied as C′ (X, 1) if C(X) is consistent, and as C′ (X, 0) otherwise. So, we can write ∃X.∀Y.∃a, b.C1(X) ∧C′2(X, Y, a) ∧C′3(X, Y, b) ∧ (¬a ∨ b) (a generalized version of such rewrite shows that QCSP+ is still in PSPACE). Inescapable complications arise in practice, as (i) no reified version is provided by the CSP environment for many constraints, and (ii) the shift to the reified version may be considerably detrimental from the solver's viewpoint, since reified constraints cannot prune values from domains so long as they don't know the value of their last parameter.

5 Implementation, Models, and Experiments

We implemented our decision procedure for QCSP+ in a system built around the CSP solver GeCode [Schulte and Tack, 2005]. Our solver-called QeCode-accepts a wide set of constraints in the input language 3 , and is publically available from [Benedetti et al., 2006c]. At present, no other system accepts a constraint language as expressive as QeCode does 4 , and no suited public domain model exists yet.

We contribute an initial test suite by devising QCSP+ generators for the examples in Section 2. Example 1 and 2 do not rely on non-boolean variables/constraints and have a straight translation into QBF or QBF+. Our generators also produce such equivalent propositional formulations. This enables us to exercise our system against QBF solvers. It is to be noticed that such comparison is of relative significance and biased in favor of QBF solvers, as it does not leverage the strengths of QeCode (e.g. non-boolean variables, propagators with a complex semantics), while an important weakness is exposed (i.e. data structures are not tailored to boolean reasoning).

Results are shown in Figure 1 and 2. For the "strategic companies" case, it comes out that only one QBF solver, out of the six state-of-the-art ones we have tested 5 , can compete with QeCode. This result is impressive in the light of a recent work [Gent et al., 2006] estimating in two to three orders of magnitude the gain (Q)CSP solvers can achieve by using the light data structures of SAT/QBF solvers (which GeCode, hence QeCode, are not using). To cross-check this hypothesis of gain we modified the QBF decision procedure described in [Benedetti, 2006] to parse and solve QBF+ specifications 6 : The results-labeled "A.B. on QBF+" in Figure 1-confirm an improvement of one/two orders of magnitude over the best QBF solver and the base solver respectively.

3 Actually, all those (the latest version of) GeCode knows.

4 Even if we eschew restricted quantifiers in the modeling.

The existence of strategies in board games is a combinatorial problem with a large number of quantifier alternations known to be hard for general purpose reasoners. For Connect n×m-k results are quite favorable to QeCode (Figure 2, only the two best performing QBF solvers are shown). Our models do not include symmetry breaking or auxiliary predicates.

6 Conclusions and FutureWork

Major obstacles complicate the modeling of real-world problems in purely-conjunctive quantified constraint languages, like QCSP or QBF. The "∀-discipline" issue has been identified as the main culprit. We radically overcome such difficulty by introducing the QCSP+ language, where restricted quantifiers are allowed. This language enrichment is obtained through a controlled integration of disjunctive operators, and is purposely designed to facilitate the inheritance of existing solving and propagation technology: We implement the full-fledged QCSP+ solver QeCode on top of GeCode. Incidentally, QeCode (which can decide plain QCSPs as special cases) happens to be the first QCSP solver to accept a wide set of constraints in the input language, including global constraints, and one of the first to be available publically.

We devise multi-language generators to establish an initial suite of instances with restricted quantification. Experimental comparisons against QBF solvers on some boolean models are quite favorable. However, our main contribution lays elsewhere: QCSP+ offers the formerly absent possibility to write and solve real-world models based on quantified constraints.

We are currently working on the modeling of applicative problems in QCSP+, and in designing decision procedures for QCSP+ and QBF+ that are not based on search.

5 We also tested Quantor [Biere, 2004] and sKizzo [Benedetti, 2005] but they are not competitive on these families.

6 The current implementation is limited to ∀∃ prefixes, but the general case equally follows from the results in Section 3.