Getting inconsistent model after translating a minizinc constraint to Gecode MiniModel.

[sirwhinesalot]

Describe the bug

Adding the following constraint to my model causes it to become inconsistent in Gecode (0 solutions, Gist shows an empty tree) but it works fine in MiniZinc with Gecode as the backend:

constraint forall(n in 0..3)(parent[n] > -1 -> (dist[n] = dist[parent[n]] + 1));

for (int i = 0; i <= 3; i++) {
  rel(*this, (parent[i] > -1) >> (dist[i] == (element(dist, parent[i]) + 1)));
}

To Reproduce

I can provide the full files if needed.

Gecode and Platform Configuration

I'm using Gecode 6.3.0 (statically linked to a C++ executable) on macOS 13.1 with Clang 14 as the compiler.

EDIT:

The problem seems to be the interaction between parent and the element constraint, if I replace parent == -1 as the "invalid" id with parent == 4, and add a fake dist[4] == 0, it has the opposite problem, it doesn't remove any solutions.

[zayenz]

Without seeing the whole models, I have a hard time seeing what the problem might be.

Given the edit, I'm wondering if you might have any issues with indexing outside of arrays, as that has tricky semantic implications.

[sirwhinesalot]

Hi Mikael,

I think it might be related to indexing outside of arrays (as the "fix" makes the model possible to solve). I ultimately solved it by using a different encoding of the problem (network flow), but here's my minizinc original and corresponding gecode example:

array[0..3] of var bool: ns ::add_to_output;

var bool: n_0__n_2 ::add_to_output;
var bool: n_1__n_2 ::add_to_output;
var bool: n_0__n_3 ::add_to_output;
var bool: n_1__n_3 ::add_to_output;

constraint n_0__n_2 -> (ns[0] /\ ns[2]);
constraint n_1__n_2 -> (ns[1] /\ ns[2]);
constraint n_0__n_3 -> (ns[0] /\ ns[3]);
constraint n_1__n_3 -> (ns[1] /\ ns[3]);

var 0..3: root;
set of int: NODE = 0..3;
array[0..3] of var 0..3: dist;
array[0..3] of var -1..3: parent;

constraint ns[root];
constraint dist[root] = 0;

% nonselected nodes have parent -1
constraint forall(n in NODE)(not ns[n] -> parent[n] = -1);

% nonselected nodes have distance 0
constraint forall(n in NODE)(not ns[n] -> dist[n] = 0);

% each in node except root must have a parent
constraint forall(n in NODE)(ns[n] -> (n = root \/ parent[n] > -1));

% each in node with a parent must be in and also its parent
constraint forall(n in NODE)(parent[n] > -1 -> (ns[n] /\ ns[parent[n]]));

% each except with a parent is one more than its parent
constraint forall(n in NODE)(parent[n] > -1 -> (dist[n] = dist[parent[n]] + 1));

constraint (parent[0] > -1) -> ((parent[0] == 2 /\ n_0__n_2) \/ (parent[0] == 3 /\ n_0__n_3));
constraint (parent[1] > -1) -> ((parent[1] == 2 /\ n_1__n_2) \/ (parent[1] == 3 /\ n_1__n_3));
constraint (parent[2] > -1) -> ((parent[2] == 0 /\ n_0__n_2) \/ (parent[2] == 1 /\ n_1__n_2));
constraint (parent[3] > -1) -> ((parent[3] == 0 /\ n_0__n_3) \/ (parent[3] == 1 /\ n_1__n_3));

solve satisfy;

This has 17 solutions.

#include "gecode/driver.hh"
#include "gecode/int.hh"
#include "gecode/minimodel.hh"
#include "gecode/search.hh"

struct Model : public Gecode::Space {
    Gecode::BoolVarArray ns;
    Gecode::BoolVar n_0__n_2;
    Gecode::BoolVar n_0__n_3;
    Gecode::BoolVar n_1__n_2;
    Gecode::BoolVar n_1__n_3;

    Model()
        : ns(*this, 5, 0, 1),
          n_0__n_2(*this, 0, 1),
          n_0__n_3(*this, 0, 1),
          n_1__n_2(*this, 0, 1),
          n_1__n_3(*this, 0, 1) {

        // Using -1 as the invalid parent instead of 4 results in 0 solutions
        Gecode::IntVar root(*this, 0, 3);
        Gecode::IntVarArgs dist(*this, 5, 0, 3);
        Gecode::IntVarArgs parent(*this, 4, 0, 4);

        Gecode::rel(*this, n_0__n_2 >> (ns[0] && ns[2]));
        Gecode::rel(*this, n_1__n_2 >> (ns[1] && ns[2]));
        Gecode::rel(*this, n_0__n_3 >> (ns[0] && ns[3]));
        Gecode::rel(*this, n_1__n_3 >> (ns[1] && ns[3]));

        Gecode::rel(*this, ns[4] == 0);
        Gecode::rel(*this, dist[4] == 0);
        Gecode::rel(*this, Gecode::element(ns, root));
        Gecode::rel(*this, Gecode::element(dist, root) == 0);
        Gecode::rel(*this, Gecode::element(parent, root) == 4);

        for (int i = 0; i <= 3; i++) {
            // nonselected nodes have parent -1
            Gecode::rel(*this, !ns[i] >> (parent[i] == 4));

            // nonselected nodes have distance 0
            Gecode::rel(*this, !ns[i] >> (dist[i] == 0));

            // each in node except root must have a parent
            Gecode::rel(*this, ns[i] >> ((root == i) || (parent[i] < 4)));

            // each in node with a parent must be in and also its parent
            Gecode::rel(*this, (parent[i] < 4) >> ns[i]);
            Gecode::rel(*this, (parent[i] < 4) >> Gecode::element(ns, parent[i]));

            // each except with a parent is one more than its parent
            Gecode::rel(*this, (parent[i] < 4) >> (dist[i] == (Gecode::element(dist, parent[i]) + 1)));
        }

        Gecode::rel(*this, (parent[0] < 4) >> (((parent[0] == 2) && n_0__n_2) || ((parent[0] == 3) && n_0__n_3)));
        Gecode::rel(*this, (parent[1] < 4) >> (((parent[1] == 2) && n_1__n_2) || ((parent[1] == 3) && n_1__n_3)));
        Gecode::rel(*this, (parent[2] < 4) >> (((parent[2] == 0) && n_0__n_2) || ((parent[2] == 1) && n_1__n_2)));
        Gecode::rel(*this, (parent[3] < 4) >> (((parent[3] == 0) && n_0__n_3) || ((parent[3] == 1) && n_1__n_3)));

        Gecode::BoolVarArgs all_bools{ns};
        all_bools << n_0__n_2;
        all_bools << n_0__n_3;
        all_bools << n_1__n_2;
        all_bools << n_1__n_3;
        Gecode::IntVarArgs all_ints{parent};
        Gecode::branch(*this, all_bools, Gecode::BOOL_VAR_NONE(), Gecode::BOOL_VAL_MIN());
        Gecode::branch(*this, all_ints, Gecode::INT_VAR_NONE(), Gecode::INT_VAL_MIN());
    }

    Model(Model& s) : Space(s) {
        ns.update(*this, s.ns);
        n_0__n_2.update(*this, s.n_0__n_2);
        n_0__n_3.update(*this, s.n_0__n_3);
        n_1__n_2.update(*this, s.n_1__n_2);
        n_1__n_3.update(*this, s.n_1__n_3);
    }

    Space* copy() { return new Model(*this); }
};

int main(int argc, char** argv) {
    Model model;
    int count = 0;
    Gecode::DFS<Model> search(&model);
    while (Model* s = search.next()) {
        count += 1;
        delete s;
    }
    std::cout << count << "\n";

This has 56 solutions. If I replace the 4 and related array elements with a -1 like in MiniZinc, I get 0.

[zayenz]

That explains it then. Indexing outside of arrays is a tricky subject. MiniZinc has special semantics that is handles when translating into the input to solvers such as Gecode (see https://www.minizinc.org/doc-2.7.6/en/modelling2.html#partiality-and-relational-semantics).

Gecode on the other hand does not have this, as it is not really a modelling language although it does have some minimal modelling support. In Particular, the reified element version that you used will post a regular element and then check the resulting value for equality. That will unfortunately for you still require that the index is valid.