Constraint Systems

A constraint system is a tup.pngle ${\mathscr C} =\langle {\mathscr V} ,$ ${\mathscr L} ,$ ${\mathscr D} ,$ $\mathscr{S},$ $\sqsubseteq^c\rangle$ where:

1. ${\mathscr V}$ is a denumerable set of variables;
2. ${\mathscr L}$ is a first-order language (the assertional language) defining a set of formulas with free variables in ${\mathscr V}$ (the constraints), closed with respect to variable renaming, existential quantification and conjunction, and allowing equalities between variables;
3. ${\mathscr D}$ is a possibly infinite set (the interpretation domain);
4. $\mathscr{S}({\varphi})$ is a set of mappings ${ {\mathscr V} }\rightarrow{ {\mathscr D} }$ (the set of solutions of a constraint $\varphi\in {\mathscr L}$) that preserves the usual semantics of equalities, $\wedge$ and $\exists$ (intersection and projection of the solutions);
5. $\sqsubseteq^c$ is a relation such that $\varphi\sqsubseteq^c\psi$ implies $\mathscr{S}({\psi})\subseteq\mathscr{S}({\varphi})$ (the entailment relation: we say that $\psi$ entails $\varphi$).

We assume that ${\mathscr L}$ contains constraints, denoted `$true$', and `$false$', which are identically true and identically false in ${\mathscr D}$. By analogy with constraint programming, further requirements on constraint systems, like solution compactness [22], can be imposed. We refer to [22] for a discussion.

In the rest of the paper, we often denote the conjunction between constraints with a simple comma. We refer to a generic mapping $\sigma:{ {\mathscr V} }\rightarrow{ {\mathscr D} }$ as an evaluation for the variables in ${\mathscr V}$. We use the notation $\langle {{x_1}\mapsto{d_1},{x_2}\mapsto{d_2},\ldots} \rangle$ to denote an evaluation $\sigma$ mapping $x_1$ to $d_1$, $x_2$ to $d_2$, and so on, and the notation ${\sigma}_{\vert{\vec{x}}}$ to denote the restriction of the evaluation $\sigma$ to the variables $\vec{x}$. We also say that a constraint $\varphi$ is satisfiable if $\mathscr{S}({\varphi})\not=\emptyset$.

Note that there exists several methods for checking satisfiability, entailment, and for variable elimination (see e.g. [10]) over linear arithmetic constraints.

We are now ready to define the framework of multiset rewriting with constraints.