001package org.cpsolver.ifs.extension;
002
003import java.util.ArrayList;
004import java.util.Collection;
005import java.util.Comparator;
006import java.util.HashMap;
007import java.util.List;
008import java.util.Map;
009import java.util.Set;
010import java.util.TreeSet;
011import java.util.concurrent.locks.ReentrantReadWriteLock;
012
013import org.cpsolver.ifs.assignment.Assignment;
014import org.cpsolver.ifs.heuristics.ValueSelection;
015import org.cpsolver.ifs.heuristics.VariableSelection;
016import org.cpsolver.ifs.model.Constraint;
017import org.cpsolver.ifs.model.ConstraintListener;
018import org.cpsolver.ifs.model.Model;
019import org.cpsolver.ifs.model.Value;
020import org.cpsolver.ifs.model.Variable;
021import org.cpsolver.ifs.solution.Solution;
022import org.cpsolver.ifs.solver.Solver;
023import org.cpsolver.ifs.util.DataProperties;
024
025
026/**
027 * Conflict-based statistics. <br>
028 * <br>
029 * The idea behind it is to memorize conflicts and to avoid their potential
030 * repetition. When a value v0 is assigned to a variable V0, hard conflicts with
031 * previously assigned variables (e.g., V1 = v1, V2 = v2, ... Vm = vm) may
032 * occur. These variables V1,...,Vm have to be unassigned before the value v0 is
033 * assigned to the variable V0. These unassignments, together with the reason
034 * for their unassignment (i.e., the assignment V0 = v0), and a counter tracking
035 * how many times such an event occurred in the past, is stored in memory. <br>
036 * <br>
037 * Later, if a variable is selected for assignment again, the stored information
038 * about repetition of past hard conflicts can be taken into account, e.g., in
039 * the value selection heuristics. Assume that the variable V0 is selected for
040 * an assignment again (e.g., because it became unassigned as a result of a
041 * later assignment), we can weight the number of hard conflicts created in the
042 * past for each possible value of this variable. In the above example, the
043 * existing assignment V1 = v1 can prohibit the selection of value v0 for
044 * variable V0 if there is again a conflict with the assignment V1 = v1. <br>
045 * <br>
046 * Conflict-based statistics are a data structure which memorizes the number of
047 * hard conflicts that have occurred during the search (e.g., that assignment V0
048 * = v0 resulted c1 times in an unassignment of V1 = v1, c2 times of V2 = v2, .
049 * . . and cm times of Vm = vm). More precisely, they form an array
050 * <pre><code>
051 * CBS[Va = va, Vb != vb] = cab,
052 * </code></pre>
053 * stating that the assignment Va = va caused the unassignment of Vb = vb a
054 * total of cab times in the past. Note that in case of n-ary constraints (where
055 * n &gt; 2), this does not imply that the assignments Va = va and Vb = vb cannot
056 * be used together. The proposed conflict-based statistics do not actually work
057 * with any constraint, they only memorize unassignments and the assignment that
058 * caused them. Let us consider a variable Va selected by the
059 * {@link VariableSelection#selectVariable(Solution)} function and a value va
060 * selected by {@link ValueSelection#selectValue(Solution, Variable)}. Once the
061 * assignment Vb = vb is selected by {@link Model#conflictValues(Assignment, Value)} to be
062 * unassigned, the array cell CBS[Va = va, Vb != vb] is incremented by one. <br>
063 * <br>
064 * The data structure is implemented as a hash table, storing information for
065 * conflict-based statistics. A counter is maintained for the tuple A = a and B
066 * != b. This counter is increased when the value a is assigned to the variable
067 * A and b is unassigned from B. The example of this structure
068 * <pre><code>
069 * A = a &nbsp;&nbsp;&nbsp; &#8594; &nbsp;&nbsp;&nbsp; 3 x B != b, &nbsp; 4 x B
070 * != c, &nbsp; 2 x C != a, &nbsp; 120 x D != a
071 * </code></pre>
072 * expresses that variable B lost its assignment b three times and its
073 * assignment c four times, variable C lost its assignment a two times, and D
074 * lost its assignment a 120 times, all because of later assignments of value a
075 * to variable A. This structure is being used in the value selection heuristics
076 * to evaluate existing conflicts with the assigned variables. For example, if
077 * there is a variable A selected and if the value a is in conflict with the
078 * assignment B = b, we know that a similar problem has already occurred 3x in
079 * the past, and hence the conflict A = a is weighted with the number 3. <br>
080 * <br>
081 * Then, a min-conflict value selection criterion, which selects a value with
082 * the minimal number of conflicts with the existing assignments, can be easily
083 * adapted to a weighted min-conflict criterion. The value with the smallest sum
084 * of the number of conflicts multiplied by their frequencies is selected.
085 * Stated in another way, the weighted min-conflict approach helps the value
086 * selection heuristics to select a value that might cause more conflicts than
087 * another value, but these conflicts occurred less frequently, and therefore
088 * they have a lower weighted sum. <br>
089 * <br>
090 * The conflict-based statistics has also implemented the following extensions:
091 * <ul>
092 * <li>If a variable is selected for an assignment, the above presented
093 * structure can also tell how many potential conflicts a value can cause in the
094 * future. In the above example, we already know that four times a later
095 * assignment of A=a caused that value c was unassigned from B. We can try to
096 * minimize such future conflicts by selecting a different value of the variable
097 * B while A is still unbound.
098 * <li>The memorized conflicts can be aged according to how far they have
099 * occurred in the past. For example, a conflict which occurred 1000 iterations
100 * ago can have half the weight of a conflict which occurred during the last
101 * iteration or it can be forgotten at all.
102 * </ul>
103 * Furthermore, the presented conflict-based statistics can be used not only
104 * inside the solving mechanism. The constructed "implications" together with
105 * the information about frequency of their occurrences can be easily accessed
106 * by users or by some add-on deductive engine to identify inconsistencies1
107 * and/or hard parts of the input problem. The user can then modify the input
108 * requirements in order to eliminate problems found and let the solver continue
109 * the search with this modified input problem. <br>
110 * <br>
111 * Parameters: <br>
112 * <table border='1' summary='Related Solver Parameters'>
113 * <tr>
114 * <th>Parameter</th>
115 * <th>Type</th>
116 * <th>Comment</th>
117 * </tr>
118 * <tr>
119 * <td>ConflictStatistics.Ageing</td>
120 * <td>{@link Double}</td>
121 * <td>Ageing of the conflict-based statistics. Every memorized conflict is aged
122 * (multiplited) by this factor for every iteration which passed from the time
123 * it was memorized. For instance, if there was a conflict 10 iterations ago,
124 * its value is ageing^10 (default is 1.0 -- no ageing).</td>
125 * </tr>
126 * <tr>
127 * <td>ConflictStatistics.AgeingHalfTime</td>
128 * <td>{@link Integer}</td>
129 * <td>Another way how to express ageing: number of iterations to decrease a
130 * conflict to 1/2 (default is 0 -- no ageing)</td>
131 * </tr>
132 * </table>
133 * 
134 * @see Solver
135 * @see Model
136 * @see ValueSelection
137 * @see VariableSelection
138 * 
139 * @version IFS 1.3 (Iterative Forward Search)<br>
140 *          Copyright (C) 2006 - 2014 Tomáš Müller<br>
141 *          <a href="mailto:muller@unitime.org">muller@unitime.org</a><br>
142 *          <a href="http://muller.unitime.org">http://muller.unitime.org</a><br>
143 * <br>
144 *          This library is free software; you can redistribute it and/or modify
145 *          it under the terms of the GNU Lesser General Public License as
146 *          published by the Free Software Foundation; either version 3 of the
147 *          License, or (at your option) any later version. <br>
148 * <br>
149 *          This library is distributed in the hope that it will be useful, but
150 *          WITHOUT ANY WARRANTY; without even the implied warranty of
151 *          MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
152 *          Lesser General Public License for more details. <br>
153 * <br>
154 *          You should have received a copy of the GNU Lesser General Public
155 *          License along with this library; if not see
156 *          <a href='http://www.gnu.org/licenses/'>http://www.gnu.org/licenses/</a>.
157 * @param <V> Variable
158 * @param <T> Value
159 */
160public class ConflictStatistics<V extends Variable<V, T>, T extends Value<V, T>> extends Extension<V, T> implements ConstraintListener<V, T> {
161    private static final String PARAM_AGEING = "ConflictStatistics.Ageing";
162    private static final String PARAM_HALF_AGE = "ConflictStatistics.AgeingHalfTime";
163    private static final String PARAM_PRINT = "ConflictStatistics.Print";
164
165    private double iAgeing = 1.0;
166    private boolean iPrint = false;
167
168    private Map<AssignedValue<T>, List<AssignedValue<T>>> iAssignments = new HashMap<AssignedValue<T>, List<AssignedValue<T>>>();
169    private Map<V, List<AssignedValue<T>>> iUnassignedVariables = new HashMap<V, List<AssignedValue<T>>>();
170    private Map<AssignedValue<T>, List<AssignedValue<T>>> iNoGoods = new HashMap<AssignedValue<T>, List<AssignedValue<T>>>();
171    
172    private final ReentrantReadWriteLock iLock = new ReentrantReadWriteLock();
173
174    public ConflictStatistics(Solver<V, T> solver, DataProperties properties) {
175        super(solver, properties);
176        iAgeing = properties.getPropertyDouble(PARAM_AGEING, iAgeing);
177        int halfAge = properties.getPropertyInt(PARAM_HALF_AGE, 0);
178        if (halfAge > 0)
179            iAgeing = Math.exp(Math.log(0.5) / (halfAge));
180        iPrint = properties.getPropertyBoolean(PARAM_PRINT, iPrint);
181    }
182
183    @Override
184    public void register(Model<V, T> model) {
185        super.register(model);
186    }
187
188    @Override
189    public void unregister(Model<V, T> model) {
190        super.unregister(model);
191    }
192
193    private void variableUnassigned(long iteration, T unassignedValue, AssignedValue<T> noGood) {
194        if (iteration <= 0) return;
195        iLock.writeLock().lock();
196        try {
197            AssignedValue<T> unass = new AssignedValue<T>(iteration, unassignedValue, iAgeing);
198            List<AssignedValue<T>> noGoodsForUnassignment = iNoGoods.get(unass);
199            if (noGoodsForUnassignment != null) {
200                if (noGoodsForUnassignment.contains(noGood)) {
201                    (noGoodsForUnassignment.get(noGoodsForUnassignment.indexOf(noGood))).incCounter(iteration);
202                } else {
203                    noGoodsForUnassignment.add(noGood);
204                }
205            } else {
206                noGoodsForUnassignment = new ArrayList<AssignedValue<T>>();
207                noGoodsForUnassignment.add(noGood);
208                iNoGoods.put(unass, noGoodsForUnassignment);
209            }
210        } finally {
211            iLock.writeLock().unlock();
212        }
213    }
214
215    public void reset() {
216        iLock.writeLock().lock();
217        try {
218            iUnassignedVariables.clear();
219            iAssignments.clear();
220        } finally {
221            iLock.writeLock().unlock();
222        }
223    }
224
225    public Map<AssignedValue<T>, List<AssignedValue<T>>> getNoGoods() {
226        return iNoGoods;
227    }
228
229    public void variableUnassigned(long iteration, T unassignedValue, T assignedValue) {
230        if (iteration <= 0) return;
231        AssignedValue<T> ass = new AssignedValue<T>(iteration, assignedValue, iAgeing);
232        AssignedValue<T> unass = new AssignedValue<T>(iteration, unassignedValue, iAgeing);
233        iLock.writeLock().lock();
234        try {
235            if (iAssignments.containsKey(unass)) {
236                List<AssignedValue<T>> asss = iAssignments.get(unass);
237                if (asss.contains(ass)) {
238                    asss.get(asss.indexOf(ass)).incCounter(iteration);
239                } else {
240                    asss.add(ass);
241                }
242            } else {
243                List<AssignedValue<T>> asss = new ArrayList<AssignedValue<T>>();
244                asss.add(ass);
245                iAssignments.put(unass, asss);
246            }
247            if (iUnassignedVariables.containsKey(unassignedValue.variable())) {
248                List<AssignedValue<T>> asss = iUnassignedVariables.get(unassignedValue.variable());
249                if (asss.contains(ass)) {
250                    (asss.get(asss.indexOf(ass))).incCounter(iteration);
251                } else {
252                    asss.add(ass);
253                }
254            } else {
255                List<AssignedValue<T>> asss = new ArrayList<AssignedValue<T>>();
256                asss.add(ass);
257                iUnassignedVariables.put(unassignedValue.variable(), asss);
258            }
259        } finally {
260            iLock.writeLock().unlock();
261        }
262    }
263
264    /**
265     * Counts number of unassignments of the given conflicting values caused by
266     * the assignment of the given value.
267     * @param iteration current iteration
268     * @param conflictValues values conflicting with the given value
269     * @param value given value
270     * @return number of unassignments
271     */
272    public double countRemovals(long iteration, Collection<T> conflictValues, T value) {
273        long ret = 0;
274        for (T conflictValue : conflictValues) {
275            ret += countRemovals(iteration, conflictValue, value);
276            // tady bylo +1
277        }
278        return ret;
279    }
280
281    /**
282     * Counts number of unassignments of the given conflicting value caused by
283     * the assignment of the given value.
284     * @param iteration current iteration
285     * @param conflictValue value conflicting with the given value
286     * @param value given value
287     * @return number of unassignments
288     */
289    public double countRemovals(long iteration, T conflictValue, T value) {
290        iLock.readLock().lock();
291        try {
292            List<AssignedValue<T>> asss = iUnassignedVariables.get(conflictValue.variable());
293            if (asss == null)
294                return 0;
295            AssignedValue<T> ass = new AssignedValue<T>(iteration, value, iAgeing);
296            int idx = asss.indexOf(ass);
297            if (idx < 0)
298                return 0;
299            return (asss.get(idx)).getCounter(iteration);
300        } finally {
301            iLock.readLock().unlock();
302        }
303    }
304
305    /**
306     * Counts potential number of unassignments of if the given value is
307     * selected.
308     * @param assignment current assignment
309     * @param iteration current iteration
310     * @param value given value
311     * @param limit conflict limit
312     * @return number of potential unassignments
313     */
314    public long countPotentialConflicts(Assignment<V, T> assignment, long iteration, T value, int limit) {
315        iLock.readLock().lock();
316        try {
317            List<AssignedValue<T>> asss = iAssignments.get(new AssignedValue<T>(iteration, value, iAgeing));
318            if (asss == null)
319                return 0;
320            long count = 0;
321            for (AssignedValue<T> ass : asss) {
322                if (ass.getValue().variable().getAssignment(assignment) == null) {
323                    if (limit >= 0) {
324                        count += ass.getCounter(iteration) * Math.max(0, 1 + limit - value.variable().getModel().conflictValues(assignment, ass.getValue()).size());
325                    } else {
326                        count += ass.getCounter(iteration);
327                    }
328                }
329            }
330            return count;            
331        } finally {
332            iLock.readLock().unlock();
333        }
334    }
335    
336    private int countAssignments(V variable) {
337        iLock.readLock().lock();
338        try {
339            List<AssignedValue<T>> assignments = iUnassignedVariables.get(variable);
340            if (assignments == null || assignments.isEmpty()) return 0;
341            int ret = 0;
342            for (AssignedValue<T> assignment: assignments) {
343                ret += assignment.getCounter(0);
344            }
345            return ret;
346        } finally {
347            iLock.readLock().unlock();
348        }
349    }
350
351    @Override
352    public String toString() {
353        iLock.readLock().lock();
354        try {
355            if (iPrint) {
356                StringBuffer sb = new StringBuffer("Statistics{");
357                TreeSet<AssignedValue<T>> sortedUnassignments = new TreeSet<AssignedValue<T>>(new Comparator<AssignedValue<T>>() {
358                    @Override
359                    public int compare(AssignedValue<T> x1, AssignedValue<T> x2) {
360                        int c1 = 0, c2 = 0;
361                        for (AssignedValue<T> y: iNoGoods.get(x1))
362                            c1 += y.getCounter(0);
363                        for (AssignedValue<T> y: iNoGoods.get(x2))
364                            c2 += y.getCounter(0);
365                        int cmp = Double.compare(c1, c2);
366                        if (cmp != 0)
367                            return -cmp;
368                        return x1.compareTo(0, x2);
369                    }
370                });
371                sortedUnassignments.addAll(iNoGoods.keySet());
372                int printedUnassignments = 0;
373                for (AssignedValue<T> x : sortedUnassignments) {
374                    int c = 0;
375                    for (AssignedValue<T> y: iNoGoods.get(x))
376                        c += y.getCounter(0);
377                    sb.append("\n    ").append(c + "x ").append(x.toString(0, false)).append(" <= {");
378                    TreeSet<AssignedValue<T>> sortedAssignments = new TreeSet<AssignedValue<T>>(new Comparator<AssignedValue<T>>() {
379                        @Override
380                        public int compare(AssignedValue<T> x1, AssignedValue<T> x2) {
381                            int cmp = Double.compare(x1.getCounter(0), x2.getCounter(0));
382                            if (cmp != 0)
383                                return -cmp;
384                            return x1.compareTo(0, x2);
385                        }
386                    });
387                    sortedAssignments.addAll(iNoGoods.get(x));
388                    int printedAssignments = 0;
389                    for (AssignedValue<T> y : sortedAssignments) {
390                        sb.append("\n        ").append(y.toString(0, true));
391                        if (++printedAssignments == 20) {
392                            sb.append("\n        ...");
393                            break;
394                        }
395                    }
396                    sb.append("\n      }");
397                    if (++printedUnassignments == 100) {
398                        sb.append("\n     ...");
399                        break;
400                    }
401                }
402                sb.append("\n    }");
403                return sb.toString();            
404            } else {
405                StringBuffer sb = new StringBuffer("Statistics{");
406                TreeSet<V> sortedUnassignedVariables = new TreeSet<V>(new Comparator<V>() {
407                    @Override
408                    public int compare(V v1, V v2) {
409                        int cmp = Double.compare(countAssignments(v1), countAssignments(v2));
410                        if (cmp != 0)
411                            return -cmp;
412                        return v1.compareTo(v2);
413                    }
414                });
415                sortedUnassignedVariables.addAll(iUnassignedVariables.keySet());
416                int printedVariables = 0;
417                for (V variable : sortedUnassignedVariables) {
418                    sb.append("\n      ").append(countAssignments(variable) + "x ").append(variable.getName()).append(" <= {");
419                    TreeSet<AssignedValue<T>> sortedAssignments = new TreeSet<AssignedValue<T>>(new Comparator<AssignedValue<T>>() {
420                        @Override
421                        public int compare(AssignedValue<T> x1, AssignedValue<T> x2) {
422                            int cmp = Double.compare(x1.getCounter(0), x2.getCounter(0));
423                            if (cmp != 0)
424                                return -cmp;
425                            return x1.compareTo(0, x2);
426                        }
427                    });
428                    sortedAssignments.addAll(iUnassignedVariables.get(variable));
429                    int printedAssignments = 0;
430                    for (AssignedValue<T> x : sortedAssignments) {
431                        sb.append("\n        ").append(x.toString(0, true));
432                        if (++printedAssignments == 20) {
433                            sb.append("\n        ...");
434                            break;
435                        }
436                    }
437                    sb.append("\n      }");
438                    if (++printedVariables == 100) {
439                        sb.append("\n      ...");
440                        break;
441                    }
442                }
443                sb.append("\n    }");
444                return sb.toString();            
445            }
446        } finally {
447            iLock.readLock().unlock();
448        }
449    }
450
451    @Override
452    public void constraintBeforeAssigned(Assignment<V, T> assignment, long iteration, Constraint<V, T> constraint, T assigned, Set<T> unassigned) {
453    }
454
455    /** Increments appropriate counters when there is a value unassigned */
456    @Override
457    public void constraintAfterAssigned(Assignment<V, T> assignment, long iteration, Constraint<V, T> constraint, T assigned, Set<T> unassigned) {
458        if (iteration <= 0)
459            return;
460        if (unassigned == null || unassigned.isEmpty())
461            return;
462        if (iPrint) {
463            // AssignmentSet noGoods =
464            // AssignmentSet.createAssignmentSet(iteration,unassigned, iAgeing);
465            // noGoods.addAssignment(iteration, assigned, iAgeing);
466            // noGoods.setConstraint(constraint);
467            AssignedValue<T> noGood = new AssignedValue<T>(iteration, assigned, iAgeing);
468            noGood.setConstraint(constraint);
469            for (T unassignedValue : unassigned) {
470                variableUnassigned(iteration, unassignedValue, noGood);
471                variableUnassigned(iteration, unassignedValue, assigned);
472            }
473        } else {
474            for (T unassignedValue : unassigned) {
475                variableUnassigned(iteration, unassignedValue, assigned);
476            }
477        }
478    }
479
480    @Override
481    public void constraintAdded(Constraint<V, T> constraint) {
482        constraint.addConstraintListener(this);
483    }
484
485    @Override
486    public void constraintRemoved(Constraint<V, T> constraint) {
487        constraint.removeConstraintListener(this);
488    }
489}