Skip to content

Post predicate in MiniSearch apparently not posting the constraint  #5

@jacopoMauro

Description

@jacopoMauro

It seems that the post predicate in minisearch is not properly behaving.

Consider for instance the following program that is using an array of 4 variables with 0..1 domain.

include "minisearch.mzn";

% locations
set of int: locations;
locations = 1..4;
array[ locations ] of var 0..1: used_locations;

constraint sum( used_locations ) = 3; 

function ann: test1(array[int] of var int: used_locations) = (
    next() /\  
    commit() /\
    print() /\
      repeat (i in 1..5) (
        print("% Enter iteration " ++ show(i) ++ "\n") /\
        let {
          int: a = 0;
          int: b = 0;
        } in (
          a := uniform(1,length(used_locations)) /\
          b := uniform(1,length(used_locations)) /\
          if sol(used_locations[a]) > sol(used_locations[b])
          then
            print("% Trying to swap " ++ show(a) ++ " with " ++ show(b) ++ "\n") /\
            scope(
              post(
               used_locations[a] = 0 /\ trace("used_locations[" ++ show(a) ++"] = 0" ++ "\n") /\
               forall (i in index_set(used_locations))(
                 if i != a /\ i != b
                 then used_locations[i] = sol(used_locations[i])
                 else true endif) 
              ) /\
              repeat (next() /\ commit() /\ print() \/ break)
            )
          else skip endif
        )
      )
);

solve search test1(used_locations);

output ["used locations: "++show(used_locations)];

Initially I ask that 3 of the 4 variables are set to be 1. Then I try to find a solution.
As soon as I have a solution I try to swap the value of the variable a having sol(a) = 0 with another variable preserving the value of the other two variables. I do this by posting the constraint used_locations[a] = 0. At this point I search for all the possible solutions of the problem. I was expecting in output just one solution (only one solution exists) but instead I got 4 different outputs that are inconsistent with the constraint that I added using the post predicate.

The output look indeed as:

% Enter iteration 5
% Trying to swap 3 with 4
used_locations[3] = 0
used locations: [1, 1, 1, 0]
----------
used locations: [1, 1, 0, 1]
----------
used locations: [1, 0, 1, 1]
----------
used locations: [0, 1, 1, 1]
----------
==========

It seems that the constraints added by using the post predicate are not added into the model.
Is this a bug?

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions