Nogoods issue containing more than 2 laterals with at least one lateral "<=" or >

[mwahbi]

Hi @cprudhom, @jgFages,

I think there is a problem when using nogoods containing more than two laterals if one of them is not "eq" or "ne". I think that addLearnt in PropNogoods is not working as well. I got nothing after propagation when I use addLearnt() instead of addNogood(). For the problem above you can test the following example (I hope my usage of nogoods is correct). The problem is with ng2: not(x=1,y=1,c>3). If we use not(y=1,c>3) or not(y=1,c>3) it work perfectly, but not when it includes three laterals.

public class Example {
    public static void main(String[] args) {
        Model model = new Model("nogoods");
        PropNogoods ngstore = model.getNogoodStore().getPropNogoods();
        ngstore.initialize();
        IntVar x = model.intVar("x", -1, 1, false);
        IntVar y = model.intVar("y", 0, 2, false);
        IntVar z = model.intVar("z", 1, 5, false);

        int lb = 2, ub = 3;
        TIntList ng = new TIntArrayList();
        // ng1: not(x=1,z<=2)
        ng.add(SatSolver.negated(ngstore.Literal(x, 1, true)));
        ng.add(SatSolver.negated(ngstore.Literal(z, lb, false)));
        ngstore.addNogood(ng);
        // ng2: not(x=1,y=1,c>3)
        ng.clear();
        ng.add(SatSolver.negated(ngstore.Literal(x, 1, true)));
        ng.add(SatSolver.negated(ngstore.Literal(y, 1, true)));
        ng.add(ngstore.Literal(z, ub, false));
        ngstore.addNogood(ng);
        Solver solver = model.getSolver();
        try {
            solver.propagate();
        } catch (ContradictionException c) { }
        System.out.println(model);
        while (solver.solve()) {
            System.out.println(new Solution(model).record());
        }
    }
}

[cprudhom]

I'll have a look today and let you know.

[cprudhom]

Just to be sure, do you have an error on execution (due to assert violation) or do you have a wrong number of solutions ?

[mwahbi]

It was a SolverException. I got the following output error message:

Model[nogoods]

[ 4 vars -- 1 cstrs ] Feasability: UNDEFINED == variables == cste -- 1 = 1 x = {-1,0,1} y = {0,1,2} z = {1,2,3,4,5} == constraints == NogoodConstraint ([PropNogoods(x, z, y)])

Solution: x=-1, y=0, z=1, Solution: x=-1, y=0, z=2, Solution: x=-1, y=0, z=3, Solution: x=-1, y=0, z=4, Solution: x=-1, y=0, z=5, Solution: x=0, y=0, z=1, Solution: x=0, y=0, z=2, Solution: x=0, y=0, z=3, Solution: x=0, y=0, z=4, Solution: x=0, y=0, z=5, Solution: x=1, y=0, z=3, Solution: x=1, y=0, z=4, Solution: x=1, y=0, z=5, Solution: x=-1, y=1, z=1, Solution: x=-1, y=1, z=2, Solution: x=-1, y=1, z=3, Solution: x=-1, y=1, z=4, Solution: x=-1, y=1, z=5, Solution: x=0, y=1, z=1, Solution: x=0, y=1, z=2, Solution: x=0, y=1, z=3, Solution: x=0, y=1, z=4, Solution: x=0, y=1, z=5,

FAILURE >> NogoodConstraint ([PropNogoods(x, z, y)]) (FALSE) Exception in thread "main" org.chocosolver.solver.exception.SolverException: The current solution does not satisfy the checker.

##################################################

################################################## FAILURE >> NogoodConstraint ([PropNogoods(x, z, y)])

org.chocosolver.solver.search.strategy.decision.DecisionPath@42110406 SAT Model[nogoods], 23 Solutions, Resolution time 0.044s, 48 Nodes (1,090.9 n/s), 43 Backtracks, 0 Fails, 0 Restarts##################################################

at org.chocosolver.solver.Solver.searchLoop(Solver.java:337)
at org.chocosolver.solver.Solver.solve(Solver.java:265)
at org.chocosolver.Example.main(Example.java:45)
at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:62)
at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
at java.lang.reflect.Method.invoke(Method.java:497)
at com.intellij.rt.execution.application.AppMain.main(AppMain.java:147)

[cprudhom]

Fixed in 5d0e02dcb30a693a189e939afeb0ccdb27fd4040