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
34 import org.sat4j.core.ConstrGroup;
35 import org.sat4j.core.LiteralsUtils;
36 import org.sat4j.core.Vec;
37 import org.sat4j.core.VecInt;
38 import org.sat4j.minisat.core.ConflictTimer;
39 import org.sat4j.minisat.core.ConflictTimerAdapter;
40 import org.sat4j.minisat.core.Constr;
41 import org.sat4j.minisat.core.ILits;
42 import org.sat4j.minisat.core.IOrder;
43 import org.sat4j.minisat.core.LearnedConstraintsDeletionStrategy;
44 import org.sat4j.minisat.core.LearningStrategy;
45 import org.sat4j.minisat.core.RestartStrategy;
46 import org.sat4j.minisat.core.SearchParams;
47 import org.sat4j.minisat.core.Solver;
48 import org.sat4j.pb.IPBSolverService;
49 import org.sat4j.pb.ObjectiveFunction;
50 import org.sat4j.pb.orders.IOrderObjective;
51 import org.sat4j.specs.ContradictionException;
52 import org.sat4j.specs.IConstr;
53 import org.sat4j.specs.IVec;
54 import org.sat4j.specs.IVecInt;
55 import org.sat4j.specs.IteratorInt;
56
57 public abstract class PBSolver extends Solver<PBDataStructureFactory> implements
58 IPBCDCLSolver<PBDataStructureFactory>, IPBSolverService {
59
60 private ObjectiveFunction objf;
61
62
63
64
65 private static final long serialVersionUID = 1L;
66
67 protected PBSolverStats stats;
68
69 public PBSolver(LearningStrategy<PBDataStructureFactory> learner,
70 PBDataStructureFactory dsf, IOrder order, RestartStrategy restarter) {
71 super(learner, dsf, order, restarter);
72 this.stats = new PBSolverStats();
73 initStats(this.stats);
74 }
75
76 public PBSolver(LearningStrategy<PBDataStructureFactory> learner,
77 PBDataStructureFactory dsf, SearchParams params, IOrder order,
78 RestartStrategy restarter) {
79 super(learner, dsf, params, order, restarter);
80 this.stats = new PBSolverStats();
81 initStats(this.stats);
82 }
83
84 public IConstr addPseudoBoolean(IVecInt literals, IVec<BigInteger> coeffs,
85 boolean moreThan, BigInteger degree) throws ContradictionException {
86 IVecInt vlits = dimacs2internal(literals);
87 assert vlits.size() == literals.size();
88 assert literals.size() == coeffs.size();
89 return addConstr(this.dsfactory.createPseudoBooleanConstraint(vlits,
90 coeffs, moreThan, degree));
91 }
92
93 public void setObjectiveFunction(ObjectiveFunction obj) {
94 this.objf = obj;
95 IOrder order = getOrder();
96 if (order instanceof IOrderObjective) {
97 ((IOrderObjective) order).setObjectiveFunction(obj);
98 }
99 }
100
101 public ObjectiveFunction getObjectiveFunction() {
102 return this.objf;
103 }
104
105 public IConstr addAtMost(IVecInt literals, IVecInt coeffs, int degree)
106 throws ContradictionException {
107
108 IVec<BigInteger> bcoeffs = new Vec<BigInteger>(coeffs.size());
109 for (int i = 0; i < coeffs.size(); i++) {
110 bcoeffs.push(BigInteger.valueOf(coeffs.get(i)));
111 }
112 return addAtMost(literals, bcoeffs, BigInteger.valueOf(degree));
113 }
114
115 public IConstr addAtMost(IVecInt literals, IVec<BigInteger> coeffs,
116 BigInteger degree) throws ContradictionException {
117 IVecInt vlits = dimacs2internal(literals);
118 assert vlits.size() == literals.size();
119 assert literals.size() == coeffs.size();
120 return addConstr(this.dsfactory.createPseudoBooleanConstraint(vlits,
121 coeffs, false, degree));
122 }
123
124 public IConstr addAtLeast(IVecInt literals, IVecInt coeffs, int degree)
125 throws ContradictionException {
126
127 IVec<BigInteger> bcoeffs = new Vec<BigInteger>(coeffs.size());
128 for (int i = 0; i < coeffs.size(); i++) {
129 bcoeffs.push(BigInteger.valueOf(coeffs.get(i)));
130 }
131 return addAtLeast(literals, bcoeffs, BigInteger.valueOf(degree));
132 }
133
134 public IConstr addAtLeast(IVecInt literals, IVec<BigInteger> coeffs,
135 BigInteger degree) throws ContradictionException {
136 IVecInt vlits = dimacs2internal(literals);
137 assert vlits.size() == literals.size();
138 assert literals.size() == coeffs.size();
139 return addConstr(this.dsfactory.createPseudoBooleanConstraint(vlits,
140 coeffs, true, degree));
141 }
142
143 public IConstr addExactly(IVecInt literals, IVecInt coeffs, int weight)
144 throws ContradictionException {
145
146 IVec<BigInteger> bcoeffs = new Vec<BigInteger>(coeffs.size());
147 for (int i = 0; i < coeffs.size(); i++) {
148 bcoeffs.push(BigInteger.valueOf(coeffs.get(i)));
149 }
150 return addExactly(literals, bcoeffs, BigInteger.valueOf(weight));
151 }
152
153 public IConstr addExactly(IVecInt literals, IVec<BigInteger> coeffs,
154 BigInteger weight) throws ContradictionException {
155 IVecInt vlits = dimacs2internal(literals);
156 assert vlits.size() == literals.size();
157 assert literals.size() == coeffs.size();
158 ConstrGroup group = new ConstrGroup(false);
159 group.add(addConstr(this.dsfactory.createPseudoBooleanConstraint(vlits,
160 coeffs, false, weight)));
161 group.add(addConstr(this.dsfactory.createPseudoBooleanConstraint(vlits,
162 coeffs, true, weight)));
163 return group;
164 }
165
166 private IConstr previousConstr = null;
167
168 public IConstr addAtMostOnTheFly(IVecInt literals, IVec<BigInteger> coefs,
169 BigInteger degree) {
170 IVecInt vlits = dimacs2internal(literals);
171 if (previousConstr != null) {
172 removeSubsumedConstr(previousConstr);
173 }
174 this.sharedConflict = this.dsfactory
175 .createUnregisteredAtMostConstraint(vlits, coefs, degree);
176 this.sharedConflict.register();
177 addConstr(this.sharedConflict);
178 previousConstr = this.sharedConflict;
179
180
181 IVecInt outReason = new VecInt();
182 this.sharedConflict.calcReasonOnTheFly(ILits.UNDEFINED, trail,
183 outReason);
184 while (!trail.isEmpty() && !outReason.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 }