    001    package ifs.extension;
    002
    003    import ifs.model.*;
    004    import ifs.solution.*;
    005    import ifs.solver.*;
    006    import ifs.util.*;
    007    import ifs.heuristics.*;
    008
    009    import java.io.*;
    010    import java.util.*;
    011
    012    /**
    013     * Conflict-based statistics.
    014     * <br><br>
    015     * The idea behind it is to memorize conflicts and to avoid their potential repetition. When a value v0 is assigned to a
    016     * variable V0, hard conflicts with previously assigned variables (e.g., V1 = v1, V2 = v2, ... Vm = vm) may occur.
    017     * These variables V1,...,Vm have to be unassigned before the value v0 is assigned to the variable V0. These unassignments,
    018     * together with the reason for their unassignment (i.e., the assignment V0 = v0), and a counter tracking how many times
    019     * such an event occurred in the past, is stored in memory.
    020     * <br><br>
    021     * Later, if a variable is selected for assignment again, the stored information about repetition of past hard conflicts
    022     * can be taken into account, e.g., in the value selection heuristics. Assume that the variable V0 is selected for an
    023     * assignment again (e.g., because it became unassigned as a result of a later assignment), we can weight the number of
    024     * hard conflicts created in the past for each possible value of this variable. In the above example, the existing
    025     * assignment V1 = v1 can prohibit the selection of value v0 for variable V0 if there is again a conflict with the
    026     * assignment V1 = v1.
    027     * <br><br>
    028     * Conflict-based statistics are a data structure which memorizes the number of hard conflicts that have occurred
    029     * during the search (e.g., that assignment V0 = v0 resulted c1 times in an unassignment of V1 = v1, c2 times of
    030     * V2 = v2, . . . and cm times of Vm = vm). More precisely, they form an array
    031     * <ul>
    032     * CBS[Va = va, Vb != vb] = cab,
    033     * </ul>
    034     * stating that the assignment Va = va caused the unassignment of Vb = vb a total of cab times in the past. Note that
    035     * in case of n-ary constraints (where n > 2), this does not imply that the assignments Va = va and Vb = vb cannot be used
    036     * together. The proposed conflict-based statistics do not actually work with any constraint, they only memorize
    037     * unassignments and the assignment that caused them. Let us consider a variable Va selected by the
    038     * {@link VariableSelection#selectVariable(Solution)} function and a value va selected by
    039     * {@link ValueSelection#selectValue(Solution, Variable)}. Once the assignment Vb = vb is selected by
    040     * {@link Model#conflictValues(Value)} to be unassigned, the array cell CBS[Va = va, Vb != vb] is incremented by one.
    041     * <br><br>
    042     * The data structure is implemented as a hash table, storing information for conflict-based statistics. A counter is
    043     * maintained for the tuple A = a and B != b. This counter is increased when the value a is assigned to the variable A
    044     * and b is unassigned from B. The example of this structure
    045     * <ul>
    046     * A = a &nbsp;&nbsp;&nbsp; &#8594; &nbsp;&nbsp;&nbsp; 3 x B != b, &nbsp; 4 x B != c, &nbsp; 2 x C != a, &nbsp; 120 x D != a
    047     * </ul>
    048     * expresses that variable B lost its assignment b three times and its assignment c four times, variable C lost its
    049     * assignment a two times, and D lost its assignment a 120 times, all because of later assignments of value a to
    050     * variable A. This structure is being used in the value selection heuristics to evaluate existing conflicts with
    051     * the assigned variables. For example, if there is a variable A selected and if the value a is in conflict with the
    052     * assignment B = b, we know that a similar problem has already occurred 3x in the past, and hence the conflict A = a is
    053     * weighted with the number 3.
    054     * <br><br>
    055     * Then, a min-conflict value selection criterion, which selects a value with the minimal number of conflicts with the
    056     * existing assignments, can be easily adapted to a weighted min-conflict criterion. The value with the smallest sum of the
    057     * number of conflicts multiplied by their frequencies is selected. Stated in another way, the weighted min-conflict
    058     * approach helps the value selection heuristics to select a value that might cause more conflicts than another
    059     * value, but these conflicts occurred less frequently, and therefore they have a lower weighted sum.
    060     * <br><br>
    061     * The conflict-based statistics has also implemented the following extensions: <ul>
    062     * <li> If a variable is selected for an assignment, the above presented structure can also tell how many potential
    063     * conflicts a value can cause in the future. In the above example, we already know that four times a later assignment
    064     * of A=a caused that value c was unassigned from B. We can try to minimize such future conflicts by selecting
    065     * a different value of the variable B while A is still unbound.
    066     * <li> The memorized conflicts can be aged according to how far they have occurred in the past. For example, a conflict
    067     * which occurred 1000 iterations ago can have half the weight of a conflict which occurred during the last iteration
    068     * or it can be forgotten at all.
    069     * </ul>
    070     * Furthermore, the presented conflict-based statistics can be used not only inside the solving mechanism. The
    071     * constructed "implications" together with the information about frequency of their occurrences can be easily accessed
    072     * by users or by some add-on deductive engine to identify inconsistencies1 and/or hard parts of the input problem.
    073     * The user can then modify the input requirements in order to eliminate problems found and let the solver continue the
    074     * search with this modified input problem.
    075     * <br><br>
    076     * Parameters:
    077     * <br>
    078     * <table border='1'><tr><th>Parameter</th><th>Type</th><th>Comment</th></tr>
    079     * <tr><td>ConflictStatistics.Ageing</td><td>{@link Double}</td><td>Ageing of the conflict-based statistics. Every memorized conflict is aged (multiplited) by this factor for every iteration which passed from the time it was memorized. For instance, if there was a conflict 10 iterations ago, its value is ageing^10 (default is 1.0 -- no ageing).</td></tr>
    080     * <tr><td>ConflictStatistics.AgeingHalfTime</td><td>{@link Integer}</td><td>Another way how to express ageing: number of iterations to decrease a conflict to 1/2 (default is 0 -- no ageing)</td></tr>
    081     * </table>
    082     * <br>
    083     * Conflict-based statistics also allows printing to HTML files during the search, after each given number of iterations.
    084     * Example of such file:<br>
    085     * <iframe src="cbs-ex.html" width="98%" height="300" scrolling="auto" frameborder="1">
    086     * [Your user agent does not support frames or is currently configured  not to display frames. However, you may visit <A href="cbs-ex.html">the related document.</A>]
    087     * </iframe>
    088     * <br><br>
    089     * Conflict-based statistics allows two modes of printing: <ul>
    090     * <li>variable based: tree selected variable &#8594; selected value &#8594; constraint &#8594; conflicting assignment is printed
    091     * <li>constraint based: tree constraint &#8594; selected variable &#8594; selected value &#8594; conflicting assignment is printed
    092     * </ul>
    093     * Where constraint is the constraint involved in the unassignment of the conflicting assignmend when selected value is assigned to the selected variable.
    094     * HTML files are written in the output directory, named stat1.html, stat2.html, ...
    095     * <br><br>
    096     * Printing parameters:
    097     * <table border='1'><tr><th>Parameter</th><th>Type</th><th>Comment</th></tr>
    098     * <tr><td>ConflictStatistics.Print</td><td>{@link Boolean}</td><td>If true, conflict-based statistics is being printed to an HTML file during the search.</td></tr>
    099     * <tr><td>ConflictStatistics.PrintInterval</td><td>{@link Integer}</td><td>Interval (expressed in the number of iterations) for printing CBS</td></tr>
    100     * <tr><td>ConflictStatistics.Type</td><td>{@link Integer}</td><td>0 for variable based, 1 from constraint based</td></tr>
    101     * <tr><td>ConflictStatistics.MaxLines</td><td>{@link Integer}</td><td>Maximal number of lines in the first level of CBS</td></tr>
    102     * <tr><td>ConflictStatistics.MaxBranchingLev1</td><td>{@link Integer}</td><td>Maximal number of lines in the second level of CBS</td></tr>
    103     * <tr><td>ConflictStatistics.MaxBranchingLev2</td><td>{@link Integer}</td><td>Maximal number of lines in the third level of CBS</td></tr>
    104     * <tr><td>ConflictStatistics.ImageBase</td><td>{@link String}</td><td>Directory with images collapse.gif, expand.gif and end.gif relative to output directory</td></tr>
    105     * </table>
    106     *
    107     * @see Solver
    108     * @see Model
    109     * @see ValueSelection
    110     * @see VariableSelection
    111     *
    112     * @author <a href="mailto:muller@ktiml.mff.cuni.cz">Tomáš Müller</a>
    113     * @version 1.0
    114     */
    115    public class ConflictStatistics extends Extension implements ConstraintListener, SolutionListener {
    116        private static org.apache.log4j.Logger sLogger = org.apache.log4j.Logger.getLogger(ConflictStatistics.class);
    117        private static final String PARAM_AGEING = "ConflictStatistics.Ageing";
    118        private static final String PARAM_HALF_AGE = "ConflictStatistics.AgeingHalfTime";
    119        private static final String PARAM_PRINT = "ConflictStatistics.Print";
    120        private static final String PARAM_PRINTINTERVAL = "ConflictStatistics.PrintInterval";
    121
    122        private static final int TYPE_VARIABLE_BASED = 0;
    123        private static final int TYPE_CONSTRAINT_BASED = 1;
    124
    125        private double iAgeing = 1.0;
    126        private long iPrintInterval = -1;
    127        private boolean iPrint = false;
    128        private int iPrintCounter = 0;
    129
    130        private Hashtable iAssignments = new Hashtable();
    131        private Hashtable iUnassignedVariables = new Hashtable();
    132        private Hashtable iNoGoods = new Hashtable();
    133
    134        public ConflictStatistics(Solver solver, DataProperties properties) {
    135            super(solver, properties);
    136            iAgeing = properties.getPropertyDouble(PARAM_AGEING, iAgeing);
    137            int halfAge = properties.getPropertyInt(PARAM_HALF_AGE, 0);
    138            if (halfAge > 0) iAgeing = Math.exp(Math.log(0.5) / ((double)halfAge));
    139            iPrint = properties.getPropertyBoolean(PARAM_PRINT, iPrint);
    140            iPrintInterval = properties.getPropertyLong(PARAM_PRINTINTERVAL, iPrintInterval);
    141        }
    142
    143        public void register(Model model) {
    144            super.register(model);
    145            if (iPrint) {
    146                getSolver().currentSolution().addSolutionListener(this);
    147            }
    148        }
    149
    150        public void unregister(Model model) {
    151            super.unregister(model);
    152            if (iPrint) {
    153                getSolver().currentSolution().removeSolutionListener(this);
    154            }
    155        }
    156
    157        private void variableUnassigned( long iteration, Value unassignedValue, AssignmentSet noGoods) {
    158            Assignment unass = new Assignment(iteration, unassignedValue, iAgeing);
    159            Vector noGoodsForUnassignment = (Vector)iNoGoods.get(unass);
    160            if (noGoodsForUnassignment != null) {
    161                if (noGoodsForUnassignment.contains(noGoods)) {
    162                    ((AssignmentSet)noGoodsForUnassignment.elementAt(noGoodsForUnassignment.indexOf(noGoods))).incCounter();
    163                } else {
    164                    noGoodsForUnassignment.addElement(noGoods);
    165                }
    166            } else {
    167                noGoodsForUnassignment = new FastVector();
    168                noGoodsForUnassignment.addElement(noGoods);
    169                iNoGoods.put(unass, noGoodsForUnassignment);
    170            }
    171        }
    172
    173        private void variableUnassigned(long iteration, Value unassignedValue, Value assignedValue) {
    174            Assignment ass = new Assignment(iteration, assignedValue, iAgeing);
    175            Assignment unass = new Assignment(iteration, unassignedValue, iAgeing);
    176            if (iAssignments.containsKey(unass)) {
    177                Vector asss = (Vector)iAssignments.get(unass);
    178                if (asss.contains(ass)) {
    179                    ((Assignment)asss.elementAt(asss.indexOf(ass))).incCounter(iteration);
    180                } else {
    181                    asss.addElement(ass);
    182                }
    183            } else {
    184                Vector asss = new FastVector();
    185                asss.addElement(ass);
    186                iAssignments.put(unass, asss);
    187            }
    188            if (iUnassignedVariables.containsKey(unassignedValue.variable())) {
    189                Vector asss = (Vector)iUnassignedVariables.get(unassignedValue.variable());
    190                if (asss.contains(ass)) {
    191                    ((Assignment)asss.elementAt(asss.indexOf(ass))).incCounter( iteration);
    192                } else {
    193                    asss.addElement(ass);
    194                }
    195            }
    196            else {
    197                Vector asss = new FastVector();
    198                asss.addElement(ass);
    199                iUnassignedVariables.put(unassignedValue.variable(), asss);
    200            }
    201        }
    202
    203        /** Counts number of unassignments of the given conflicting values caused by the assignment
    204         * of the given value.
    205         */
    206        public double countRemovals(long iteration, Collection conflictValues, Value value) {
    207            long ret = 0;
    208            for (Iterator i = conflictValues.iterator(); i.hasNext();) {
    209                Value conflictValue = (Value)i.next();
    210                ret += countRemovals(iteration, conflictValue, value);
    211                // tady bylo +1
    212            }
    213            return ret;
    214        }
    215
    216        /** Counts number of unassignments of the given conflicting value caused by the assignment
    217         * of the given value.
    218         */
    219        public double countRemovals(long iteration, Value conflictValue, Value value) {
    220            Vector asss = (Vector)iUnassignedVariables.get(conflictValue.variable());
    221            if (asss == null)
    222                return 0;
    223            Assignment ass = new Assignment(iteration, value, iAgeing);
    224            int idx = asss.indexOf(ass);
    225            if (idx < 0)
    226                return 0;
    227            return ((Assignment)asss.elementAt(idx)).getCounter(iteration);
    228        }
    229
    230        /** Counts potential number of unassignments of if the given value is selected.
    231         */
    232        public long countPotentialConflicts(long iteration, Value value, int limit) {
    233            Vector asss = (Vector)iAssignments.get(new Assignment(iteration, value, iAgeing));
    234            if (asss == null) return 0;
    235            long count = 0;
    236            for (Enumeration i = asss.elements(); i.hasMoreElements();) {
    237                Assignment ass = (Assignment)i.nextElement();
    238                if (ass.getValue().variable().getAssignment() == null) {
    239                    if (limit >= 0) {
    240                        count += ass.getCounter(iteration) * Math.max(0,1+limit - value.variable().getModel().conflictValues(ass.getValue()).size());
    241                    }
    242                    else {
    243                        count += ass.getCounter(iteration);
    244                    }
    245                }
    246            }
    247            return count;
    248        }
    249
    250        private void menu_item(PrintWriter out, String imgBase, String id, String name, String title, String page, boolean isCollapsed) {
    251            out.println("<div style=\"margin-left:5px;\">");
    252            out.println("<A style=\"border:0;background:0\" id=\"__idMenu"+id+"\" href=\"javascript:toggle('"+id+"')\" name=\""+name+"\" title=\"Expand "+name+"\">");
    253            out.println("<img id=\"__idMenuImg"+id+"\" border=\"0\" src=\""+(imgBase == null ? "img/" : imgBase)+(isCollapsed ? "expand" : "collapse")+".gif\" align=\"absmiddle\"></A>");
    254            out.println("&nbsp;<A target=\"__idContentFrame\" "+(page == null ? "" : "href=\""+page+"\" ")+"title=\""+(title == null ? "" : title)+"\" >"+ name+(title == null?"":" <font color='gray'>[" + title + "]</font>")+"</A><br>");
    255            out.println("</div>");
    256            out.println("<div ID=\"__idMenuDiv"+id+"\" style=\"display:"+(isCollapsed ? "none" : "block")+";position:relative;margin-left:18px;\">");
    257        }
    258
    259        private void leaf_item(PrintWriter out, String imgBase, String name, String title,String page) {
    260            out.println("<div style=\"margin-left:5px;\">");
    261            out.println("<img border=\"0\" src=\""+(imgBase == null ? "img/" : imgBase)+"end.gif\" align=\"absmiddle\">");
    262            out.println("&nbsp;<A target=\"__idContentFrame\" "+(page == null ? "" : "href=\"" + page + "\" ")+"title=\""+(title == null ? "" : title)+"\" >"+name+(title == null ? "" : " <font color='gray'>[" + title + "]</font>")+"</A><br>");
    263            out.println("</div>");
    264        }
    265
    266        private void end_item(PrintWriter out) {
    267            out.println("</div>");
    268        }
    269
    270        private void unassignedVariableMenuItem(PrintWriter out, String imgBase, String menuId, long counter, Variable variable) {
    271            menu_item(out, imgBase, menuId, counter + "x " + variable.getName(), variable.getDescription(), null, true);
    272        }
    273
    274        private void unassignmentMenuItem(PrintWriter out, String imgBase, String menuId, double counter, Assignment unassignment) {
    275            menu_item(out, imgBase, menuId, Math.round(counter) + "x " + unassignment.getValue().getName(), unassignment.getValue().getDescription(), null, true);
    276        }
    277
    278        private void constraintMenuItem(PrintWriter out, String imgBase, String menuId, long counter, Constraint constraint) {
    279            String name = (constraint == null ? null : constraint.getClass().getName().substring( constraint.getClass().getName().lastIndexOf('.') + 1) + (constraint.getName() == null ? "" : " " + constraint.getName()));
    280            menu_item(out, imgBase, menuId, counter + "x " + name, (constraint == null ? null : constraint.getDescription()), null, true);
    281        }
    282
    283        private void assignmentsMenuItem(PrintWriter out, String imgBase, String menuId, AssignmentSet set) {
    284            StringBuffer names = new StringBuffer();
    285            for (Enumeration e = set.getSet().elements(); e.hasMoreElements();) {
    286                Assignment a = (Assignment)e.nextElement();
    287                names.append(names.length() == 0 ? "" : ", ").append(a.getValue().variable().getName());
    288            }
    289            menu_item(out, imgBase, menuId, set.getCounter() + "x [" + names + "]", null, null, true);
    290        }
    291
    292        private void assignmentLeafItem(PrintWriter out, String imgBase, Assignment assignment) {
    293            leaf_item(out, imgBase, assignment.getValue().variable().getName()+" := "+assignment.getValue().getName(), null, null);
    294        }
    295
    296        private void assignmentLeafItem(PrintWriter out, String imgBase, long counter,Assignment assignment) {
    297            leaf_item(out, imgBase, counter+"x "+assignment.getValue().variable().getName()+" := "+assignment.getValue().getName(), null, null);
    298        }
    299
    300        /** Print conflict-based statistics in HTML format */
    301        public void printHtml(long iteration, PrintWriter out, long maxVariables, long unassignmentLimit, long assignmentLimit, int type) {
    302            printHtml(iteration, out, true, maxVariables, unassignmentLimit, assignmentLimit, null, type);
    303        }
    304
    305        /** Print conflict-based statistics in HTML format */
    306        public void printHtml(long iteration, PrintWriter out, DataProperties params) {
    307            printHtml(iteration,out,
    308            params.getPropertyBoolean("ConflictStatistics.PringHeader", false),
    309            params.getPropertyInt("ConflictStatistics.MaxLines", 25),
    310            params.getPropertyInt("ConflictStatistics.MaxBranchingLev1", 100),
    311            params.getPropertyInt("ConflictStatistics.MaxBranchingLev2", 10),
    312            params.getProperty("ConflictStatistics.ImageBase", null),
    313            params.getPropertyInt("ConflictStatistics.Type",TYPE_VARIABLE_BASED));
    314        }
    315
    316        /** Print conflict-based statistics in HTML format */
    317        public void printHtml(long iteration, PrintWriter out, boolean printHeader, long maxVariables, long unassignmentLimit, long assignmentLimit, String imgBase, int type) {
    318            if (printHeader) {
    319                out.println("<html><head>");
    320                out.println("<meta http-equiv=\"Content-Type\" content=\"text/html; charset=UTF-8\" />");
    321                out.println();
    322                out.println("<style type=\"text/css\">");
    323                out.println("<!--");
    324                out.println("A:link     { color: blue; text-decoration: none; border:0; background:0; }");
    325                out.println("A:visited  { color: blue; text-decoration: none; border:0; background:0; }");
    326                out.println("A:active   { color: blue; text-decoration: none; border:0; background:0; }");
    327                out.println("A:hover    { color: blue; text-decoration: none; border:0; background:0; }");
    328                out.println(".TextBody  { background-color: white; color:black; font-size: 12px; }");
    329                out.println(".WelcomeHead { color: black; margin-top: 0px; margin-left: 0px; font-weight: bold; text-align: right; font-size: 30px; font-family: Comic Sans MS}");
    330                out.println("-->");
    331                out.println("</style>");
    332                out.println();
    333                out.println("<script language=\"javascript\" type=\"text/javascript\">");
    334                out.println("function toggle(item) {");
    335                out.println("       obj=document.getElementById(\"__idMenuDiv\"+item);");
    336                out.println("       visible=(obj.style.display!=\"none\");");
    337                out.println("       img=document.getElementById(\"__idMenuImg\" + item);");
    338                out.println("       menu=document.getElementById(\"__idMenu\" + item);");
    339                out.println("       if (visible) {obj.style.display=\"none\";img.src=\""+(imgBase == null ? "img/" : imgBase)+"expand.gif\";menu.title='Expand '+menu.name;}");
    340                out.println("       else {obj.style.display=\"block\";img.src=\""+(imgBase == null ? "img/" : imgBase)+"collapse.gif\";menu.title='Collapse '+menu.name;}");
    341                out.println("}");
    342                out.println("</script>");
    343                out.println();
    344                out.println("</head>");
    345                out.println("<body class=\"TextBody\">");
    346                out.println("<br><table border='0' width='100%'>");
    347                out.println("<tr><td width=12>&nbsp;</td><td bgcolor='#BBCDE4' align='right'>");
    348                out.println("<div class=WelcomeHead>Conflict Statistics&nbsp;</div></td></tr></table><br>");
    349                out.println("<ul>");
    350            }
    351            if (type == TYPE_VARIABLE_BASED) {
    352                Hashtable variables = new Hashtable();
    353                Hashtable variable2Assignments = new Hashtable();
    354                for (Enumeration e1 = iNoGoods.keys(); e1.hasMoreElements();) {
    355                    Assignment ass = (Assignment)e1.nextElement();
    356                    long cnt = 0;
    357                    for (Enumeration e2 = ((Vector)iNoGoods.get(ass)).elements();e2.hasMoreElements();)
    358                        cnt += ((AssignmentSet)e2.nextElement()).getCounter();
    359                    ass.setCounter(cnt);
    360                    cnt += (variables.containsKey(ass.getValue().variable())?((Long)variables.get(ass.getValue().variable())).longValue():0L);
    361                    variables.put(ass.getValue().variable(), new Long(cnt));
    362                    Vector assignments = (Vector)variable2Assignments.get(ass.getValue().variable());
    363                    if (assignments == null) {
    364                        assignments = new FastVector();
    365                        variable2Assignments.put(ass.getValue().variable(),assignments);
    366                    }
    367                    assignments.addElement(ass);
    368                }
    369                int varCounter = 0;
    370                for (Enumeration e1 = ToolBox.sortEnumeration(variables.keys(),new VariableComparator(variables));e1.hasMoreElements();) {
    371                    Variable variable = (Variable)e1.nextElement();
    372                    varCounter++;
    373                    if (varCounter > maxVariables)
    374                        break;
    375                    long varCnt = ((Long)variables.get(variable)).longValue();
    376                    unassignedVariableMenuItem(out,imgBase,String.valueOf(variable.getId()),varCnt,variable);
    377                    for (Enumeration e2 = ToolBox.sortEnumeration(((Vector)variable2Assignments.get(variable)).elements(),Assignment.getComparator(iteration));e2.hasMoreElements();) {
    378                        Assignment ass = (Assignment)e2.nextElement();
    379                        if (!ass.getValue().variable().equals(variable))
    380                            continue;
    381                        double cntUnas = 0.0;
    382                        for (Enumeration e3 = ((Vector)iNoGoods.get(ass)).elements();e3.hasMoreElements();)
    383                            cntUnas += ((AssignmentSet)e3.nextElement()).getCounter();
    384                        if (Math.round(cntUnas) < unassignmentLimit) continue;
    385                        unassignmentMenuItem(out,imgBase,ass.getValue().variable().getId()+"."+ass.getValue().getId(),cntUnas,ass);
    386                        int id = 0;
    387                        Hashtable constr2counter = new Hashtable();
    388                        Hashtable constr2assignments = new Hashtable();
    389                        for (Enumeration e3 = ((Vector)iNoGoods.get(ass)).elements();e3.hasMoreElements();) {
    390                            AssignmentSet x = (AssignmentSet)e3.nextElement();
    391                            if (x.getConstraint() == null) continue;
    392                            Long cnter = (Long)constr2counter.get(x.getConstraint());
    393                            if (cnter == null)
    394                                constr2counter.put(x.getConstraint(), new Long(x.getCounter()));
    395                            else
    396                                constr2counter.put(x.getConstraint(), new Long(x.getCounter() + cnter.longValue()));
    397                            Vector aaa = (Vector)constr2assignments.get(x.getConstraint());
    398                            if (aaa == null) {
    399                                aaa = new FastVector();
    400                                constr2assignments.put(x.getConstraint(), aaa);
    401                            }
    402                            aaa.addElement(x);
    403                        }
    404                        for (Enumeration e3 = ToolBox.sortEnumeration(constr2counter.keys(),new ConstraintComparator(constr2counter));e3.hasMoreElements();) {
    405                            Constraint constraint = (Constraint)e3.nextElement();
    406                            Long cnter = (Long)constr2counter.get(constraint);
    407                            constraintMenuItem(out,imgBase,ass.getValue().variable().getId()+"."+ass.getValue().getId()+"."+constraint.getId(),cnter.longValue(),constraint);
    408                            if (cnter.longValue() >= assignmentLimit) {
    409                                for (Enumeration e4 = ((Vector)constr2assignments.get(constraint)).elements();e4.hasMoreElements();) {
    410                                    AssignmentSet x = (AssignmentSet)e4.nextElement();
    411                                    boolean printAssignmentsMenuItem = (x.getSet().size() > 2);
    412                                    if (printAssignmentsMenuItem)
    413                                        assignmentsMenuItem(out,imgBase,ass.getValue().variable().getId()+"."+ass.getValue().getId()+"."+constraint.getId()+"."+(++id),x);
    414                                    //menu_item(out, imgBase, ass.getValue().variable().getId()+"."+ass.getValue().getId()+"."+(++id), x.getCounter()+"x "+(x.getName()==null?null:x.getName()), x.getDescription(), null, true);
    415                                    for (Enumeration e5 = ToolBox.sortEnumeration(x.getSet().elements(),Assignment.getComparator(iteration));e5.hasMoreElements();) {
    416                                        Assignment a = (Assignment)e5.nextElement();
    417                                        if (!ass.equals(a)) {
    418                                            if (printAssignmentsMenuItem)
    419                                                assignmentLeafItem(out, imgBase, a);
    420                                            else
    421                                                assignmentLeafItem(out, imgBase, x.getCounter(), a);
    422                                        }
    423                                    }
    424                                    if (printAssignmentsMenuItem)
    425                                        end_item(out);
    426                                }
    427                            }
    428                            end_item(out);
    429                        }
    430                        end_item(out);
    431                    }
    432                    end_item(out);
    433                }
    434            }
    435            else
    436                if (type == TYPE_CONSTRAINT_BASED) {
    437                    Hashtable constraint2assignments = new Hashtable();
    438                    Hashtable constraint2counter = new Hashtable();
    439                    for (Enumeration e1 = iNoGoods.keys(); e1.hasMoreElements();) {
    440                        Assignment ass = (Assignment)e1.nextElement();
    441                        for (Enumeration e2 = ((Vector)iNoGoods.get(ass)).elements();e2.hasMoreElements();) {
    442                            AssignmentSet set = (AssignmentSet)e2.nextElement();
    443                            if (set.getConstraint() == null) continue;
    444                            Hashtable assignments = (Hashtable)constraint2assignments.get(set.getConstraint());
    445                            if (assignments == null) {
    446                                assignments = new Hashtable();
    447                                constraint2assignments.put(set.getConstraint(),assignments);
    448                            }
    449                            Vector unassignments = (Vector)assignments.get(ass);
    450                            if (unassignments == null) {
    451                                unassignments = new FastVector();
    452                                assignments.put(ass, unassignments);
    453                            }
    454                            unassignments.addElement(set);
    455                            Long cnt = (Long)constraint2counter.get(set.getConstraint());
    456                            constraint2counter.put(set.getConstraint(),new Long(set.getCounter()+(cnt == null ? 0 : cnt.longValue())));
    457                        }
    458                    }
    459                    int constrCounter = 0;
    460                    for (Enumeration e1 = ToolBox.sortEnumeration(constraint2counter.keys(), new ConstraintComparator(constraint2counter)); e1.hasMoreElements();) {
    461                        Constraint constraint = (Constraint)e1.nextElement();
    462                        constrCounter++;
    463                        if (constrCounter > maxVariables)
    464                            break;
    465                        Long constrCnt = (Long)constraint2counter.get(constraint);
    466                        Hashtable constrAssignments = (Hashtable)constraint2assignments.get(constraint);
    467                        constraintMenuItem(out, imgBase, String.valueOf(constraint.getId()), constrCnt.longValue(), constraint);
    468
    469                        Hashtable variables = new Hashtable();
    470                        Hashtable variable2Assignments = new Hashtable();
    471                        for (Enumeration e2 = constrAssignments.keys(); e2.hasMoreElements(); ) {
    472                            Assignment ass = (Assignment)e2.nextElement();
    473                            long cnt = 0;
    474                            for (Enumeration e3 = ((Vector)constrAssignments.get(ass)).elements(); e3.hasMoreElements();)
    475                                cnt += ((AssignmentSet)e3.nextElement()).getCounter();
    476                            ass.setCounter(cnt);
    477                            cnt += (variables.containsKey(ass.getValue().variable()) ? ((Long)variables.get(ass.getValue().variable())).longValue() : 0L);
    478                            variables.put(ass.getValue().variable(), new Long(cnt));
    479                            Vector assignments = (Vector)variable2Assignments.get(ass.getValue().variable());
    480                            if (assignments == null) {
    481                                assignments = new FastVector();
    482                                variable2Assignments.put(ass.getValue().variable(),assignments);
    483                            }
    484                            assignments.addElement(ass);
    485                        }
    486
    487                        for (Enumeration e2 = ToolBox.sortEnumeration(variables.keys(),new VariableComparator(variables));e2.hasMoreElements();) {
    488                            Variable variable = (Variable)e2.nextElement();
    489                            long varCnt = ((Long)variables.get(variable)).longValue();
    490                            if (varCnt < unassignmentLimit)
    491                                continue;
    492                            unassignedVariableMenuItem(out,imgBase,constraint.getId() + "." + variable.getId(),varCnt,variable);
    493
    494                            for (Enumeration e3 = ToolBox.sortEnumeration(((Vector)variable2Assignments.get(variable)).elements(),Assignment.getComparator(iteration));e3.hasMoreElements();) {
    495                                Assignment ass = (Assignment)e3.nextElement();
    496                                if (!ass.getValue().variable().equals(variable))
    497                                    continue;
    498                                double cntUnas = 0.0;
    499                                for (Enumeration e4 = ((Vector)iNoGoods.get(ass)).elements();e4.hasMoreElements();)
    500                                    cntUnas += ((AssignmentSet)e4.nextElement()).getCounter();
    501                                if (Math.round(cntUnas) < assignmentLimit)
    502                                    continue;
    503                                unassignmentMenuItem(out, imgBase, constraint.getId()+"."+ass.getValue().variable().getId()+"."+ass.getValue().getId(),cntUnas,ass);
    504
    505                                int id = 0;
    506                                for (Enumeration e4 = ((Vector)constrAssignments.get(ass)).elements();e4.hasMoreElements();) {
    507                                    AssignmentSet x = (AssignmentSet)e4.nextElement();
    508                                    boolean printAssignmentsMenuItem = (x.getSet().size() > 2);
    509                                    if (printAssignmentsMenuItem)
    510                                        assignmentsMenuItem(out, imgBase, constraint.getId()+"."+ass.getValue().variable().getId()+"."+ass.getValue().getId()+"."+(++id), x);
    511                                    for (Enumeration e5 = ToolBox.sortEnumeration(x.getSet().elements(), Assignment.getComparator(iteration)); e5.hasMoreElements();) {
    512                                        Assignment a = (Assignment)e5.nextElement();
    513                                        if (!ass.equals(a)) {
    514                                            if (printAssignmentsMenuItem)
    515                                                assignmentLeafItem(out, imgBase, a);
    516                                            else
    517                                                assignmentLeafItem(out, imgBase, x.getCounter(),a);
    518                                        }
    519                                    }
    520                                    if (printAssignmentsMenuItem)
    521                                        end_item(out);
    522                                }
    523
    524                                end_item(out);
    525                            }
    526                            end_item(out);
    527                        }
    528                        end_item(out);
    529                    }
    530
    531                }
    532            if (printHeader) {
    533                out.println("</ul>");
    534                out.println("</body></html>");
    535            }
    536        }
    537
    538        /** Print conflict-based statistics */
    539        public void print(PrintWriter out, long iteration) {
    540            out.print("Statistics{");
    541            for (Enumeration e1 =ToolBox.sortEnumeration(iNoGoods.keys(),Assignment.getComparator(iteration));e1.hasMoreElements();) {
    542                Assignment ass = (Assignment)e1.nextElement();
    543                double cnt = 0.0;
    544                for (Enumeration e2 = ((Vector)iNoGoods.get(ass)).elements();e2.hasMoreElements();)
    545                    cnt += ((AssignmentSet)e2.nextElement()).getCounter();
    546                if (cnt < 100) continue;
    547                out.print("\n      "+cnt+"x "+ass.getValue().variable().getName()+" != "+ass.getValue().getName()+" <= {");
    548                for (Enumeration e2 = ((Vector)iNoGoods.get(ass)).elements();e2.hasMoreElements();) {
    549                    AssignmentSet x = (AssignmentSet)e2.nextElement();
    550                    if (x.getCounter() >= 10) {
    551                        out.print("\n        "+x.getCounter()+"x "+(x.getName() == null ? null : x.getName())+ "{");
    552                        for (Enumeration e3 = ToolBox.sortEnumeration(x.getSet().elements(),Assignment.getComparator(iteration));e3.hasMoreElements();) {
    553                            Assignment a = (Assignment)e3.nextElement();
    554                            out.print(a.getValue().variable().getName()+" := "+a.getValue().getName()+(e3.hasMoreElements() ? "," : ""));
    555                        }
    556                        out.print(e2.hasMoreElements() ? "}," : "}");
    557                    }
    558                }
    559                out.print("\n      }");
    560            }
    561            out.print("\n    }");
    562            out.flush();
    563        }
    564
    565        public String toString() {
    566            StringBuffer sb = new StringBuffer("Statistics{");
    567            for (Enumeration e1 = ToolBox.sortEnumeration(iUnassignedVariables.keys(), Assignment.getComparator(0));e1.hasMoreElements();) {
    568                Variable variable = (Variable)e1.nextElement();
    569                if (variable.countAssignments() < 100) continue;
    570                sb.append("\n      ").append(variable.countAssignments() + "x ").append(variable.getName()).append(" <= {");
    571                for (Enumeration e2 = ToolBox.sortEnumeration(((Vector)iUnassignedVariables.get(variable)).elements(),Assignment.getComparator(0));e2.hasMoreElements();) {
    572                    Assignment x = (Assignment)e2.nextElement();
    573                    if (x.getCounter(0) >= 10)
    574                        sb.append("\n        ").append(x.toString(0, true)).append(e2.hasMoreElements() ? "," : "");
    575                }
    576                sb.append("\n      }");
    577            }
    578            sb.append("\n    }");
    579            return sb.toString();
    580        }
    581
    582        public void getInfo(Hashtable info) {
    583            //info.put("Statistics: IsGood.Time",sTimeFormat.format(((double)iIsGoodTime)/60000.0)+" min");
    584            //info.put("Statistics: NoGood.Time",sTimeFormat.format(((double)iNoGoodTime)/60000.0)+" min");
    585            /*info.put("Statistics: VariableAssigned.Time",sTimeFormat.format(((double)iVariableAssignedTime)/60000.0)+" min");
    586             *info.put("Statistics: VariableUnassigned.Time",sTimeFormat.format(((double)iVariableUnassignedTime)/60000.0)+" min");
    587             *info.put("Statistics: Bad assignments:", String.valueOf(iBadAssignments.size()));*/
    588        }
    589
    590        private class VariableComparator implements java.util.Comparator {
    591            Hashtable iVars = null;
    592            public VariableComparator(Hashtable vars) {
    593                iVars = vars;
    594            }
    595            public int compare(Object o1, Object o2) {
    596                long c1 = ((Long)iVars.get(o1)).longValue();
    597                long c2 = ((Long)iVars.get(o2)).longValue();
    598                if (c1 != c2)
    599                    return (c1 < c2 ? 1 : -1);
    600                    return ((Variable)o1).getName().compareTo(((Variable)o2).getName());
    601            }
    602        }
    603
    604        private class ConstraintComparator implements java.util.Comparator {
    605            Hashtable iConstrs = null;
    606            public ConstraintComparator(Hashtable constrs) {
    607                iConstrs = constrs;
    608            }
    609            public int compare(Object o1, Object o2) {
    610                long c1 = ((Long)iConstrs.get(o1)).longValue();
    611                long c2 = ((Long)iConstrs.get(o2)).longValue();
    612                if (c1 != c2)
    613                    return (c1 < c2 ? 1 : -1);
    614                    return ((Constraint)o1).getName().compareTo(
    615                    ((Constraint)o2).getName());
    616            }
    617        }
    618
    619        public void constraintBeforeAssigned( long iteration, Constraint constraint, Value assigned, Set unassigned) {
    620        }
    621
    622        /** Increments appropriate counters when there is a value unassigned */
    623        public void constraintAfterAssigned(long iteration, Constraint constraint, Value assigned, Set unassigned) {
    624            if (unassigned == null || unassigned.isEmpty())
    625                return;
    626            if (iPrint) {
    627                AssignmentSet noGoods = AssignmentSet.createAssignmentSet(iteration,unassigned, iAgeing);
    628                noGoods.addAssignment(iteration, assigned, iAgeing);
    629                noGoods.setConstraint(constraint);
    630                for (Iterator i = unassigned.iterator(); i.hasNext();) {
    631                    Value unassignedValue = (Value)i.next();
    632                    variableUnassigned(iteration, unassignedValue, noGoods);
    633                    variableUnassigned(iteration, unassignedValue, assigned);
    634                }
    635            } else {
    636                for (Iterator i = unassigned.iterator(); i.hasNext();) {
    637                    Value unassignedValue = (Value)i.next();
    638                    variableUnassigned(iteration, unassignedValue, assigned);
    639                }
    640            }
    641        }
    642
    643        public void constraintAdded(Constraint constraint) {
    644            constraint.addConstraintListener(this);
    645        }
    646        public void constraintRemoved(Constraint constraint) {
    647            constraint.removeConstraintListener(this);
    648        }
    649
    650        /* Solution listener -- prints conflict-based statistics in HTML format.*/
    651        public void solutionUpdated(Solution solution) {
    652            if (iPrint && iPrintInterval>0 && (solution.getIteration()%iPrintInterval) == 0) {
    653                try {
    654                    int maxLines = getProperties().getPropertyInt("ConflictStatistics.MaxLines", 25);
    655                    int maxBr1 = getProperties().getPropertyInt("ConflictStatistics.MaxBranchingLev1", 100);
    656                    int maxBr2 = getProperties().getPropertyInt("ConflictStatistics.MaxBranchingLev2", 10);
    657                    String imgBase = getProperties().getProperty("ConflictStatistics.ImageBase", null);
    658                    if (TYPE_VARIABLE_BASED == getProperties().getPropertyInt("ConflictStatistics.Type",TYPE_VARIABLE_BASED)) {
    659                        PrintWriter pw = new PrintWriter(new FileWriter(getProperties().getProperty("General.Output", ".")+File.separator+"stat"+(++iPrintCounter)+".html"));
    660                        printHtml(solution.getIteration(),pw,true,maxLines,maxBr1,maxBr2,imgBase,TYPE_VARIABLE_BASED);
    661                        pw.flush();
    662                        pw.close();
    663                    } else {
    664                        PrintWriter pw = new PrintWriter(new FileWriter(getProperties().getProperty("General.Output", ".")+File.separator+"stat"+(++iPrintCounter)+".html"));
    665                        printHtml(solution.getIteration(),pw,true,maxLines,maxBr1,maxBr2,imgBase,TYPE_CONSTRAINT_BASED);
    666                        pw.flush();
    667                        pw.close();
    668                    }
    669                }
    670                catch (Exception io) {
    671                    io.printStackTrace();
    672                    sLogger.error(io);
    673                }
    674            }
    675        }
    676        public void getInfo(Solution solution, Dictionary info) {
    677        }
    678        public void bestCleared(Solution solution) {
    679        }
    680        public void bestSaved(Solution solution) {
    681        }
    682        public void bestRestored(Solution solution) {
    683        }
    684    }