Many constraints

of the different type


Adding the constraint

$X_1\neq X_2 + c$

where $c$ is a constant

should be quite easy

It requires to define the filter function.


The 2 rules of $X_1\neq X_2 + c$

1. if $X_2$ is instantied to $v_2$,
then $v_2+c$ must be removed from $X_1$ values,

2. if $X_1$ is instantied to $v_1$,
then $v_1-c$ must be removed from $X_2$ values.


Let’s fix the code


  class NotEqual:
      def __init__(self, v1, v2, c=0):
          pass

      def filter(self, vars):
          pass

>>🥛<<


The NotEqual class

class NotEqual:
    def __init__(self, v1, v2, c=0):
        self.v1 = v1
        self.v2 = v2
        self.c = c

    def filter(self, vars):
      size = len(vars[self.v1]) + len(vars[self.v2])
      if len(vars[self.v2]) == 1:
          f = min(vars[self.v2]) + self.c
          nd1 = {v for v in vars[self.v1] if v != f}
          if len(nd1) == 0:
            return False
          vars[self.v1] = nd1
      if len(vars[self.v1]) == 1:
          f = min(vars[self.v1]) - self.c
          nd2 = {v for v in vars[self.v2] if v != f}
          if len(nd2) == 0:
            return False
          vars[self.v2] = nd2
      modif = size > len(vars[self.v1]) + len(vars[self.v2])
      return modif or None

🚀 Constraints

  • Different level of inconsistency
  • Global reasoning vs decomposition
  • Explain domain modifications
  • Reification, entailment, …