Disunification is the problem of deciding satisfiability of a
system of equations and disequations w.r.t. a given equational theory.
In this paper we disunification problem in the context of ACI1
equational theories.
This problem is of great importance, for instance, for the development
of complex constraint solvers over sets.
We start by providing a characterization of the interpretation structures
suitable to model the axioms in ACI1 theories, and we develop
extensions of (general) ACI1 which correspond to the ``intuitive''
Herbrand-based models on the class of conjunctions of equations and disequations.
The satisfiability problem is solved using known techniques for the
equality constraints and novel methodologies to transform disequation
constraints into solved forms. We propose three solved forms, offering
an increasingly more precise characterization of the set of solutions.
For each solved form we provide the corresponding rewriting algorithm
and we study the time complexity for the transformation and the successive
satisfiability test.
Remarkably, two of the solved forms can be computed and tested in polynomial
time.
All these solved forms are adequate to be efficiently used in the context
of a Constraint Logic Programming system---e.g., they do not introduce
arbitrary variable quantifications (as happens in some of the existing
solved forms for disunification problems).
The novel results achieved open new possibilities in the practical
and efficient manipulation of ACI1 constraints.
Keywords: CLP, disunification, equational theories,
solved forms, complexity.