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();
// ng: 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);
// 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();
//Assert.assertTrue(var.isInstantiatedTo(-1));
} catch (ContradictionException c) {
c.printStackTrace();
}
System.out.println(model);
while (solver.solve()) {
System.out.println(new Solution(model).record());
}
}
}
cprudhom
commented
8 years ago
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(); // ng: 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); // 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(); //Assert.assertTrue(var.isInstantiatedTo(-1)); } catch (ContradictionException c) { c.printStackTrace(); } System.out.println(model); while (solver.solve()) { System.out.println(new Solution(model).record()); } } }