Logically Combining Constraints

When modeling, it happens that, for some problems, constraints must be logically combined. For example, assuming that $x$ is a 1-dimensional array of variables, the statement:

Sum(x) > 10 or AllDifferent(x)

enforces that the sum of values assigned to the variables of $x$ must be greater than 10, or the values assigned to $x$ variables must be all different. As another example, assuming that $y$ is an integer variable, the statement:

$y \neq -1 \Rightarrow x[y] = 1$

enforces that when the value of $y$ is different from $-1$ then the value in $x$ at index $y$ must be equal to 1.

The question is: how can we deal with such situations? The answer is multiple, as one can:

• use the complex (control) structures If() and Match(), or their logical equivalent forms involving the Python operators ‘

  ’, ‘&’ and ‘~’,

• benefit from automatic reformulation mechanisms,
• exploit tabulation,
• post meta-constraints (not in the perimeter of XCSP$³$-core),
• use explicit reification (not in the perimeter of XCSP$³$-core).

As indicated above, meta-constraints and explicit reification are very general mechanisms that are not in the perimeter of XCSP$³$-core. Consequently, in all our illustrative examples, we avoid them. The very good news is that the complex (control) structures If() and Match() (or their logical equivalent forms), together with automatic reformulation mechanisms are strong instruments that allows us to write models in a declative manner, while generating instances that stay within the limits of XCSP$³$-core (and mainly preserving the structure of the models). Tabulation can also be relevant for simplifying some complex logical constrained expressions (and for making sometimes the solving process more efficient). What is stated above is proven by the production of compact and highly readable models for more than 400 problems (available on our website) of various nature and origin.

To illustrate how it works, we need first to import the library PyCSP$^3$:

from pycsp3 import *

Using Complex Structures If() and Then()

In PySCP$³$, one simple way of combining constraints is to build complex expressions/structures by means of the functions If() and Match() (introduced in Version 2.2). First, do note that the first letter is capitalized, and so If is different from the Python keyword if and Match is different from the Python keyword match.

Let us start with the function If() whose signature is:

def If(test, *testOthers, Then, Else=None):

The two first parameters (test and testOthers) are positional, and allow us to indicate a (possibly singleton) sequence of constraints. It is important to note that it is not possible to use a classical condition (i.e., an expression which is not a constraint), as those employed with the Python keyword if. Two named parameters follow the sequence of tests/conditions:

• Then, which is required and must be named, is either a single constraint or a list (or tuple) of constraints,
• Else, which is optional (as None is a default value), is either None, a single constraint or a list (or tuple) of constraints.

The signature of the function Match() is:

def Match(Expr, *, Cases):

The first parameter must be either a variable of the model, or a constraining expression, i.e., an expression involving at least one variable of the model. The second parameter is required, and must be named. Its value must be a dictionary such that each key of this dictionary must be a value or an expression, and the associated value must be a constraint or a list (or tuple) of constraints.

We illustrate various uses of these two high-level functions by introducing a model for the problem Arithmetic Target from Minizinc Challenge 2022. The Arithmetic Problem is to determine the set of operations to be applied on a sequence of numbers (given as input) so as to get some output (target).

An example of data is given by:

numbers = cp_array([1, 2, 4, 6, 6, 7, 8, 9])
target = 814

We also need:

n = len(numbers)
m = 2 * n  # - 1

M = range(1, m)
VAL, ADD, SUB, MUL, DIV, NO = Tokens = range(6)

We start by introducing all arrays of variables; and stand-alone variables, from the original Minizinc model:

# x[i] is the token associated with the ith node
x = VarArray(size=m, dom=lambda i: {-1} if i == 0 else Tokens)

# left[i] is the left child (or 0 if none) of the ith node
left = VarArray(size=m, dom=lambda i: {-1} if i == 0 else range(m))

# right[i] is the right child (or 0 if none) of the ith node
right = VarArray(size=m, dom=lambda i: {-1} if i == 0 else range(m))

# lowest[i] is the lowest descendant of the ith node
lowest = VarArray(size=m, dom=lambda i: {-1} if i == 0 else range(m))

# highest[i] is the highest descendant of the ith node
highest = VarArray(size=m, dom=lambda i: {-1} if i == 0 else range(m))

# index[i] is the index of the number associated with the ith node
index = VarArray(size=m, dom=lambda i: {-1} if i == 0 else range(n + 1))

# leaf[i] is 1 if the ith node is a leaf
leaf = VarArray(size=m, dom={0, 1})

# parent[i] is 1 if the ith node is a parent
parent = VarArray(size=m, dom={0, 1})

# unused[i] is the ith element is unused
unused = VarArray(size=m, dom={0, 1})

# the tree depth
depth = Var(dom=range(1, 2 * n))

# z1[i] is the value associated with the ith node
z1 = VarArray(size=m, dom=lambda i: {-1} if i == 0 else range(10 * target + 1))

# z2 is the number of used nodes
z2 = Var(dom=range(1, n + 1))

Let us print some arrays of variables:

print(x)
print(parent)
print(z1)

[x[0], x[1], x[2], x[3], x[4], x[5], x[6], x[7], x[8], x[9], x[10], x[11], x[12], x[13], x[14], x[15]]
[parent[0], parent[1], parent[2], parent[3], parent[4], parent[5], parent[6], parent[7], parent[8], parent[9], parent[10], parent[11], parent[12], parent[13], parent[14], parent[15]]
[z1[0], z1[1], z1[2], z1[3], z1[4], z1[5], z1[6], z1[7], z1[8], z1[9], z1[10], z1[11], z1[12], z1[13], z1[14], z1[15]]

We post a few constraints:

satisfy(
  # ensuring that the special value 0 appears n-1 times
  Count(index, value=0) == n - 1,

  # ensuring all indexes of numbers are different (except for the special value 0)
  AllDifferent(index, excepting=0),
   
  # ensuring that the tree has n leaves
  Count(x, value=VAL) == n,
   
  # computing the tree depth
  depth == highest[1],
   
  # computing the number of unused nodes
  2 * z2 - 1 == depth
);

We run the solver on the current model, while indicating a timeout set to 10 seconds:

if solve(options="-t=10s") is SAT:
    print(values(x))

[-1, 0, 0, 0, 0, 0, 0, 0, 0, 1, 1, 1, 1, 1, 1, 1]

Then, we post complex constraints by using conjunction():

satisfy(
  # determining leaves
  [
    leaf[i] == conjunction(
      x[i] == VAL,
      left[i] == 0,
      right[i] == 0,
      highest[i] == i,
      lowest[i] == i,
      index[i] != 0
    ) for i in M
  ],

  # determining parents
  [
    parent[i] == conjunction(
      x[i] not in {VAL, NO},
      x[left[i]] != NO,
      x[right[i]] != NO,
      left[i] == i + 1,
      right[i] > left[i],
      right[i] == highest[left[i]] + 1,
      lowest[i] == i,
      highest[i] == highest[right[i]],
      index[i] == 0
    ) for i in M
  ],

  # determining unused elements
  [
    unused[i] == conjunction(
      x[i] in {NO, VAL},
      left[i] == 0,
      right[i] == 0,
      If(x[i] == VAL, Then=index[i] != 0),
      If(x[i] == NO, Then=index[i] == 0),
      lowest[i] == 0,
      highest[i] == 0
    ) for i in M
  ]
);

We run the solver on the extended model:

if solve(options="-t=10s") is SAT:
    print(values(x))

[-1, 0, 0, 0, 0, 0, 0, 0, 0, 1, 1, 1, 1, 1, 1, 1]

Next, we use the two functions If() (note that i <= depth is a constraint) and Match():

satisfy(
  # constraining leaves, parents and unused elements
  [
    If(
      i <= depth,
      Then=either(leaf[i], parent[i]),
      Else=unused[i]
    ) for i in M
  ],

  # computing values associated with all elements
  [
    Match(
      x[i],
      Cases={
        VAL: z1[i] == numbers[index[i]],
        ADD: z1[i] == z1[left[i]] + z1[right[i]],
        SUB: z1[i] == z1[left[i]] - z1[right[i]],
        MUL: z1[i] == z1[left[i]] * z1[right[i]],
        DIV: z1[i] * z1[right[i]] == z1[left[i]],
        NO: z1[i] == 0}
    ) for i in M
  ]
);

We run the solver on the current model:

if solve(options="-t=10s -di=0") is SAT:
    print(values(x))

[-1, 0, 5, 5, 0, 5, 0, 5, 0, 5, 5, 5, 0, 0, 0, 0]

It is also possible to post some symmetry-breaking constraints (but this is not certain that it helps the solver):

satisfy(
  # tag(symmetry-breaking)
  [
    # associativity
    [
      Match(
        x[i],
        Cases={
          ADD: x[left[i]] != ADD,
          MUL: x[left[i]] != MUL,
          SUB: x[left[i]] != SUB}
      ) for i in M
    ],

    # identity
    [
      [If(x[i] == ADD, Then=[z1[left[i]] != 0, z1[right[i]] != 0]) for i in M],
      [If(x[i] == MUL, Then=[z1[left[i]] != 1, z1[right[i]] != 1]) for i in M]
    ],
    
    # symmetry of addition and multiplication
    [If(x[i] in (ADD, MUL), Then=x[left[i]] <= x[right[i]]) for i in M],
    
    # distributivity of multiplication
    [
      If(
        x[i] in {ADD, SUB}, x[left[i]] == MUL, x[right[i]] == MUL,
        Then=[
          z1[left[left[i]]] != z1[left[right[i]]],
          z1[left[left[i]]] != z1[right[right[i]]],
          z1[right[left[i]]] != z1[left[right[i]]],
          z1[right[left[i]]] != z1[right[right[i]]]]
      ) for i in M
    ],
    
    # distributivity of division
    [
      If(
        x[i] in {ADD, SUB}, x[left[i]] == DIV, x[right[i]] == DIV,
        Then=z1[right[left[i]]] != z1[right[right[i]]]
      ) for i in M
    ],
    
    # conditions with respect to addition and multiplication
    [
     (
       If(x[i] == ADD, x[right[i]] == VAL, Then=x[left[i]] == VAL),
       If(x[i] == MUL, x[right[i]] == VAL, Then=x[left[i]] == VAL),
       If(
         x[i] == ADD, x[left[i]] == VAL, x[right[i]] == VAL,
         Then=index[left[i]] < index[right[i]]
       ),
       If(
         x[i] == MUL, x[left[i]] == VAL, x[right[i]] == VAL,
         Then=index[left[i]] < index[right[i]]
       ),
       If(
         x[i] == ADD, x[left[i]] == VAL, x[right[i]] == ADD, x[left[right[i]]]==VAL,
         Then=index[left[i]] < index[left[right[i]]]
       ),
       If(
         x[i] == MUL, x[left[i]] == VAL, x[right[i]] == MUL, x[left[right[i]]]==VAL,
         Then=index[left[i]] < index[left[right[i]]]
       )
     ) for i in M
    ],

    # all numbers with the same value should be assigned in sorted order
    [
      If(
        x[i] == VAL, x[j] == VAL, numbers[index[i]] == numbers[index[j]],
        Then=index[i] < index[j]
      ) for i, j in combinations(M, 2)
    ],
    
    # sorting nodes of equivalent value
    [If(z1[i] == z1[j], Then=x[i] >= x[j]) for i, j in combinations(M, 2)]
  ]
)

Using Reformulation

When using the complex structures If() and Match(), as well as the classical Python operators ‘|’, ‘\&’ and ‘~’, some reformulation mechanisms are automatically applied when compiling complex logic-based expressions (so as to stay within the limits of XCSP$³$-core).
It is then possible to logically combine (global) constraints.

We start an illustration by discarding everything that has been posted (both variables and constraints):

clear()

We start by introducing an array of variables $x$ and a stand-alone variable $y$.

x = VarArray(size=4, dom=range(4))
y = Var(range(-1, 4))

Let us see how reformulation is automatically applied with the following model:

satisfy(
    (Sum(x) > 10) | AllDifferent(x),
    
    If(y != -1, Then=x[y] == 1)
);

Note that for the first complex constraint, instead of using the operator ‘|’, we could equivalently write either(Sum(x) > 10, AllDifferent(x)), or If(Sum(x) <= 10, Then=AllDifferent(x)), or even imply(Sum(x) <= 10, AllDifferent(x)). Also, we could equivalently write for the second constraint (y == -1) | (x[y] == 1), or imply(y != -1, x[y] == 1), instead of using the function If().

When displaying the posted constraints, one can see that some auxiliary variables, called aux_gb, have been automatically introduced.

print(posted())

intension(function:or(gt(aux_gb[0],10),eq(aux_gb[1],4)))
intension(function:imp(ne(y,-1),eq(aux_gb[3],1)))
sum(list:[x[0], x[1], x[2], x[3]], condition:(eq,aux_gb[0]))
nValues(list:[x[0], x[1], x[2], x[3]], condition:(eq,aux_gb[1]))
element(list:[x[0], x[1], x[2], x[3]], index:aux_gb[2], condition:(eq,aux_gb[3]))
extension(list:[y, aux_gb[2]], supports:(-1,*)(0,0)(1,1)(2,2)(3,3))

We can find a solution:

if solve() is SAT:
    print(f" Solution : {values(x)} {value(y)}")

 Solution : [0, 1, 2, 3] -1

Precisely, one can observe that four auxiliary variables have been automatically introduced. The generated XCSP$^3$ instance has been the subject of some reformulation rules which, importantly, allow us to remain within the perimeter of XCSP$^3$-core. Actually, the main reformulation rule is the following: if a condition-based global constraint is involved in a complex formulation, it can be replaced by an auxiliary variable while ensuring apart that what is ‘computed’ by the constraint is equal to the value of the new introduced variable. For example, Sum(x) > 10 becomes aux > 10 while posting Sum(x) == aux apart (after having introduced the auxiliary variable aux). By proceeding that way, we obtain classical Intension constraints.

Many global constraints are condition-based, i.e., involve a condition in their statements. This is the case for:

• AllDifferent, since AllDifferent(x) is equivalent to NValues(x) == len(x)
• AllEqual, since AllEqual(x) is equivalent to NValues(x) == 1
• Sum
• Count
• NValues
• Minimum and Maximum
• Element
• Cumulative
• BinPacking (first form)
• Knapsack

Illustrations can be found for Stable Marriage, Diagnosis and Vellino models.

Using Tabulation

In this section, we claim modeling with tables can be relevant to logically combine involved constraints.

First, let us recall that table constraints are important in constraint programming because

• they are easily handled by end-users of constraint systems,
• they can be perceived as a universal modeling mechanism since any constraint can theoretically be expressed in tabular form (although this may lead to time/space explosion),
• sometimes, they happen to be simple and natural choices for dealing with tricky situations: this is the case when no adequate (global) constraint exists or when a logical combination of (small) constraints must be represented as a unique table constraint for efficiency reasons.

If ever needed, another argument showing the importance of universal structures like tables, and also diagrams, is the rising of (automatic) tabling techniques, i.e., the process of converting sub-problems into tables, by hand, using heuristics or by annotations.

The problems Amaze and Layout are two nice illustrations of the interest of tabling, the fact of reperesenting subsets of constraints by table constraints.

Posting Meta-Constraints

In PyCSP$^3$, some functions have been specifically introduced to build meta-constraints: And(), Or(), Not(), Xor() and Iff(). It is important to note that the first letter of these function names is uppercase. If one also wants to generate a meta-constraint form with the function If(), one has to specify the parameter meta with value True, because that function is usually employed for posting classical constraints (i.e., not meta-constraints).

As an illustration, we show how to capture the previous equations with meta-constraints. We start by introducing an array of variables $x$ and a stand-alone variable $i$.

unpost(ALL)

print(posted())

[]

We post the two meta-constraints:

satisfy(
   Or(Sum(x) > 10, AllDifferent(x)),
    
   If(y != -1, Then=x[y] == 1, meta=True)
);

We can display the internal representation of the two posted meta-constraints; this way, although a little bit technical, we can see that the meta-constraints are present (and not decomposed). Note that ‘gt’, ‘ne’ and ‘eq’ stands for ‘strictly greater than’, ‘not equal to’ and ‘equal to’.

print(posted())

or(sum(list:[x[0], x[1], x[2], x[3]], condition:(gt,10)),allDifferent(list:[x[0], x[1], x[2], x[3]]))
ifThen(intension(function:ne(y,-1)),element(list:[x[0], x[1], x[2], x[3]], index:aux_gb[4], condition:(eq,1)))
extension(list:[y, aux_gb[4]], supports:(-1,*)(0,0)(1,1)(2,2)(3,3))

As you can see, with meta-constraints, we can stay very close to the original (formal) formulation. Unfortunately, there is a price to pay: the generated instances are no more in the perimeter of XCSP$^3$-core (and consequently, it is not obvious to find an appropriate constraint solver to read such instances). Of course, in the future, some additional tools could be developed to offer the user the possibility of reformulating XCSP$^3$ instances (and possibly, the perimeter of XCSP$^3$-core could be slightly extended). Meanwhile, the solutions presented below should be chosen in priority.

Using Explicit Reification

Reification is the fact of representing the satisfaction value of certain constraints by means of Boolean variables. Reifying a constraint $c$ requires the introduction of an associated variable $b$ while considering the logical equivalence $b \Leftrightarrow c$. The two equations given earlier could be transformed by reifying three constraints, as follows:

$b_1 \Leftrightarrow \mathtt{Sum}(x) > 10$
$b_2 \Leftrightarrow \mathtt{AllDifferent}(x)$
$b_1 \lor b_2$

$b_3 \Leftrightarrow x[y] = 1$
$y \neq -1 \Rightarrow b_3$

Currently, there is no PyCSP$^3$ function (or mechanism) to deal with explicit reification (i.e., explicitly associating a Boolean variable with a reified constraint), although this is possible in XCSP$^3$. The main reason is that when reification is involved, XCSP$^3$ instances are no more in the perimeter of XCSP$^3$-core (and consequently, it is not obvious to find an appropriate constraint solver to read such instances). Actually, reification is outside the scope of XCSP$^3$-core because it complexifies the task of constraint solvers. Even if this restriction could be relaxed in the future (e.g., half reification), for the moment, we are not aware of any situation (based on our experience of having modeled more around 200 problems) that cannot be (efficiently) handled with the solutions presented in the three first sections of this notebook.