Link Search Menu Expand Document
PyCSP3
Documentation Data GitHub XCSP3 About
Documentation
XCSP web site is provided by CRIL
This site uses Just the Docs, a documentation theme for Jekyll.
download notebook

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 $i$ is an integer variable, the statement:

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

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

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

  • meta-constraints
  • reification
  • tabling
  • reformulation

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

from pycsp3 import *

Using Meta-Constraints

In PyCSP$^3$, some functions have been specifically introduced to build meta-constraints: And(), Or(), Not(), Xor(), IfThen(), IfThenElse() and Iff(). It is important to note that the first letter of these function names is uppercase.

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$.

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

We post the two meta-constraints:

satisfy(
   Or(Sum(x) > 10, AllDifferent(x)),
   IfThen(i != -1, x[i] == 1)
);

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())

extension(list:[i, aux_gb[0]], supports:(-1,*)(0,0)(1,1)(2,2)(3,3))
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(i,-1)),element(list:[x[0], x[1], x[2], x[3]], index:aux_gb[0], condition:(eq,1)))

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 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[i] = 1$
$i \neq -1 \Rightarrow b_3$

Currently, there is no PyCSP$^3$ function (or mechanism) to deal with reification, 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 modeling around 200 problems) that cannot be (efficiently) handled with the solutions presented below.

Using Tabling

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.

Using Reformulation

Earlier, we have seen that meta-constraint operators can be applied by calling specific PyCSP$^3$ functions And(), Or(), … But, what about using the classical Python operators ‘|’, ‘&’ and ‘~’? These operators, which are redefined in PyCSP$^3$, can be used to build constraints Intension, but also more complex forms obtained by logically combining (global) constraints.

We start by discarding all posted constraints:

unpost(ALL)

We can check that there are no more constraints:

print(posted())

[]

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

satisfy(
    (Sum(x) > 10) | AllDifferent(x),
    imply(i != -1, x[i] == 1)
);

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

print(posted())

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

We can find a solution:

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

 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.