1 /*******************************************************************************
2 * SAT4J: a SATisfiability library for Java Copyright (C) 2004, 2012 Artois University and CNRS
3 *
4 * All rights reserved. This program and the accompanying materials
5 * are made available under the terms of the Eclipse Public License v1.0
6 * which accompanies this distribution, and is available at
7 * http://www.eclipse.org/legal/epl-v10.html
8 *
9 * Alternatively, the contents of this file may be used under the terms of
10 * either the GNU Lesser General Public License Version 2.1 or later (the
11 * "LGPL"), in which case the provisions of the LGPL are applicable instead
12 * of those above. If you wish to allow use of your version of this file only
13 * under the terms of the LGPL, and not to allow others to use your version of
14 * this file under the terms of the EPL, indicate your decision by deleting
15 * the provisions above and replace them with the notice and other provisions
16 * required by the LGPL. If you do not delete the provisions above, a recipient
17 * may use your version of this file under the terms of the EPL or the LGPL.
18 *
19 * Based on the original MiniSat specification from:
20 *
21 * An extensible SAT solver. Niklas Een and Niklas Sorensson. Proceedings of the
22 * Sixth International Conference on Theory and Applications of Satisfiability
23 * Testing, LNCS 2919, pp 502-518, 2003.
24 *
25 * See www.minisat.se for the original solver in C++.
26 *
27 * Contributors:
28 * CRIL - initial API and implementation
29 *******************************************************************************/
30 package org.sat4j.minisat.restarts;
31
32 import org.sat4j.minisat.core.Constr;
33 import org.sat4j.minisat.core.RestartStrategy;
34 import org.sat4j.minisat.core.SearchParams;
35 import org.sat4j.minisat.core.SolverStats;
36
37 /**
38 * Luby series
39 */
40 public final class LubyRestarts implements RestartStrategy {
41
42 public static final int DEFAULT_LUBY_FACTOR = 32;
43
44 /**
45 *
46 */
47 private static final long serialVersionUID = 1L;
48
49 // 21-06-2012 back from SAT 2012
50 // computing luby values the way presented by Donald Knuth in his invited
51 // talk at the SAT 2012 conference
52 // u1
53 private int un = 1;
54 // v1
55 private int vn = 1;
56
57 /**
58 * returns the current value of the luby sequence.
59 *
60 * @return the current value of the luby sequence.
61 */
62 public int luby() {
63 return this.vn;
64 }
65
66 /**
67 * Computes and return the next value of the luby sequence. That method has
68 * a side effect of the value returned by luby(). luby()!=nextLuby() but
69 * nextLuby()==luby().
70 *
71 * @return the new current value of the luby sequence.
72 * @see #luby()
73 */
74 public int nextLuby() {
75 if ((this.un & -this.un) == this.vn) {
76 this.un = this.un + 1;
77 this.vn = 1;
78 } else {
79 this.vn = this.vn << 1;
80 }
81 return this.vn;
82 }
83
84 private int factor;
85
86 private int bound;
87 private int conflictcount;
88
89 public LubyRestarts() {
90 this(DEFAULT_LUBY_FACTOR); // uses TiniSAT default
91 }
92
93 /**
94 * @param factor
95 * the factor used for the Luby series.
96 * @since 2.1
97 */
98 public LubyRestarts(int factor) {
99 setFactor(factor);
100 }
101
102 public void setFactor(int factor) {
103 this.factor = factor;
104 }
105
106 public int getFactor() {
107 return this.factor;
108 }
109
110 public void init(SearchParams params, SolverStats stats) {
111 this.un = 1;
112 this.vn = 1;
113 this.bound = luby() * this.factor;
114 }
115
116 public long nextRestartNumberOfConflict() {
117 return this.bound;
118 }
119
120 public void onRestart() {
121 this.bound = nextLuby() * this.factor;
122 this.conflictcount = 0;
123 }
124
125 @Override
126 public String toString() {
127 return "luby style (SATZ_rand, TiniSAT) restarts strategy with factor "
128 + this.factor;
129 }
130
131 public boolean shouldRestart() {
132 return this.conflictcount >= this.bound;
133 }
134
135 public void onBackjumpToRootLevel() {
136 this.conflictcount = 0;
137 }
138
139 public void reset() {
140 this.conflictcount = 0;
141 }
142
143 public void newConflict() {
144 this.conflictcount++;
145 }
146
147 public void newLearnedClause(Constr learned, int trailLevel) {
148 }
149 }