View Javadoc

1   package org.sat4j.minisat.restarts;
2   
3   import org.sat4j.minisat.core.RestartStrategy;
4   import org.sat4j.minisat.core.SearchParams;
5   
6   /**
7    * Luby series code taken from SATZ_rand 5.0 from Henry Kautz
8    * http://www.cs.rochester.edu/u/kautz/satz-rand/satz-rand-v5.0.tgz
9    * 
10   * <pre>
11   * Luby's series 
12   *  long luby_super(int i)
13   *  {
14   *  long power;
15   *  int k;
16   * 
17   *  if (i&lt;=0){
18   *  fprintf(stderr, &quot;bad argument super(%d)\n&quot;, i);
19   *  exit(1);
20   *  }
21   *  /* let 2&circ;k be the least power of 2 &gt;= (i+1) 
22   *  k = 1;
23   *  power = 2;
24   *  while (power &lt; (i+1)){
25   *  k += 1;
26   *  power *= 2;
27   *  }
28   *  if (power == (i+1)) return (power/2);
29   *  return (luby_super(i - (power/2) + 1));
30   *  }
31   * </pre>
32   */
33  public class LubyRestarts implements RestartStrategy {
34  
35      /**
36       * 
37       */
38      private static final long serialVersionUID = 1L;
39  
40      static final long luby_super(long i) {
41          long power;
42          long k;
43  
44          assert i > 0;
45          /* let 2^k be the least power of 2 >= (i+1) */
46          k = 1;
47          power = 2;
48          while (power < (i + 1)) {
49              k += 1;
50              power *= 2;
51          }
52          if (power == (i + 1))
53              return (power / 2);
54          return (luby_super(i - (power / 2) + 1));
55      }
56  
57      private int factor;
58      private int count;
59      
60      public LubyRestarts() {
61          setFactor(32); // uses TiniSAT default
62      }
63      
64      public void setFactor(int factor) {
65          this.factor = factor;
66      }
67      
68      public int getFactor() {
69          return factor;
70      }
71      
72      public void init(SearchParams params) {
73          count = 1;
74      }
75  
76      public long nextRestartNumberOfConflict() {
77          return luby_super(count)*factor;
78      }
79  
80      public void onRestart() {
81          count++;
82      }
83      
84      @Override
85      public String toString() {
86          return "luby style (SATZ_rand, TiniSAT) restarts strategy with factor "+factor; 
87      }
88  
89  }