
## 4 Representing Qcsp Instances This Is A Proposal For Qcsp And Qcsp+ By M. Benedetti, A. Lallouet And

J. Vautard.

The Quantified Constraint Satisfaction Problem (QCSP) is an extension of CSP in which variables may be quantified universally or existentially. A QCSP
instance corresponds to a sequence of quantified variables, called prefix, followed by a conjunction of constraints. QCSP and its semantics were introduced in [5].

QCSP+ is an extension of QCSP, introduced in [3] to overcome some difficulties that may occur when modelling real problems with classical QCSP. From a logic viewpoint, an instance of QCSP+ is a formula in which (i) quantification scopes of alternate type are nested one inside the other, (ii) the quantification in each scope is *restricted* by a CSP called restriction or *precondition*, and (iii) a CSP
to be satisfied, called goal, is attached to the innermost scope. An example with 4 scopes is:
∀X1 (L
∀ 1
(X1) →
∃Y1 (L
∃
1
(X1, Y1) ∧
∀X2 (L
∀ 2
(X1, Y1, X2) →
∃Y2 (L
∃ 2
(X1, Y1, X2, Y2) ∧ G(X1, X2, Y1, Y2))
)
)
) (1)
where X1, X2, Y1, and Y1 are in general sets of variables, and each L
Q
iis a conjunction of constraints. A more compact and readable syntax for QCSP+
employs square braces to enclose restrictions. An example with 3 scopes is as follows
∀X1[L
∀
1
(X1)] ∃Y1[L
∃
1
(X1, Y1)] ∀X2[L
∀
2
(X1, Y1, X2)] G(X1, Y1, X2)
which reads "for all values of X1 which satisfy the constraints L
∀
1
(X1), there exists a value for Y1 that satisfies L
∃ 1
(X1, Y1) and is such that for all values for X2 which satisfy L
∀
2
(X1, Y1, X2), the goal G(X1, X2, Y1) is satisfied".

A standard QCSP can be viewed as a particular case of QCSP+ in which all quantifications are unrestricted, i.e. all the CPSs L
Q
iare empty.

## 4.1 Presentation

With respect to format XCSP 2.0, here is the extension to the XML element called <presentation> in order to deal with a QCSP instance:
- the attribute format must be given the value "XCSP 2.1". - the attribute type is required and its value must be "QCSP" or "QCSP+".