@Test(groups="1s", timeOut=60000) public void testDeclareDomainNogood(){ IntVar var = vars[0].getModel().intVar("X4", -1, 1, false); PNG.declareDomainNogood(var); try{ PNG.doReduce(13); Assert.assertTrue(var.isInstantiatedTo(-1)); }catch (ContradictionException c){ Assert.fail(); } }
boolean declareDomainNogood(IntVar var) { int size = var.getDomainSize(); int[] lits = new int[size * 2]; int a = var.getLB(); int ub = var.getUB(); int i = 0; while (a <= ub) { lits[i] = Literal(var, a, true); lits[i + size] = Literal(var, a, false); i++; a = var.nextValue(a); } TIntList clauses = new TIntArrayList(); boolean add = false; for (int j = size; j < 2 * size - 1; j++) { clauses.add(negated(lits[j])); clauses.add(lits[j + 1]); add |= sat_.addClause(clauses); clauses.clear(); } for (int k = 0; k < size - 1; k++) { clauses.add(lits[k]); clauses.add(negated(lits[size + k])); clauses.add(lits[size + k + 1]); add |= sat_.addClause(clauses); clauses.clear(); clauses.add(negated(lits[k])); clauses.add(lits[size + k]); add |= sat_.addClause(clauses); clauses.clear(); clauses.add(negated(lits[k])); clauses.add(negated(lits[size + k + 1])); add |= sat_.addClause(clauses); clauses.clear(); } storeEarlyDeductions(); return add; }
PropNogoods extends Propagator<Variable> { boolean declareDomainNogood(IntVar var) { int size = var.getDomainSize(); int[] lits = new int[size * 2]; int a = var.getLB(); int ub = var.getUB(); int i = 0; while (a <= ub) { lits[i] = Literal(var, a, true); lits[i + size] = Literal(var, a, false); i++; a = var.nextValue(a); } TIntList clauses = new TIntArrayList(); boolean add = false; for (int j = size; j < 2 * size - 1; j++) { clauses.add(negated(lits[j])); clauses.add(lits[j + 1]); add |= sat_.addClause(clauses); clauses.clear(); } for (int k = 0; k < size - 1; k++) { clauses.add(lits[k]); clauses.add(negated(lits[size + k])); clauses.add(lits[size + k + 1]); add |= sat_.addClause(clauses); clauses.clear(); clauses.add(negated(lits[k])); clauses.add(lits[size + k]); add |= sat_.addClause(clauses); clauses.clear(); clauses.add(negated(lits[k])); clauses.add(negated(lits[size + k + 1])); add |= sat_.addClause(clauses); clauses.clear(); } storeEarlyDeductions(); return add; } }
PropNogoods extends Propagator<Variable> { boolean declareDomainNogood(IntVar var) { int size = var.getDomainSize(); int[] lits = new int[size * 2]; int a = var.getLB(); int ub = var.getUB(); int i = 0; while (a <= ub) { lits[i] = Literal(var, a, true); lits[i + size] = Literal(var, a, false); i++; a = var.nextValue(a); } TIntList clauses = new TIntArrayList(); boolean add = false; for (int j = size; j < 2 * size - 1; j++) { clauses.add(negated(lits[j])); clauses.add(lits[j + 1]); add |= sat_.addClause(clauses); clauses.clear(); } for (int k = 0; k < size - 1; k++) { clauses.add(lits[k]); clauses.add(negated(lits[size + k])); clauses.add(lits[size + k + 1]); add |= sat_.addClause(clauses); clauses.clear(); clauses.add(negated(lits[k])); clauses.add(lits[size + k]); add |= sat_.addClause(clauses); clauses.clear(); clauses.add(negated(lits[k])); clauses.add(negated(lits[size + k + 1])); add |= sat_.addClause(clauses); clauses.clear(); } storeEarlyDeductions(); return add; } PropNogoods(Model model); }
PropNogoods extends Propagator<Variable> { boolean declareDomainNogood(IntVar var) { int size = var.getDomainSize(); int[] lits = new int[size * 2]; int a = var.getLB(); int ub = var.getUB(); int i = 0; while (a <= ub) { lits[i] = Literal(var, a, true); lits[i + size] = Literal(var, a, false); i++; a = var.nextValue(a); } TIntList clauses = new TIntArrayList(); boolean add = false; for (int j = size; j < 2 * size - 1; j++) { clauses.add(negated(lits[j])); clauses.add(lits[j + 1]); add |= sat_.addClause(clauses); clauses.clear(); } for (int k = 0; k < size - 1; k++) { clauses.add(lits[k]); clauses.add(negated(lits[size + k])); clauses.add(lits[size + k + 1]); add |= sat_.addClause(clauses); clauses.clear(); clauses.add(negated(lits[k])); clauses.add(lits[size + k]); add |= sat_.addClause(clauses); clauses.clear(); clauses.add(negated(lits[k])); clauses.add(negated(lits[size + k + 1])); add |= sat_.addClause(clauses); clauses.clear(); } storeEarlyDeductions(); return add; } PropNogoods(Model model); @Override void propagate(int evtmask); @Override void propagate(int idxVarInProp, int mask); @Override ESat isEntailed(); void initialize(); int Literal(IntVar ivar, int value, boolean eq); int Literal(SetVar svar, int value, boolean in); @SuppressWarnings("unused") boolean addNogood(int p); @SuppressWarnings("unused") boolean addNogood(TIntList lits); void addLearnt(int... lits); }
PropNogoods extends Propagator<Variable> { boolean declareDomainNogood(IntVar var) { int size = var.getDomainSize(); int[] lits = new int[size * 2]; int a = var.getLB(); int ub = var.getUB(); int i = 0; while (a <= ub) { lits[i] = Literal(var, a, true); lits[i + size] = Literal(var, a, false); i++; a = var.nextValue(a); } TIntList clauses = new TIntArrayList(); boolean add = false; for (int j = size; j < 2 * size - 1; j++) { clauses.add(negated(lits[j])); clauses.add(lits[j + 1]); add |= sat_.addClause(clauses); clauses.clear(); } for (int k = 0; k < size - 1; k++) { clauses.add(lits[k]); clauses.add(negated(lits[size + k])); clauses.add(lits[size + k + 1]); add |= sat_.addClause(clauses); clauses.clear(); clauses.add(negated(lits[k])); clauses.add(lits[size + k]); add |= sat_.addClause(clauses); clauses.clear(); clauses.add(negated(lits[k])); clauses.add(negated(lits[size + k + 1])); add |= sat_.addClause(clauses); clauses.clear(); } storeEarlyDeductions(); return add; } PropNogoods(Model model); @Override void propagate(int evtmask); @Override void propagate(int idxVarInProp, int mask); @Override ESat isEntailed(); void initialize(); int Literal(IntVar ivar, int value, boolean eq); int Literal(SetVar svar, int value, boolean in); @SuppressWarnings("unused") boolean addNogood(int p); @SuppressWarnings("unused") boolean addNogood(TIntList lits); void addLearnt(int... lits);  }