Skip to content

Commit

Permalink
Choco3: AllDifferentExcept0.java
Browse files Browse the repository at this point in the history
  • Loading branch information
@hakank
hakank committed Dec 23, 2013
1 parent 5b1602c commit 00a087c
Showing 1 changed file with 30 additions and 49 deletions.
79 changes: 30 additions & 49 deletions choco3/AllDifferentExcept0.java
View file
Expand Up @@ -23,10 +23,12 @@
import solver.constraints.Constraint;
import solver.constraints.IntConstraintFactory;
import solver.constraints.IntConstraintFactory.*;
import solver.constraints.nary.cnf.Literal;
import solver.constraints.nary.cnf.Node;
import solver.constraints.nary.cnf.Node.*;
import solver.constraints.nary.cnf.ALogicTree;
import solver.constraints.LogicalConstraintFactory;
import solver.constraints.SatFactory;
import solver.constraints.nary.cnf.ILogical;
import solver.constraints.nary.cnf.LogOp;
import solver.constraints.nary.cnf.LogicTreeToolBox;

import solver.search.strategy.IntStrategyFactory;
import solver.variables.IntVar;
import solver.variables.BoolVar;
Expand All @@ -35,7 +37,7 @@

public class AllDifferentExcept0 extends AbstractProblem {

@Option(name = "-n", usage = "n, size of array (default 6).", required = false)
@Option(name = "-n", usage = "n, size of array (default 4).", required = false)
int n = 4;

@Option(name = "-m", usage = "Max value (default n).", required = false)
Expand All @@ -62,7 +64,7 @@ public void allDifferentExceptC(IntVar[] v, int c) {
for(int j = i+1; j < v.length; j++) {

// if v[i] != c && v[j] != c -> v[i] != v[j]
// Alternative approach
// Alternative approach:
// a[i] != c) * (a[j] != c) <= (a[i] != a[j])

/*
Expand All @@ -78,53 +80,32 @@ public void allDifferentExceptC(IntVar[] v, int c) {
);
*/

// 2013-04-15/hakank: How do I a similar construct in Choco3?

//
// This works but is way too complex to be natural...
//
BoolVar[] b = VariableFactory.boolArray("b_"+i+"_"+j, 3, solver);
solver.post(LogicalConstraintFactory.ifThenElse(b[0],
IntConstraintFactory.arithm(v[i], "!=", c),
IntConstraintFactory.arithm(v[i], "=", c)));

solver.post(LogicalConstraintFactory.ifThenElse(b[1],
IntConstraintFactory.arithm(v[j], "!=", c),
IntConstraintFactory.arithm(v[j], "=", c)));


solver.post(LogicalConstraintFactory.ifThenElse(b[2],
IntConstraintFactory.arithm(v[i], "!=", v[j]),
IntConstraintFactory.arithm(v[i], "=", v[j])));

// Note: As stated in IntConstraintFactory.java, we have to state both ways
// of implies, i.e.
// B => C
// not(B) => "not"(C)
//
solver.post(IntConstraintFactory.implies(
b[0],
(IntConstraintFactory.arithm(v[i], "!=", c))));
solver.post(IntConstraintFactory.implies(
VariableFactory.not(b[0]),
(IntConstraintFactory.arithm(v[i], "=", c))));

solver.post(IntConstraintFactory.implies(
b[1],
(IntConstraintFactory.arithm(v[j], "!=", c))));
solver.post(IntConstraintFactory.implies(
VariableFactory.not(b[1]),
(IntConstraintFactory.arithm(v[j], "=", c))));

solver.post(IntConstraintFactory.implies(
b[2],
(IntConstraintFactory.arithm(v[i], "!=", v[j]))));
solver.post(IntConstraintFactory.implies(
VariableFactory.not(b[2]),
(IntConstraintFactory.arithm(v[i], "=", v[j]))));

// b[0] * b[1] <= b[2]
/*
IntVar b01 = VariableFactory.enumerated("b2", 0, 1, solver);
solver.post(IntConstraintFactory.times(b[0], b[1], b01));
solver.post(IntConstraintFactory.arithm(b01, "<=", b[2]));
*/

// This works as well (and is a little more natural the variant above):
// if b[0] && b[1] -> b[2]
ALogicTree t = Node.implies(
Node.and(Literal.pos(b[0]), Literal.pos(b[1])),
Literal.pos(b[2])
);
solver.post(IntConstraintFactory.clauses(t, solver));
// I haven't got it to work with implies so I rely on the MIP trick
// for implication, i.e. b[0] * b[1] <= b[2].
// LogOp root = LogOp.implies(LogOp.and(b[0], b[1]), b[2]);
// ILogical l = LogicTreeToolBox.toCNF(root, solver);
// System.out.println("l: " + l);

IntVar t = VariableFactory.enumerated("t", 0, 2, solver);
solver.post(IntConstraintFactory.times(b[0],b[1],t));
solver.post(IntConstraintFactory.arithm(t,"<=",b[2])); // b[0]*b[1] <= b[2]


}
}
Expand Down

2 comments on commit 00a087c

@brahimbo
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

hi Hakank, i copy this code in eclipse but the error is in line 84 in post:
solver.post(LogicalConstraintFactory.ifThenElse(b[0],

  •                                                    IntConstraintFactory.arithm(v[i], "!=", c),

  •                                                    IntConstraintFactory.arithm(v[i], "=", c)));
    in post the error is: The method post(Constraint) in the type Solver is not applicable for the arguments (void) : 2 quick fixes availibale change to postTemp(...) or unpost(...) but i can't find the solution thank .you

@cprudhom
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Hi Brahimbo,
The post of Hakank is now out of date.
A constraint declared thanks to LogicalConstraintFactory does no longer need to be posted, its declaration implies its addition to the solver. This to avoid reifying such type of constraints.

Please sign in to comment.