Skip to content

Commit b5d6c7b

Browse files
committed
Pull Request : cleaning in progress
1 parent 663a936 commit b5d6c7b

File tree

3 files changed

+101
-141
lines changed

3 files changed

+101
-141
lines changed

solver/src/main/java/org/chocosolver/solver/constraints/nary/alldifferent/algo/AlgoAllDiffBimodal.java

Lines changed: 69 additions & 97 deletions
Original file line numberDiff line numberDiff line change
@@ -43,47 +43,51 @@ public class AlgoAllDiffBimodal implements IAlldifferentAlgorithm {
4343
public static final String PARTIAL = "AC_PARTIAL";
4444
public static final String TUNED = "AC_TUNED";
4545

46+
public static final int BFS = 0;
47+
public static final int DFS = 1;
48+
public static final int PRUNE = 2;
49+
4650
Propagator<IntVar> aCause;
4751
Model model;
4852
protected IntVar[] vars;
4953
private final int R; // Total number of variables
50-
private TrackingList variablesDynamic; // The dynamic list of uninstantiated variables
54+
private final TrackingList variablesDynamic; // The dynamic list of uninstantiated variables
5155
private final int minValue;
5256
private final int maxValue;
5357
private final int D; // Total number of values
54-
private TrackingList valuesDynamic; // The dynamic list of values present in the domain of at least one variable and not matched to an instantiated variable
58+
private final TrackingList valuesDynamic; // The dynamic list of values present in the domain of at least one variable and not matched to an instantiated variable
5559
private final int fail; // Symbol signifying we couldn't find an augmenting path
56-
private BipartiteMatching matching; // The matching used dynamically
57-
private int[] parentBFS; // Array storing the parent of each value-node in the BFS tree
58-
private int[] queueBFS; // Queue of the variables to explore during the BFS
60+
private final BipartiteMatching matching; // The matching used dynamically
61+
private final int[] parentBFS; // Array storing the parent of each value-node in the BFS tree
62+
private final int[] queueBFS; // Queue of the variables to explore during the BFS
5963
private int headBFS;
6064
private int tailBFS;
6165
private int minValSearchedNodes; // For failure explanation
6266
private int maxValSearchedNodes; // For failure explanation
6367
private final int t_node; // Symbol representing the artificial sink node of the Residual Graph
64-
private TrackingList complementSCC; // List of the values that are not in the discovered SCC
65-
private int[] tarjanStack; // The stack used in Tarjan's algorithm to find the SCCs
68+
private final TrackingList complementSCC; // List of the values that are not in the discovered SCC
69+
private final int[] tarjanStack; // The stack used in Tarjan's algorithm to find the SCCs
6670
private int topTarjan;
67-
private boolean[] inStack; // Boolean array informing the presence of a value in the stack
68-
private int[] pre; // Pre visit order of the values
69-
private int[] low; // Low point of the values
71+
private final boolean[] inStack; // Boolean array informing the presence of a value in the stack
72+
private final int[] pre; // Pre visit order of the values
73+
private final int[] low; // Low point of the values
7074
private int numVisit; // Current visit number of the DFS in Tarjan's algorithm
7175
private boolean firstSCC; // Indicates if the discovered SCC is the first discovered one in the current propagation
7276
private final String mode; // Indicating the mode in which we are using the procedure (Classic, Complement, Hybrid or Tuned)
7377
private boolean pruned; // True if some variable-value pairs were pruned
7478

75-
private int[] SCCpartition; // Partition of the values relative to the SCCs
76-
private int[] SCCindices; // End point of each SCC in the partition
79+
private final int[] sccPartition; // Partition of the values relative to the SCCs
80+
private final int[] sccIndices; // End point of each SCC in the partition
7781
private int numberOfSCCs;
78-
private int[] SCCbelonging; // index of the SCC each value belongs to
79-
private int[] upToDateSCC; // indicating for each value if its SCC has been updated in this call
82+
private final int[] sccBelonging; // index of the SCC each value belongs to
83+
private final int[] upToDateSCC; // indicating for each value if its SCC has been updated in this call
8084
private int updateKey; // This key is incremented at each call, to reset the upToDate information
8185

8286
//***********************************************************************************
8387
// CONSTRUCTORS
8488
//***********************************************************************************
8589

86-
public AlgoAllDiffBimodal(IntVar[] variables, Propagator<IntVar> cause, String ACmode) {
90+
public AlgoAllDiffBimodal(IntVar[] variables, Propagator<IntVar> cause, String acMode) {
8791
// Variables and data structures for the whole procedure
8892
this.aCause = cause;
8993
this.model = variables[0].getModel();
@@ -104,7 +108,7 @@ public AlgoAllDiffBimodal(IntVar[] variables, Propagator<IntVar> cause, String A
104108
this.fail = minValue - 1;
105109
this.matching = new BipartiteMatching(0, R-1, minValue, maxValue);
106110

107-
this.mode = ACmode;
111+
this.mode = acMode;
108112

109113
// Specific data structures for finding the maximum matching
110114
this.parentBFS = new int[D];
@@ -123,10 +127,10 @@ public AlgoAllDiffBimodal(IntVar[] variables, Propagator<IntVar> cause, String A
123127
this.low = new int[D];
124128

125129
// Specific data structures for generating the explanations
126-
this.SCCpartition = new int[D];
127-
this.SCCindices = new int[D];
130+
this.sccPartition = new int[D];
131+
this.sccIndices = new int[D];
128132
this.numberOfSCCs = 0;
129-
this.SCCbelonging = new int[D];
133+
this.sccBelonging = new int[D];
130134
this.upToDateSCC = new int[D];
131135
this.updateKey = 0;
132136
}
@@ -150,16 +154,11 @@ private void refineUniverse(TrackingList valueUniverse) { // The tracking list i
150154

151155
public boolean propagate() throws ContradictionException {
152156
this.pruned = false;
157+
// propInstDependant is set to false by default, meaning that this propagator does not require the Instantiation Propagator to be called just before
153158
updateDynamicStructuresOpening(false);
154-
boolean foundMatching = findMaximumMatching();
155-
if(foundMatching) {
156-
filter();
157-
updateDynamicStructuresEnding();
158-
}
159-
//NOTE: don't need anymore because of generateFailureExplanation
160-
// else {
161-
// vars[0].instantiateTo(vars[0].getLB() - 1, aCause);
162-
// }
159+
findMaximumMatching();
160+
filter();
161+
updateDynamicStructuresEnding();
163162
return this.pruned;
164163
}
165164

@@ -168,7 +167,7 @@ public boolean propagate() throws ContradictionException {
168167
//***********************************************************************************
169168

170169

171-
private boolean findMaximumMatching() throws ContradictionException {
170+
private void findMaximumMatching() throws ContradictionException {
172171
complementSCC.refill(); // This will be used to find the cut for a failure explanation
173172
int var = variablesDynamic.getSource();
174173
while (variablesDynamic.hasNext(var)) { // We increase the size of the current matching until no unmatched variable remains
@@ -181,16 +180,11 @@ private boolean findMaximumMatching() throws ContradictionException {
181180
}
182181
else {
183182
// It is not possible to get a maximum matching --> the constraint can not be satisfied
184-
//NOTE: BUG FOUND ---> when an exception is raised, the refill operation is not call and the structure of the tracking list is broken
185-
//NOTE: solution ---> integrate the refill operation in the generateFailureExplanation() method, before raising the exception
186183
generateFailureExplanation();
187-
// valuesDynamic.refill(); // valuesDynamic is a backtrackable TrackingList, we must refill it to avoid breaking its structure while backtracking
188-
return false;
189184
}
190185
}
191186
}
192187
valuesDynamic.refill(); // valuesDynamic is a global variable used in the whole filtering procedure, so we must refill it
193-
return true;
194188
}
195189

196190

@@ -219,7 +213,7 @@ private int augmentingPath(int root) {
219213
int var = queueBFS[headBFS];
220214
headBFS++;
221215
int val;
222-
if (choiceBimodalBFS(var)) { // If var has a small domain, we iterate over its domain and explore the unvisited values
216+
if (choice(BFS, var)) { // If var has a small domain, we iterate over its domain and explore the unvisited values
223217
int ub = vars[var].getUB();
224218
for (val = vars[var].getLB(); val <= ub; val = vars[var].nextValue(val)) {
225219
if (valuesDynamic.isPresent(val) && stop(var, val)) {return val;}
@@ -251,11 +245,11 @@ private boolean stop(int var, int val) {
251245
public void generateFailureExplanation() throws ContradictionException {
252246
Reason reason = Reason.undef();
253247
if (aCause.lcg()) {
254-
int nvars = tailBFS;
255-
int nvals = tailBFS - 1;
256-
int[] explanation = new int[1 + nvars * (2 + (maxValSearchedNodes - minValSearchedNodes + 1) - nvals)];
248+
int nVars = tailBFS;
249+
int nVals = tailBFS - 1;
250+
int[] explanation = new int[1 + nVars * (2 + (maxValSearchedNodes - minValSearchedNodes + 1) - nVals)];
257251
// Store the values between minValSearchedNodes and maxValSearchedNodes that does not belong to the searched nodes
258-
int[] nonValues = new int[(maxValSearchedNodes - minValSearchedNodes + 1) - nvals];
252+
int[] nonValues = new int[(maxValSearchedNodes - minValSearchedNodes + 1) - nVals];
259253
int m = 0;
260254
for (int value = minValSearchedNodes + 1; value < maxValSearchedNodes; value++) {
261255
if (!isInSearchedNodes(value)) { // The value does not belong to the searched nodes
@@ -315,7 +309,7 @@ private void bimodalDFS(int var) throws ContradictionException {
315309
declareInStack(matching.getMatchU(var), true);
316310
int val;
317311

318-
if(choiceBimodalDFS(var)) { // If var has a small domain then iterate over the domain
312+
if(choice(DFS, var)) { // If var has a small domain then iterate over the domain
319313
int ub = vars[var].getUB();
320314
for (val = vars[var].getLB(); val <= ub; val = vars[var].nextValue(val)) {
321315
// ======================= Case 1 : explore a non-visited value =======================
@@ -332,7 +326,7 @@ private void bimodalDFS(int var) throws ContradictionException {
332326
int pointerVar = valuesDynamic.getPrevious(vars[var].getLB()); //Optimisation: start iterating from the lower bound instead of the beginning of the list (the list is sorted in ascending order)
333327
int var_ub = vars[var].getUB(); //Optimisation
334328
while (valuesDynamic.hasNext(pointerVar) && pointerVar < var_ub) { // Explore all the branches going out of var in the DFS tree
335-
pointerVar = valuesDynamic.trackLeft(pointerVar); // Go back in the list of unvisited values
329+
pointerVar = valuesDynamic.trackPrev(pointerVar); // Go back in the list of unvisited values
336330

337331
while(valuesDynamic.hasNext(pointerVar) && pointerVar < var_ub && !vars[var].contains(valuesDynamic.getNext(pointerVar))) { // Go to the last consecutive non-domain value
338332
pointerVar = valuesDynamic.getNext(pointerVar);
@@ -377,7 +371,7 @@ private void process(int var, int val) throws ContradictionException {
377371

378372

379373
/**
380-
* In this function we prune all the arcs coming from the variables of the discovered SCC and pointing toward valyes outside the discovered SCC
374+
* In this function we prune all the arcs coming from the variables of the discovered SCC and pointing toward values outside the discovered SCC
381375
*/
382376
private void prune(int root) throws ContradictionException {
383377
complementSCC.refill();
@@ -440,7 +434,7 @@ private void prune(int root) throws ContradictionException {
440434

441435
if (vars[var].getDomainSize() > 1) { // If the domain is a singleton there is nothing to prune
442436

443-
if (choicePrune(var)) { // If var has a small domain then iterate over the domain and prune the values that are in the complement
437+
if (choice(PRUNE, var)) { // If var has a small domain then iterate over the domain and prune the values that are in the complement
444438
int ub = vars[var].getUB();
445439
for (int domainValue = vars[var].getLB(); domainValue <= ub; domainValue = vars[var].nextValue(domainValue)) {
446440
if (complementSCC.isPresent(domainValue)) {
@@ -483,8 +477,8 @@ public void generatePruningExplanation(int sourceVar, int destinationVal) throws
483477
} else {
484478
// Get the minimum and maximum values of the destination SCC
485479
for (int i = getStartPositionSCC(scc); i < getEndPositionSCC(scc); i++) {
486-
minValSCC = Math.min(minValSCC, SCCpartition[i]);
487-
maxValSCC = Math.max(maxValSCC, SCCpartition[i]);
480+
minValSCC = Math.min(minValSCC, sccPartition[i]);
481+
maxValSCC = Math.max(maxValSCC, sccPartition[i]);
488482
}
489483

490484
// Create the array of the explanation with the right size
@@ -502,7 +496,7 @@ public void generatePruningExplanation(int sourceVar, int destinationVal) throws
502496
// Start generating the explanation
503497
m = 1;
504498
for (int i = getStartPositionSCC(scc); i < getEndPositionSCC(scc); i++) {
505-
int var = matching.getMatchV(SCCpartition[i]);
499+
int var = matching.getMatchV(sccPartition[i]);
506500
explanation[m++] = MiniSat.neg(vars[var].getLit(minValSCC, LR_GE));
507501
for (int value : nonValues) {
508502
explanation[m++] = MiniSat.neg(vars[var].getLit(value, LR_NE));
@@ -597,57 +591,33 @@ private void updateDynamicStructuresEnding() {
597591
// These functions decide whether the domain is considered as small or large
598592
//***********************************************************************************
599593

600-
601-
private boolean choiceBimodalBFS(int var) {
602-
switch (mode) {
603-
case CLASSIC:
604-
return true;
605-
case COMPLEMENT:
606-
return false;
607-
case PARTIAL:
608-
// return vars[var].getDomainSize() < valuesDynamic.getSize();
609-
return Math.max((vars[var].getUB() - vars[var].getLB() + 63) >> 6, vars[var].getDomainSize()) < valuesDynamic.getSize(); // More suited to BitSet domain representation
610-
case TUNED:
611-
// return vars[var].getDomainSize() < valuesDynamic.getSize();
612-
return Math.max((vars[var].getUB() - vars[var].getLB() + 63) >> 6, vars[var].getDomainSize()) < valuesDynamic.getSize(); // More suited to BitSet domain representation
613-
default:
614-
return true;
615-
}
616-
617-
}
618-
619-
private boolean choiceBimodalDFS(int var) {
594+
private boolean choice(int algo, int var) {
620595
switch (mode) {
621596
case CLASSIC:
622597
return true;
623598
case COMPLEMENT:
624599
return false;
625600
case PARTIAL:
626-
// return vars[var].getDomainSize() < valuesDynamic.getSize();
627-
return Math.max((vars[var].getUB() - vars[var].getLB() + 63) >> 6, vars[var].getDomainSize()) < valuesDynamic.getSize(); // More suited to BitSet domain representation
628-
case TUNED:
629-
// return vars[var].getDomainSize() < Math.sqrt(valuesDynamic.getSize());
630-
return Math.max((vars[var].getUB() - vars[var].getLB() + 63) >> 6, vars[var].getDomainSize()) < Math.sqrt(valuesDynamic.getSize()); // More suited to BitSet domain representation
631-
default:
632-
return true;
633-
}
634-
}
635-
636-
private boolean choicePrune(int var) {
637-
switch (mode) {
638-
case CLASSIC:
639-
return true;
640-
case COMPLEMENT:
641-
return false;
642-
case PARTIAL:
643-
// return vars[var].getDomainSize() < complementSCC.getSize();
644-
return Math.max((vars[var].getUB() - vars[var].getLB() + 63) >> 6, vars[var].getDomainSize()) < complementSCC.getSize(); // More suited to BitSet domain representation
601+
if (algo == BFS || algo == DFS) {
602+
// return vars[var].getDomainSize() < valuesDynamic.getSize();
603+
return Math.max((vars[var].getUB() - vars[var].getLB() + 63) >> 6, vars[var].getDomainSize()) < valuesDynamic.getSize(); // More suited to BitSet domain representation
604+
} else {
605+
// return vars[var].getDomainSize() < complementSCC.getSize();
606+
return Math.max((vars[var].getUB() - vars[var].getLB() + 63) >> 6, vars[var].getDomainSize()) < complementSCC.getSize(); // More suited to BitSet domain representation
607+
}
645608
case TUNED:
646-
// return vars[var].getDomainSize() < complementSCC.getSize();
647-
return Math.max((vars[var].getUB() - vars[var].getLB() + 63) >> 6, vars[var].getDomainSize()) < complementSCC.getSize(); // More suited to BitSet domain representation
648-
default:
649-
return true;
609+
if (algo == BFS) {
610+
// return vars[var].getDomainSize() < valuesDynamic.getSize();
611+
return Math.max((vars[var].getUB() - vars[var].getLB() + 63) >> 6, vars[var].getDomainSize()) < valuesDynamic.getSize(); // More suited to BitSet domain representation
612+
} else if (algo == DFS) {
613+
// return vars[var].getDomainSize() < Math.sqrt(valuesDynamic.getSize());
614+
return Math.max((vars[var].getUB() - vars[var].getLB() + 63) >> 6, vars[var].getDomainSize()) < Math.sqrt(valuesDynamic.getSize()); // More suited to BitSet domain representation
615+
} else {
616+
// return vars[var].getDomainSize() < complementSCC.getSize();
617+
return Math.max((vars[var].getUB() - vars[var].getLB() + 63) >> 6, vars[var].getDomainSize()) < complementSCC.getSize(); // More suited to BitSet domain representation
618+
}
650619
}
620+
return true;
651621
}
652622

653623

@@ -688,11 +658,11 @@ private void declareInStack(int val, boolean present) {
688658
}
689659

690660
private int getSCC(int val) {
691-
return SCCbelonging[val - minValue];
661+
return sccBelonging[val - minValue];
692662
}
693663

694664
private void setSCC(int val, int scc) {
695-
SCCbelonging[val - minValue] = scc;
665+
sccBelonging[val - minValue] = scc;
696666
}
697667

698668
private boolean isUpToDateSCC(int val) {return upToDateSCC[val - minValue] == updateKey; }
@@ -711,13 +681,15 @@ private void resetSCCs() {
711681
private void newSCC() {
712682
numberOfSCCs++;
713683
int lastSCC = getLastSCC();
714-
if (lastSCC == 0) {SCCindices[lastSCC] = 0;}
715-
else {SCCindices[lastSCC] = SCCindices[lastSCC - 1];}
684+
if (lastSCC == 0) {
685+
sccIndices[lastSCC] = 0;}
686+
else {
687+
sccIndices[lastSCC] = sccIndices[lastSCC - 1];}
716688
}
717689

718690
private void addToSCC(int val, int scc) {
719-
SCCpartition[SCCindices[scc]] = val;
720-
SCCindices[scc]++;
691+
sccPartition[sccIndices[scc]] = val;
692+
sccIndices[scc]++;
721693
setSCC(val, scc);
722694
setUpToDateSCC(val);
723695
}
@@ -732,12 +704,12 @@ private int getStartPositionSCC(int scc) {
732704
if(scc == 0) {
733705
return 0;
734706
} else {
735-
return SCCindices[scc - 1];
707+
return sccIndices[scc - 1];
736708
}
737709
}
738710

739711
private int getEndPositionSCC(int scc) {
740-
return SCCindices[scc];
712+
return sccIndices[scc];
741713
}
742714

743715
private int getSizeScc(int scc) {return getEndPositionSCC(scc) - getStartPositionSCC(scc);}

0 commit comments

Comments
 (0)