Quantified Constraint Satisfaction Problems: From Relaxations to Explanations

1 Introduction

One of the disadvantages of the classical CSP framework is that it lacks sufficient expressive power for modelling particular aspects of real world problems, for example, uncertainty or other forms of uncontrollability in the environment in which a set of constraints must be satisfied.

In this paper we are concerned with the Quantified CSP, a generalisation of the classical CSP that allows some of the variables to be universally quantified [Chen, 2004]. The semantics of universal quantification over a variable is that the set of constraints must be satisfiable for any assignment to it. This is in contrast with classical CSP, where all variables are existentially quantified, i.e. any assignment to an existentially quantified variable that satisfies the constraints is satisfactory. While the classical CSP is known to be NP-complete in general, the QCSP is PSPACE-complete [Chen, 2004]. We consider the problem of relaxing an instance of the QCSP when it is, for example, unsatisfiable. We propose several novel forms of problem relaxation for the QCSP and present an algorithm for generating conflict-based explanations of inconsistency.

Our motivation comes from problems in conformant planning and supply-chain management. We are interested in using constraints to support the local decision-making processes of a company that must supply products to a set of customers, while managing a complex network of its own suppliers. Classical CSP is not sufficiently expressive to model this type of problem concisely, since some of the variables are not under the control of the decision-maker, but we can model the problem as a Quantified CSP. The parallels between adversarial games and QCSP are natural: we can model variables under our control using existential quantifiers and those variables outside our control using universal quantifiers [Chen, 2004].

The remainder of this paper is organised as follows. In Section 2 we present a formal definition of the fundamental concepts in constraint satisfaction and the Quantified CSP. We present several new forms of problem relaxation in Section 3 that have previously not been considered due to the literature's focus on classical CSP. We show how these forms of relaxation can be captured using the notion of requirement relaxation. Section 4 presents an approach to generating explanations of conflict in Quantified CSP based on requirement relaxation. We show how an existing explanation generation algorithm for classical CSPs can be extended to the quantified case. We review the most related work in Section 5. A number of concluding remarks are made in Section 6.

2 Preliminaries

Definition 1 (Classical Constraint Satisfaction Problem)

A constraint satisfaction problem (CSP) is a 3-tuple P ˆ= 〈X,D, C〉 where X is a finite set of variables X ˆ= {x1, . . . , xn}, D is a set of finite domains D ˆ= {D(x1), . . . ,D(xn)} where the domain D(xi) is the finite set of values that variable xi can take, and a set of constraints C ˆ= {c1, . . . , cm}. Each constraint ci is defined by the ordered set var(ci) of the variables it involves, and a set sol(ci) of allowed combinations of values. An assignment of values to the variables in var(ci) satisfies ci if it belongs to sol(ci). A solution to a CSP is an assignment of a value from its domain to each variable such that every constraint in C is satisfied.

A fundamental notion used in reasoning about classical CSPs is that of arc consistency [Mackworth, 1977]. Due to logical conjunction, any assignment to the variables that is locally inconsistent with a constraint is guaranteed not to be part of any consistent solution.

In the classical CSP we can regard all variables as being existentially quantified: we wish to show that there exist assignments for each of the variables that satisfy all constraints simultaneously. However, we can generalise further by also allowing variables to be universally quantified.

Definition 2 (Quantified CSP) A QCSP, φ, has the form

where C is a set of constraints (see Definition 1) defined over the variables x1 . . . xn, and Q is a sequence of quantifiers over the variables x1 . . . xn where each Qi (1 ≤ i ≤ n) is either an existential, ∃, or a universal, ∀, quantifier 1 . The expression ∃xi.c means that "there exists a value a ∈ D(xi) such that the assignment (xi, a) satisfies c". Similarly, the expression ∀xi.c means that "for every value a ∈ D(xi), (xi, a) satisfies c".

Definition 3 (Semantics of QCSP) (based on [Gent et al., 2005]) We define the semantics of the QCSP, Q.C, recursively as follows. If C is empty then the problem is true. If Q is of the form ∃x1Q2x2 . . . Qnxn then Q.C is true iff there exists a value a ∈ D(x1) such that Q2x2 . . . Qnxn.(C ∪{x1 = a}) is true. If Q is of the form ∀x1Q2x2 . . .Qnxn then Q.C is true iff for every value a ∈ D(x1) such that Q2x2 . . .Qnxn.(C ∪ {x1 = a}) is true. Otherwise, Q.C is false.

Example 1 (Quantified CSP) Consider a QCSP defined on the variables x1 and x2 such that D(x1) = D(x2) = {1, 2, 3} as follows: ∃x1∀x2.{x1 < x2}. This QCSP is false. This is because for any value for variable x1 there is at least one value in the domain of x2 that is inconsistent with it. ▲

The above deals only with the equivalent of the decision problem for QCSPs; the analogous treatment for exemplification requires consideration of a winning strategy generalising the idea of a solution [Chen, 2004]. Of course, the order of the quantifiers in a QCSP is critical. Consider the following QCSP: ∃x1 ∈ {0, 1}∀x2 ∈ {0, 1}.{x1 ̸= x2} is false, while ∀x2 ∈ {0, 1}∃x1 ∈ {0, 1}.{x1 ̸= x2} is true.

3 Relaxation

Our motivation for studying relaxations of the QCSP relates to the observation that many real world problems are overconstrained. Accordingly, we are often interested in relaxing the constraints of the problem so that we find a solution that is at least relatively satisfactory. In this scenario, problem relaxation can be seen as a way of exploring the space of alternative models for a given problem. Furthermore, problem relaxations give us a language with which we can explain the over-constrainedness of a problem. Moving from classical CSPs to QCSPs provides us with a richer class of relaxations, and hence, a more expressive language for explanations.

One of the most well known frameworks for reasoning about problem relaxation in classical CSP is Partial Constraint Satisfaction [Freuder and Wallace, 1992]. One can identify four possible ways of relaxing a classical CSP: the domain of a variable can be enlarged; the relation of a constraint (the set of allowed tuples) can be enlarged; a constraint can be removed from the problem; or, a variable can be removed from the problem. Note that all of these strategies can be regarded as enlarging domain or constraint relations. (And domains can themselves be formulated as unary constraints.)

1 When the domain of a variable is clear from context we often write Qixi rather than Qixi ∈ D(xi) in the quantifier sequence.

While all of these forms of relaxation are available to us in the QCSP, the additional expressiveness we have access to within the QCSP gives rise to new forms of relaxation that are not available in classical CSP.

3.1 Relaxation for the Quantified CSP

A useful viewpoint to adopt when studying the QCSP is to consider an instance of the problem as an adversarial game between two players: a universal player who sets the universally quantified variables, and an existential player, who sets the existentially quantified variables [Chen, 2004]. In these terms, we can regard relaxations of the QCSP as modifications to the problem that make it easier for the existential player to win. From the perspective of the universal player, a relaxation of the QCSP may restrict the ways in which this player can falsify the formula. For example, we can restrict the domain of values of the universally quantified variables. From the perspective of the existential player, a relaxation increases the set of responses that can be played to counteract the choices of the universal player. We proceed by discussing five classes of relaxation that are available in the context of the QCSP. While the first two of these are familiar from CSP, the remaining three are particular to the more expressive framework, and have no direct equivalents in the unquantified case.

Single Constraint Relaxation. This is the type of relaxation equivalent to that normally considered in classical CSPs. For example this is the classical approach in the PCSP framework in which allowed tuples are added to an extensionally represented constraint. In principle, this may be replacing a constraint with any logically weaker one. As mentioned earlier, complete removal of a constraint may be considered as a special case of this type of relaxation.

Example 2 (Single Constraint Relaxation) Consider the following QCSP, which is false:

If we relax the constraint between x1 and x2 from < to ≤ to get the following:

the QCSP becomes true. This is because if the existential player sets x1 to 1, the universal can no longer find an assignment that falsifies the QCSP. ▲

Relaxation of Existentially Quantified Domains. Enlarging the domain of an existentially quantified variable is the direct equivalent of relaxing domains in the classical framework.

Example 3 (Relaxation of Existential Domains) We revisit the QCSP presented in Example 2. This is false because the scenario in which the universal player sets x2 to 1 is available. To counter this, the existential player must be able to play a value that is smaller than 1. A suitable relaxation is the following, which adds the value 0 to the domain of x1:

the relaxed QCSP is true since the existential player can set x1 to 0 and the universal player cannot falsify the formula. ▲

Relaxation of Universally Quantified Domains. A class of relaxation not corresponding to any in classical CSPs is to remove values from the domains of universally quantified variables. Doing so reduces the number of scenarios under which the existential player must find satisfying assignments for the existential variables, leading to a more satisfiable problem. The rationale for this may be an analysis of which 'problem values' it may be permissible to ignore, or the narrowing of a range with a probabilistic interpretation.

Example 4 (Relaxation of Universal Domains) Returning to the QCSP of Example 2, which is false, due to the availability of the assignment of x2 to 1, for which the existential player has no satisfying counter-assignment. However, if we relax the domain of the universally quantified variable x2 so that it no longer contains the value 1 to get the following:

the relaxed QCSP is true since the existential player can set x1 to 1 and the universal player cannot falsify the formula. ▲

Quantifier Relaxation. A fourth form of relaxation, also with no direct equivalent in classical CSP, is to reverse the quantification of a variable from universal to existential. This relaxation corresponds to achieving control over a factor previously considered to be environmental. This further relaxes the universal domain relaxation.

Example 5 (Quantifier Relaxation) We revisit the QCSP presented in Example 2, which is false. If relax the universal quantifier on variable x2 to be existential to get:

the relaxed QCSP is true.

▲

QuantifierMoving. Afifth class of problemrelaxation corresponds to moving a universally quantified variable to the left in the sequence of quantifiers. Equivalently, we can consider moving an existentially quantified variable to the right in the sequence of quantifiers. This corresponds to analysis or oracular knowledge of the value of an environment variable, or of delaying a decision until better information is available.

Example 6 (QuantifierMoving) We consider an example, based on one presented earlier in this paper. The following QCSP is false:

We relax this problem by moving the universally quantified variable to the left to give the following QCSP which is true:

Informally, the relaxed QCSP gives the existential player the opportunity to react to the actions of the universal player. ▲

It should be noted that whether each of these relaxations is sensibly possible for a given application is a modelling or knowledge engineering question. In each case, a given constraint, domain, or quantifier may be inherent to the problem, or "background", and thus not susceptible to relaxation.

We claim that this set of relaxations is comprehensive (unless reformulation of the original problem is considered in conjunction with relaxation). It is also orthogonal, if we apply quantifier relaxation only in the case where the domain is a singleton, in the sense that all possible single-step relaxations result in problems that are mutually incomparable.

3.2 QCSP Relaxation as Requirement Relaxation

We now present a uniform treatment of the relaxation of both quantifiers and constraints, that is, the first four classes of relaxation we identify above. Requirements correspond to either a constraint in the QCSP, or a universal quantifier, and we frame relaxation of each as instances of requirement relaxation, over a partial order defined for that purpose.

Definition 4 (Relaxation of a QCSP) We define the relaxation φ[r] of a QCSP φ to a relaxed version of a single requirement to a new value, r, as follows:

This can then be extended to a set of relaxations R: φ[∅] = φ, φ[{r} ∪ R] = (φ[r])[R].

Definition 5 (Ordering over Requirement Relaxations)

Given the set of possible relaxations, R(R), of a requirement R, we say that (r1 ∈ R(R)) ⊑ (r2 ∈ R(R)) iff for any problem φ, if φ[r1] is satisfiable then φ[r2] is, necessarily. We further require that this partial order also be a meetsemilattice, i.e. that greatest lower bounds are guaranteed to exist: if r1, r2 ∈ R(R), then r1 ⊓ r2 is well-defined.

The ordering operator and property we use to make formal the notion of relaxation per se: if r1 ⊏ r2, then we say that r2 is a (strict) relaxation of r1. The greatest lower bound corresponds to the unique requirement relaxation which is as constraining as both of its arguments, but no more (that is, the greatest such element of the relaxation space). The lattice property follows naturally from the relaxation spaces we shall define, and is motivated by the observation that we progressively tighten approximations downwards, and that our relaxation spaces must have a unique least element. For clarity in that respect, we will define the meet operator directly. The partial order may be defined as r1 ⊑ r2 ˆ= r1 = (r1⊓r2), and we note that in each case it is straightforward to derive a closed form for the comparison.

We now define the space of relaxations for constraints, the first form of relaxation we identified above. Essentially, a relaxation of a constraint involves adding additional allowed tuples into its relation.

Definition 6 (Requirement Relaxation for Constraints)

Given a constraint c ˆ= 〈var(c), sol(c)〉 we define its relaxations in terms of adding additional allowed tuples to sol(c) as follows:

The elements of R(c) form the usual lattice using intersection, that is, ⊓ ˆ= ∩.

We now consider universal quantifier relaxation. Informally, the space of possible relaxations for a universal quantifier corresponds to restricting the quantifier to any one of the exponentially many subsets of the domain of the quantified variable, narrowing to a single choice of value, and thereafter widening to existentially quantified subsets. It therefore corresponds to the second, third and fourth forms of relaxation identified in Section 3.1. Of course, in practice, one can limit this relaxation space to a subset of tractable size.

Definition 7 (Requirement Relaxation for Universals)

Given a requirement, r, on a universally quantified variable x, i.e. r ˆ= ∀x ∈ D(x), the set of relaxations R(∀x ∈ D(x)) is defined as:

The elements of R(∀x ∈ D(x)) form the following meetsemilattice:

Note the existence of unique top and bottom points, corresponding to trivially- and un-satisfiable quantifications: ⊤ = (∀x ∈ ∅), ⊥ = (∃x ∈ ∅).

We can now define the space of possible relaxations of a given QCSP in terms of its constituent requirements in the natural way, in terms of the cross-product of the available relaxations for each, and similarly the associated comparison and meet operations.

Before we consider how explanations of falsity can be computed using relaxations, we consider two special cases of relaxation: namely, 1-point and 2-point relaxation spaces. The former, which we denote by R1, contains only the original constraint itself, and is useful when we wish to ensure that some constraints or quantifiers cannot be relaxed. The latter, R2, contains both the original constraint, and ⊤, the maximal relaxation; it is useful when we wish to model the case where we either maintain the requirement or completely relax it.

4 FromRelaxations to Explanations

We now consider explanations for the QCSP. A familiar notion of explanation is that based on minimal conflicts [Junker, 2004]. As we have considered quantification, which is not readily presentable in terms of elements of a conflict set, and further, more general relaxations of constraints than their removal, it is necessary to generalise this notion to that of a minimally conflicting explanation, or alternatively, a maximally relaxed conflict-based explanation. We will henceforth refer to these as maximal, following the relaxation ordering previously defined. We define this notion with respect to a (typically incomplete) consistency propagation method Π, such as QAC [Bordeaux and Monfroy, 2002], in a similar way to Junker [Junker, 2004].

Definition 8 (Maximally Relaxed Explanation) Given

a consistency propagator Π, a maximally relaxed (Πconflict-based) explanation of a Π-inconsistent QCSP φ, is a maximally relaxed QCSP, X, that is inconsistent with respect to Π; i.e. such that φ ⊑ X, ⊥ ∈ Π(X) and for all X ′ such that X ⊏ X ′ , ⊥ /∈ Π(X ′ ).

4.1 Explanation Algorithms

We adopt a scheme similar to that of the QUICKXPLAIN 'family' of algorithms [Junker, 2001; 2004], modified and extended in the following way. We replace the removal (respectively, addition) of a constraint with a specified requirement relaxation (resp. tightening). The specified relaxations form a semilattice, as described in the previous section. This could, in principle, be every possible relaxation, but at a minimum we generally wish to consider the specified relaxations corresponding to the removal (resp. imposition) of each constraint, and the relaxation of a universal quantifier to an existential one: that is, corresponding to relaxation space R2. We may further restrict the set of specified relaxations on the basis that some constraints, and some variables, are intrinsically environmental, and that they should participate in every explanation; this corresponds to using relaxation space R1.

As consideration of every possible relaxation is in general completely intractable, it will generally be desirable to specify a much smaller set. This may be done in broadly two ways. Firstly, as part of the modelling process, an expert specifying the class of problem instances under consideration can give the sets of possible requirement relaxations that are meaningful. Secondly, we can consider a user-driven refinement step, after initial exploration of the available explanations, based on a base step choice of available relaxations, when these have been found to be unsatisfactory.

4.2 The SIMPLEQUANTIFIEDXPLAIN Algorithm

When the set of specified relaxations are binary, i.e. requirements are either in place or fully relaxed, we can use the equivalent of Junker's algorithms, modified simply to use, instead of the imposition and removal of a constraint, the choice between the original and relaxed requirement throughout. We firstly reformulate Junker's REPLAYXPLAIN [Junker, 2001] in terms of relaxations in Algorithm 1, thereby generalising it to QCSPs with (at most) one distinct relaxation available for each of the original requirements, i.e. a requirement is either present, or fully relaxed. We call this modified procedure SIMPLEQUANTIFIEDXPLAIN. We provide as arguments φ, a QCSP, and R, a set of available relaxations, which here should only contain the greatest relaxations allowed for each requirement, ri, that is relaxable in the specified relaxation Rs, i.e. R = {⊤i : i ∈ [1,m+ n],⊤i = ⊔ Rs(ri), |Rs(ri)| > 1}. (This is only well-defined for spaces with a unique maximal relaxation.) We begin with a maximally relaxed problem, using all of the available relaxations R, then build a working set W of relaxations we then iteratively omit, until a Π-inconsistency occurs. At that point we conclude that the relaxation r last added to W (that is, last removed from the subproblem) can be added to a set X corresponding to a partial conflict, and that no further relaxations need to be considered, as some subset of W must be minimal, and still yield an inconsistency. We iteratively continue doing this until the set of possible further relaxations is exhausted, at which point X can be used to relax the original problem φ to yield a maximally relaxed inconsistent problem, φ[R -X], which is our explanation.

Algorithm1: SIMPLEQUANTIFIEDXPLAIN(φ,R)

Input : A QCSP φ; a set of available single-step relaxations R ⊆ {⊤1, . . . , ⊤n+m}. Output: A maximally relaxed conflict-based explanation for φ. if ⊥ /∈ Π(φ) then return exception "no conflict"; if R = ∅ then return φ; X ← ∅; R0 ← R; while R0 ̸= ∅ do W ← ∅; while ⊥ /∈ Π(φ[R - (X ∪ W )]) do select (any) r fromR0; W ← W ∪ {r}; R0 ← R0 - {r}; X ← X ∪ {r}; R0 ← W - {r}; return φ[R - X];

Note that we do not, as with REPLAYXPLAIN and Junker's other explanation procedures, split the input into background and user constraints, and nor do we restrict the output to only user constraints, since the syntax of quantified problems precludes us from doing so. We are instead able to designate some constraints and some quantified variables as not relaxable, which then can be regarded as playing the same role as background constraints. Thus implicitly, user requirements must have at least one available relaxation. One difference in the form of this algorithm is that the 'background' constraints are included in the explanation. Background constraints may be removed from the output after the fact if desired. Observe that the two are equivalent in this sense: if REPLAYXPLAIN (C, U) = X, and SIMPLEQUANTIFIEDXPLAIN (C∪U, {⊤i : ci ∈ U}) =Xq, and Xq = X∪C. (Assuming similar ordering of relaxations (constraints) in each case.) The remaining algorithms presented by Junker may be reformulated in terms of relaxations similarly. (Discussion of the correctness and complexity of this algorithm is deferred until after the presentation of QUANTIFIEDXPLAIN, of which it is a special case.)

Example 7 (SIMPLEQUANTIFIEDXPLAIN) Consider the execution of SIMPLEQUANTIFIEDXPLAIN(φ,R), where φ ˆ= ∃x1 ∈ {1, 2}∀x2 ∈ {1, 2, 3}.{x1 < x2} and R ˆ= {x2 = ⊤, c = ⊤}, a trace of the progress of which is shown in Figure 1. Note that in this case, the explanation is unique, and identical to the original problem, as no relaxation is possible without introducing consistency. Had different choices of relaxations been made, a different trace would have occurred, but the same final result. ▲

4.3 The QUANTIFIEDXPLAIN Algorithm

We now consider QUANTIFIEDXPLAIN (Algorithm 2), a more general algorithm allowing for requirement relaxation lattices of arbitrary size. Once again we follow the basic structure of REPLAYEXPLAIN, but now the key difference is that instead of successively adding constraints to a conflict set (or as in SIMPLEQUANTIFIEDXPLAIN, removing available relaxations), we instead consider a current candidate relaxation comprising one element from each relaxation space, r1 . . . rm+n, and use ⊏ to obtain successive approximations to a maximally relaxed explanation. We begin with a maximal relaxation of each requirement, and then progressively tighten these one at a time: we select an i such that ri may be assigned a new value strictly less than the old one, tightening by a minimal amount at each step to ensure maximality of the final relaxation of the whole problem. When an inconsistency is detected, we eliminate all relaxations tighter than or incomparable to the current approximation from future consideration, as unnecessary for a maximally relaxed explanation. At the same time, we restrict the relaxation space for the last-relaxed requirement, Ri, to ensure that that requirement may not be as relaxed as the earlier value, r′i , that did not produce an inconsistency, as we have guaranteed that that value cannot take part in the explanation currently under construction. We then repeat this process with the relaxation spaces so restricted, until eventually only one possibility remains for each relaxation, thus fully determining the chosen explanation. The complexity of this algorithm (and that of SIMPLEQUANTIFIEDXPLAIN) is equivalent to that of Junker's REPLAYXPLAIN, given a consistency operator of similar complexity, and similar numbers of available relaxations. However, in the QCSP case, there is scope for each of those to be significantly larger.

Algorithm 2: QUANTIFIEDXPLAIN(φ, R)

Input : A QCSP φ; a set of relaxation spaces for each quantifier and constraint, R ⊆ R(φ). Output: A maximally relaxed conflict-based explanation for φ. if ⊥ /∈ Π(φ) then return exception "no conflict"; enumerate R as R1 . . . Rm+n; if ∀i ∈ [1, m + n]|Ri| = 1 then return φ; while ∃i : |Ri| > 1 do foreach Ri do choose an ri from maxima(Ri); if ⊥ ∈ Π(φ′ = φ[{r1, . . . , rm+n}]) then return φ′ ; while ⊥ /∈ Π(φ[{r1, . . . , rm+n}]) do choose an i s.t. ri ̸= bigsqcap(Ri); r′i ← ri; choose an ri from maxima{r : r ∈ Ri, r ⊏ ri}; Ri ← {r : r ∈ Ri, r′i ̸⊑ r}; foreach Rj do Rj ← {r : r ∈ Rj , rj ⊑ r}; return φ[{r1, . . . , rm+n}];

Example 8 (QUANTIFIEDXPLAIN) Consider the QCSP φ ˆ= ∃x1 ∈ {1, 2}∀x2 ∈ {1, 2, 3}.{x1 < x2} and the execution of QUANTIFIEDXPLAIN on φ with the following relaxation spaces: R1(∃x1 ∈ {1, 2}); R8(∀x2 ∈ D(x2)) = {(∀x2 ∈ D′ (x2) : ∅ ⊂ D′ (x2) ⊆ D(x2)}∪{∃x2 ∈ D(x2)}; and R3(x1 < x2) = {x1 < x2, x1 ≤ x2,⊤}. We give a trace of QUANTIFIEDXPLAIN in Figure 2. ▲

The proof of correctness of QUANTIFIEDXPLAIN relies on the following properties, analogous to [Junker, 2001]:

Property 1 If each relaxation space has a unique top element, and ⊥ ∈ Π(φ[{⊤1, . . . , ⊤m+n}]), then the only maximally relaxed explanation is φ[{⊤1, . . . , ⊤m+n}].

Property 2 If ⊥ /∈ Π(φ[{r1, . . . , rm+n}]), for all maximal ri, then no conflict exists, and thus no explanation.

Property 3 If ⊥ ∈ Π(φ[ri]), and X is a maximally relaxed explanation for φ, given the relaxation spaces R1 . . .R′i . . .Rm+n, then X is also a maximally relaxed explanation for φ given the relaxation spaces R1 . . .Ri . . .Rm+n, where R′i = {r ∈ Ri, ri ⊑ r}.

Property 4 If ⊥ ∈ Π(φ[ri]) and ⊥ /∈ Π(φ[r′i ]), where ri ⊏ r′i , then if X is a maximally relaxed explanation for φ, given the relaxation spaces R1 . . .R′i . . .Rm+n, then X is also a maximally relaxed explanation for φ given the relaxation spaces R1 . . .Ri . . .Rm+n, where R′i = {r ∈ Ri, r′i ̸⊑ r}.

Theorem 1 (Maximally Relaxed Explanations) If ⊥ ∈ Π(φ), and R is a set of available relaxations of some, all or none of the requirements of φ, and QUANTIFIEDXPLAIN (φ, R) = X, then: ⊥ ∈ Π(X), and if X ′ = X[r] for some r ∈ R such that X ⊏ X ′ , then ⊥ /∈ Π(X ′ ).

5 RelatedWork

Benhamou and Goualard studied quantified interval constraints, with engineering applications in mind [Benhamou and Goualard, 2000]. More recently, researchers have begun to study how classical CSP concepts such as arc-consistency, satisfiability and interchangeability can be extended to the QCSP [Bordeaux et al., 2005]. A number of techniques for solving the QCSP have been proposed based on encodings to QBF [Gent et al., 2004], as well as using a systematic QCSP solver, called QCSP-Solve, directly [Gent et al., 2005]. A variety of repair-based methods have also been proposed [Stergiou, 2005]. A deep study of the complexity of the QCSP is also available [Chen, 2004]. Our work on relaxation and explanations is the first on these important aspects of reasoning about QCSPs.

6 Conclusions and Future Work

We have extended the concepts of problem relaxation and explanation of inconsistency to the QCSP. We showed that the generality of the QCSP allows for the definition of a number of different forms of relaxation not available in classical CSP. We presented an algorithm called QUANTIFIEDXPLAIN for computing minimally conflicting explanations for QCSPs. Our work on relaxation and explanations for the QCSP is the first study on these interesting and practical aspects of quantified constraint reasoning. We plan to extend the explanation algorithm to deal uniformly with the final class of relaxation, that of quantifier moving, and to establish complexity comparable to Junker's QUICKXPLAIN algorithm. Another important area is that of preferred explanations, with which it would be possible to improve the situation presented here, where an arbitrary explanation is generated from those possible.

Acknowledgements. This work was supported by Science Foundation Ireland (Grant 03/CE3/I405). We thank Hubie Chen, Helene Fargier and Nic Wilson for their comments.