{ "cells": [ { "cell_type": "markdown", "id": "ac658db4", "metadata": {}, "source": [ "# Logically Combining Constraints" ] }, { "cell_type": "markdown", "id": "84d00330", "metadata": {}, "source": [ "When modeling, it happens that, for some problems, constraints must be logically combined.\n", "For example, assuming that \$x\$ is a 1-dimensional array of variables, the statement: \n", "> Sum(x) > 10 or AllDifferent(x)\n", "\n", "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:\n", "> \$i \\neq -1 \\Rightarrow x[i] = 1\$\n", "\n", "enforces that when the value of \$i\$ is different from \$-1\$ then the value in \$x\$ at index \$i\$ must be equal to 1.\n", "\n", "The question is: how can we deal with such situations?\n", "The answer is multiple, as we can use:\n", "- meta-constraints\n", "- reification\n", "- tabling\n", "- reformulation" ] }, { "cell_type": "markdown", "id": "2dc54ec8", "metadata": {}, "source": [ "To illustrate how it works, we need first to import the library PyCSP\$^3\$:" ] }, { "cell_type": "code", "execution_count": 1, "id": "f7ddce1d", "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "\n", " \u001b[93mWarning: \u001b[0mUnknown option: -f\n", "\n" ] } ], "source": [ "from pycsp3 import *" ] }, { "cell_type": "markdown", "id": "ffe8eb6f", "metadata": {}, "source": [ "## Using Meta-Constraints" ] }, { "cell_type": "markdown", "id": "b7a86910", "metadata": {}, "source": [ "In PyCSP\$^3\$, some functions have been specifically introduced to build meta-constraints: *And()*, *Or()*, *Not()*, *Xor()*, *IfThen()*, *IfThenElse()* and *Iff()*.\n", "It is important to note that the first letter of these function names is uppercase." ] }, { "cell_type": "markdown", "id": "d139477c", "metadata": {}, "source": [ "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\$." ] }, { "cell_type": "code", "execution_count": 2, "id": "9442fa63", "metadata": {}, "outputs": [], "source": [ "x = VarArray(size=4, dom=range(4))\n", "i = Var(range(-1, 4))" ] }, { "cell_type": "markdown", "id": "584fc556", "metadata": {}, "source": [ "We post the two meta-constraints:" ] }, { "cell_type": "code", "execution_count": 3, "id": "182ed7e2", "metadata": {}, "outputs": [], "source": [ "satisfy(\n", " Or(Sum(x) > 10, AllDifferent(x)),\n", " IfThen(i != -1, x[i] == 1)\n", ");" ] }, { "cell_type": "markdown", "id": "c807416e", "metadata": {}, "source": [ "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'." ] }, { "cell_type": "code", "execution_count": 4, "id": "b5e14d71", "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "or(sum(list:[x, x, x, x], condition:(gt,10)),allDifferent(list:[x, x, x, x]))\n", "ifThen(intension(function:ne(i,-1)),element(list:[x, x, x, x], index:i, condition:(eq,1)))\n" ] } ], "source": [ "print(posted())" ] }, { "cell_type": "markdown", "id": "5ff8d9be", "metadata": {}, "source": [ "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. " ] }, { "cell_type": "markdown", "id": "c3403c82", "metadata": {}, "source": [ "## Using Reification" ] }, { "cell_type": "markdown", "id": "c980f488", "metadata": {}, "source": [ "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:\n", "> \$b_1 \\Leftrightarrow \\mathtt{Sum}(x) > 10\$
\n", "> \$b_2 \\Leftrightarrow \\mathtt{AllDifferent}(x)\$
\n", "> \$b_1 \\lor b_2\$
\n", "\n", "> \$b_3 \\Leftrightarrow x[i] = 1\$