1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30 package org.sat4j.pb.core;
31
32 import java.math.BigInteger;
33 import java.util.HashSet;
34 import java.util.Set;
35
36 import org.sat4j.core.ConstrGroup;
37 import org.sat4j.core.LiteralsUtils;
38 import org.sat4j.core.Vec;
39 import org.sat4j.core.VecInt;
40 import org.sat4j.minisat.core.ConflictTimer;
41 import org.sat4j.minisat.core.ConflictTimerAdapter;
42 import org.sat4j.minisat.core.Constr;
43 import org.sat4j.minisat.core.ILits;
44 import org.sat4j.minisat.core.IOrder;
45 import org.sat4j.minisat.core.LearnedConstraintsDeletionStrategy;
46 import org.sat4j.minisat.core.LearningStrategy;
47 import org.sat4j.minisat.core.RestartStrategy;
48 import org.sat4j.minisat.core.SearchParams;
49 import org.sat4j.minisat.core.Solver;
50 import org.sat4j.pb.IPBSolverService;
51 import org.sat4j.pb.ObjectiveFunction;
52 import org.sat4j.pb.orders.IOrderObjective;
53 import org.sat4j.specs.ContradictionException;
54 import org.sat4j.specs.IConstr;
55 import org.sat4j.specs.IVec;
56 import org.sat4j.specs.IVecInt;
57 import org.sat4j.specs.IteratorInt;
58
59 public abstract class PBSolver extends Solver<PBDataStructureFactory> implements
60 IPBCDCLSolver<PBDataStructureFactory>, IPBSolverService {
61
62 private ObjectiveFunction objf;
63
64
65
66
67 private static final long serialVersionUID = 1L;
68
69 protected PBSolverStats stats;
70
71 public PBSolver(LearningStrategy<PBDataStructureFactory> learner,
72 PBDataStructureFactory dsf, IOrder order, RestartStrategy restarter) {
73 super(learner, dsf, order, restarter);
74 this.stats = new PBSolverStats();
75 initStats(this.stats);
76 }
77
78 public PBSolver(LearningStrategy<PBDataStructureFactory> learner,
79 PBDataStructureFactory dsf, SearchParams params, IOrder order,
80 RestartStrategy restarter) {
81 super(learner, dsf, params, order, restarter);
82 this.stats = new PBSolverStats();
83 initStats(this.stats);
84 }
85
86 public IConstr addPseudoBoolean(IVecInt literals, IVec<BigInteger> coeffs,
87 boolean moreThan, BigInteger degree) throws ContradictionException {
88 IVecInt vlits = dimacs2internal(literals);
89 assert vlits.size() == literals.size();
90 assert literals.size() == coeffs.size();
91 return addConstr(this.dsfactory.createPseudoBooleanConstraint(vlits,
92 coeffs, moreThan, degree));
93 }
94
95 public void setObjectiveFunction(ObjectiveFunction obj) {
96 this.objf = obj;
97 IOrder order = getOrder();
98 if (order instanceof IOrderObjective) {
99 ((IOrderObjective) order).setObjectiveFunction(obj);
100 }
101 }
102
103 public ObjectiveFunction getObjectiveFunction() {
104 return this.objf;
105 }
106
107 public IConstr addAtMost(IVecInt literals, IVecInt coeffs, int degree)
108 throws ContradictionException {
109
110 IVec<BigInteger> bcoeffs = new Vec<BigInteger>(coeffs.size());
111 for (int i = 0; i < coeffs.size(); i++) {
112 bcoeffs.push(BigInteger.valueOf(coeffs.get(i)));
113 }
114 return addAtMost(literals, bcoeffs, BigInteger.valueOf(degree));
115 }
116
117 public IConstr addAtMost(IVecInt literals, IVec<BigInteger> coeffs,
118 BigInteger degree) throws ContradictionException {
119 IVecInt vlits = dimacs2internal(literals);
120 assert vlits.size() == literals.size();
121 assert literals.size() == coeffs.size();
122 return addConstr(this.dsfactory.createPseudoBooleanConstraint(vlits,
123 coeffs, false, degree));
124 }
125
126 public IConstr addAtLeast(IVecInt literals, IVecInt coeffs, int degree)
127 throws ContradictionException {
128
129 IVec<BigInteger> bcoeffs = new Vec<BigInteger>(coeffs.size());
130 for (int i = 0; i < coeffs.size(); i++) {
131 bcoeffs.push(BigInteger.valueOf(coeffs.get(i)));
132 }
133 return addAtLeast(literals, bcoeffs, BigInteger.valueOf(degree));
134 }
135
136 public IConstr addAtLeast(IVecInt literals, IVec<BigInteger> coeffs,
137 BigInteger degree) throws ContradictionException {
138 IVecInt vlits = dimacs2internal(literals);
139 assert vlits.size() == literals.size();
140 assert literals.size() == coeffs.size();
141 return addConstr(this.dsfactory.createPseudoBooleanConstraint(vlits,
142 coeffs, true, degree));
143 }
144
145 public IConstr addExactly(IVecInt literals, IVecInt coeffs, int weight)
146 throws ContradictionException {
147
148 IVec<BigInteger> bcoeffs = new Vec<BigInteger>(coeffs.size());
149 for (int i = 0; i < coeffs.size(); i++) {
150 bcoeffs.push(BigInteger.valueOf(coeffs.get(i)));
151 }
152 return addExactly(literals, bcoeffs, BigInteger.valueOf(weight));
153 }
154
155 public IConstr addExactly(IVecInt literals, IVec<BigInteger> coeffs,
156 BigInteger weight) throws ContradictionException {
157 IVecInt vlits = dimacs2internal(literals);
158 assert vlits.size() == literals.size();
159 assert literals.size() == coeffs.size();
160 ConstrGroup group = new ConstrGroup(false);
161 group.add(addConstr(this.dsfactory.createPseudoBooleanConstraint(vlits,
162 coeffs, false, weight)));
163 group.add(addConstr(this.dsfactory.createPseudoBooleanConstraint(vlits,
164 coeffs, true, weight)));
165 return group;
166 }
167
168 public IConstr addAtMostOnTheFly(IVecInt literals, IVec<BigInteger> coefs,
169 BigInteger degree) {
170 IVecInt vlits = dimacs2internal(literals);
171 this.sharedConflict = this.dsfactory
172 .createUnregisteredAtMostConstraint(vlits, coefs, degree);
173 this.sharedConflict.register();
174 addConstr(this.sharedConflict);
175
176
177 IVecInt outReason = new VecInt();
178 this.sharedConflict.calcReasonOnTheFly(ILits.UNDEFINED, trail,
179 outReason);
180 Set<Integer> subset = new HashSet<Integer>();
181 for (IteratorInt it = outReason.iterator(); it.hasNext();) {
182 subset.add(it.next());
183 }
184 while (!trail.isEmpty() && !subset.contains(trail.last())) {
185 undoOne();
186 if (!trailLim.isEmpty() && trailLim.last() == trail.size()) {
187 trailLim.pop();
188 }
189 }
190 return this.sharedConflict;
191 }
192
193 public IConstr addAtMostOnTheFly(IVecInt literals, IVecInt coefs, int degree) {
194 IVec<BigInteger> coeffsCpy = new Vec<BigInteger>(coefs.size());
195 for (IteratorInt iterator = coefs.iterator(); iterator.hasNext();) {
196 coeffsCpy.push(BigInteger.valueOf(iterator.next()));
197 }
198 return addAtMostOnTheFly(literals, coeffsCpy,
199 BigInteger.valueOf(degree));
200 }
201
202
203
204
205 public final LearnedConstraintsDeletionStrategy objectiveFunctionBased = new LearnedConstraintsDeletionStrategy() {
206
207 private static final long serialVersionUID = 1L;
208 private boolean[] inObjectiveFunction;
209
210 private final ConflictTimer clauseManagement = new ConflictTimerAdapter(
211 1000) {
212 private static final long serialVersionUID = 1L;
213 private int nbconflict = 0;
214 private static final int MAX_CLAUSE = 5000;
215 private static final int INC_CLAUSE = 1000;
216 private int nextbound = MAX_CLAUSE;
217
218 @Override
219 public void run() {
220 this.nbconflict += bound();
221 if (this.nbconflict >= this.nextbound) {
222 this.nextbound += INC_CLAUSE;
223 this.nbconflict = 0;
224 setNeedToReduceDB(true);
225 }
226 }
227
228 @Override
229 public void reset() {
230 super.reset();
231 this.nextbound = MAX_CLAUSE;
232 if (this.nbconflict >= this.nextbound) {
233 this.nbconflict = 0;
234 setNeedToReduceDB(true);
235 }
236 }
237 };
238
239 public void reduce(IVec<Constr> learnedConstrs) {
240 int i, j;
241 for (i = j = 0; i < learnedConstrs.size(); i++) {
242 Constr c = learnedConstrs.get(i);
243 if (c.locked() || c.getActivity() <= 2.0) {
244 learnedConstrs.set(j++, PBSolver.this.learnts.get(i));
245 } else {
246 c.remove(PBSolver.this);
247 }
248 }
249 if (isVerbose()) {
250 System.out
251 .println(getLogPrefix()
252 + "cleaning " + (learnedConstrs.size() - j)
253 + " clauses out of " + learnedConstrs.size() + "/" + PBSolver.this.stats.conflicts);
254 System.out.flush();
255 }
256 PBSolver.this.learnts.shrinkTo(j);
257
258 }
259
260 public ConflictTimer getTimer() {
261 return this.clauseManagement;
262 }
263
264 @Override
265 public String toString() {
266 return "Objective function driven learned constraints deletion strategy";
267 }
268
269 public void init() {
270 this.inObjectiveFunction = new boolean[nVars() + 1];
271 if (PBSolver.this.objf == null) {
272 throw new IllegalStateException(
273 "The strategy does not make sense if there is no objective function");
274 }
275 for (IteratorInt it = PBSolver.this.objf.getVars().iterator(); it
276 .hasNext();) {
277 this.inObjectiveFunction[Math.abs(it.next())] = true;
278 }
279 this.clauseManagement.reset();
280 }
281
282 public void onClauseLearning(Constr constr) {
283 boolean fullObj = true;
284
285 for (int i = 0; i < constr.size(); i++) {
286 fullObj = fullObj
287 && this.inObjectiveFunction[LiteralsUtils.var(constr
288 .get(i))];
289 }
290 if (fullObj) {
291 constr.incActivity(1.0);
292 } else {
293 constr.incActivity(constr.size());
294 }
295 }
296
297 public void onConflictAnalysis(Constr reason) {
298
299 }
300
301 public void onPropagation(Constr from) {
302
303 }
304 };
305 }