View Javadoc

1   /*
2    * SAT4J: a SATisfiability library for Java Copyright (C) 2004-2006 Daniel Le Berre
3    * 
4    * Based on the original minisat specification from:
5    * 
6    * An extensible SAT solver. Niklas E?n and Niklas S?rensson. Proceedings of the
7    * Sixth International Conference on Theory and Applications of Satisfiability
8    * Testing, LNCS 2919, pp 502-518, 2003.
9    * 
10   * This library is free software; you can redistribute it and/or modify it under
11   * the terms of the GNU Lesser General Public License as published by the Free
12   * Software Foundation; either version 2.1 of the License, or (at your option)
13   * any later version.
14   * 
15   * This library is distributed in the hope that it will be useful, but WITHOUT
16   * ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS
17   * FOR A PARTICULAR PURPOSE. See the GNU Lesser General Public License for more
18   * details.
19   * 
20   * You should have received a copy of the GNU Lesser General Public License
21   * along with this library; if not, write to the Free Software Foundation, Inc.,
22   * 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
23   * 
24   */
25  
26  package org.sat4j.minisat.core;
27  
28  import java.io.PrintWriter;
29  import java.io.Serializable;
30  import java.lang.reflect.Field;
31  import java.util.HashMap;
32  import java.util.Map;
33  
34  /**
35   * Contains some statistics regarding the search.
36   * 
37   * @author daniel
38   * 
39   */
40  public class SolverStats implements Serializable {
41      private static final long serialVersionUID = 1L;
42  
43      public int starts;
44  
45      public long decisions;
46  
47      public long propagations;
48  
49      public long inspects;
50  
51      public long conflicts;
52  
53      public long learnedliterals;
54  
55      public long learnedbinaryclauses;
56  
57      public long learnedternaryclauses;
58  
59      public long learnedclauses;
60  
61      public long rootSimplifications;
62  
63      public long reducedliterals;
64  
65      public long changedreason;
66  
67      public int reduceddb;
68  
69      public void reset() {
70          starts = 0;
71          decisions = 0;
72          propagations = 0;
73          inspects = 0;
74          conflicts = 0;
75          learnedliterals = 0;
76          learnedclauses = 0;
77          learnedbinaryclauses = 0;
78          learnedternaryclauses = 0;
79          rootSimplifications = 0;
80          reducedliterals = 0;
81          changedreason = 0;
82          reduceddb = 0;
83      }
84  
85      public void printStat(PrintWriter out, String prefix) {
86          out.println(prefix + "starts\t\t: " + starts);
87          out.println(prefix + "conflicts\t\t: " + conflicts);
88          out.println(prefix + "decisions\t\t: " + decisions);
89          out.println(prefix + "propagations\t\t: " + propagations);
90          out.println(prefix + "inspects\t\t: " + inspects);
91          out.println(prefix + "learnt literals\t: " + learnedliterals);
92          out
93                  .println(prefix + "learnt binary clauses\t: "
94                          + learnedbinaryclauses);
95          out.println(prefix + "learnt ternary clauses\t: "
96                  + learnedternaryclauses);
97          out.println(prefix + "learnt clauses\t: " + learnedclauses);
98          out.println(prefix + "root simplifications\t: " + rootSimplifications);
99          out.println(prefix + "removed literals (reason simplification)\t: "
100                 + reducedliterals);
101         out.println(prefix + "reason swapping (by a shorter reason)\t: "
102                 + changedreason);
103         out.println(prefix + "Calls to reduceDB\t: " + reduceddb);
104     }
105 
106     public Map<String, Number> toMap() {
107         Map<String, Number> map = new HashMap<String, Number>();
108         for (Field f : this.getClass().getDeclaredFields()) {
109             try {
110                 map.put(f.getName(), (Number) f.get(this));
111             } catch (IllegalArgumentException e) {
112                 // TODO Auto-generated catch block
113                 e.printStackTrace();
114             } catch (IllegalAccessException e) {
115                 // TODO Auto-generated catch block
116                 e.printStackTrace();
117             }
118         }
119         return map;
120     }
121 }