Distinct and disjoint constraints.

[rkaminsk]

Currently, we have an O(n*log(n)) propagation algorithm for distinct constraints and an O(n^2) algorithm for disjoint constraints. The propagation algorithm for distinct constraints can still be made stronger. Even though we should probably keep the existing algorithm (as an option) because it should be quite fast. Furthermore, there might be an O(n*log(n)) algorithm for disjoint constraints.

The current implementation of distinct and disjoint constraints still needs refinement. There is some translation happening in the builder which should really be moved to the constraint state. Furthermore, the translation for distinct constraints should be refined as indicated in the code.

A good propagator for distinct constraints seems to be the one in the first paper but the one in the second paper is easier to understand and easier to generalize to disjoint constraints:

• https://cs.uwaterloo.ca/~vanbeek/Publications/ijcai03.pdf
• https://www.aaai.org/Papers/AAAI/1998/AAAI98-051.pdf

The following python code implements the algorithm in the first paper and we should probably also make it available in clingcon.

from bisect import bisect_left, bisect_right


class Domain:
    def __init__(self, lower, upper):
        self.lower = lower
        self.upper = upper


class Rank:
    def __init__(self, var, minrank, maxrank):
        self.var = var
        self.minrank = minrank
        self.maxrank = maxrank

    def __repr__(self):
        return f"({self.minrank},{self.maxrank})"


class Distinct:
    def __init__(self):
        self.variables = ["x1", "x2", "x3", "x4", "x5", "x6"]
        self.domain = {
            "x1": Domain(3, 4),
            "x2": Domain(2, 4),
            "x3": Domain(3, 4),
            "x4": Domain(2, 5),
            "x5": Domain(3, 6),
            "x6": Domain(1, 6)}

    def init(self):
        bounds = set()
        bounds.add(max(dom.upper for dom in self.domain.values()) + 3)
        bounds.add(-1)
        bounds.update(dom.lower for dom in self.domain.values())
        bounds.update(dom.upper + 1 for dom in self.domain.values())
        self.bounds = sorted(bounds)

        self.t = [999]
        self.h = [999]
        self.d = [999]
        for i in range(1, len(self.bounds)):
            self.t.append(i - 1)
            self.h.append(i - 1)
            self.d.append(self.bounds[i] - self.bounds[i - 1])

        self.maxsorted = sorted([Rank(
            var,
            bisect_left(self.bounds, self.domain[var].lower),
            bisect_right(self.bounds, self.domain[var].upper)) for var in self.variables], key=lambda x: x.maxrank)

    def pathmax(self, a, x):
        while x < a[x]:
            x = a[x]
        return x

    def pathset(self, a, x, y, z):
        while x != y:
            a[x], x = z, a[x]

    def propagate(self):
        self.init()
        for rank in self.maxsorted:
            print(f"processing {rank.var} in [{self.domain[rank.var].lower},{self.domain[rank.var].upper}]")
            x = rank.minrank
            y = rank.maxrank
            z = self.pathmax(self.t, x + 1)
            j = self.t[z]
            self.d[z] = self.d[z] - 1
            if self.d[z] == 0:
                self.t[z] = z + 1
                z = self.pathmax(self.t, self.t[z])
                self.t[z] = j
            self.pathset(self.t, x + 1, z, z)
            if self.d[z] < self.bounds[z] - self.bounds[y]:
                print("  UNSAT")
                return False
            if self.h[x] > x:
                w = self.pathmax(self.h, self.h[x])
                rank.min = self.bounds[w]
                print(f"  update lower bound of {rank.var} to {rank.min} where the assignments to the variables in the hall interval [{self.bounds[self.h[w]+1]},{self.bounds[w]-1}] can be used as reason")
                self.pathset(self.h, x, w, w)
            if self.d[z] == self.bounds[z] - self.bounds[y]:
                self.pathset(self.h, self.h[y], j - 1, y)
                self.h[y] = j - 1
                print(f"  new hall interval [{self.bounds[self.h[y]+1]},{self.bounds[y]-1}]")
        return True


constraint = Distinct()
constraint.propagate()