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.minisat.core.ConflictTimer;
38 import org.sat4j.minisat.core.ConflictTimerAdapter;
39 import org.sat4j.minisat.core.Constr;
40 import org.sat4j.minisat.core.IOrder;
41 import org.sat4j.minisat.core.LearnedConstraintsDeletionStrategy;
42 import org.sat4j.minisat.core.LearningStrategy;
43 import org.sat4j.minisat.core.RestartStrategy;
44 import org.sat4j.minisat.core.SearchParams;
45 import org.sat4j.minisat.core.Solver;
46 import org.sat4j.pb.ObjectiveFunction;
47 import org.sat4j.pb.orders.IOrderObjective;
48 import org.sat4j.specs.ContradictionException;
49 import org.sat4j.specs.IConstr;
50 import org.sat4j.specs.IVec;
51 import org.sat4j.specs.IVecInt;
52 import org.sat4j.specs.IteratorInt;
53
54 public abstract class PBSolver extends Solver<PBDataStructureFactory> implements
55 IPBCDCLSolver<PBDataStructureFactory> {
56
57 private ObjectiveFunction objf;
58
59
60
61
62 private static final long serialVersionUID = 1L;
63
64 protected PBSolverStats stats;
65
66 public PBSolver(LearningStrategy<PBDataStructureFactory> learner,
67 PBDataStructureFactory dsf, IOrder order, RestartStrategy restarter) {
68 super(learner, dsf, order, restarter);
69 this.stats = new PBSolverStats();
70 initStats(this.stats);
71 }
72
73 public PBSolver(LearningStrategy<PBDataStructureFactory> learner,
74 PBDataStructureFactory dsf, SearchParams params, IOrder order,
75 RestartStrategy restarter) {
76 super(learner, dsf, params, order, restarter);
77 this.stats = new PBSolverStats();
78 initStats(this.stats);
79 }
80
81 public IConstr addPseudoBoolean(IVecInt literals, IVec<BigInteger> coeffs,
82 boolean moreThan, BigInteger degree) throws ContradictionException {
83 IVecInt vlits = dimacs2internal(literals);
84 assert vlits.size() == literals.size();
85 assert literals.size() == coeffs.size();
86 return addConstr(this.dsfactory.createPseudoBooleanConstraint(vlits,
87 coeffs, moreThan, degree));
88 }
89
90 public void setObjectiveFunction(ObjectiveFunction obj) {
91 this.objf = obj;
92 IOrder order = getOrder();
93 if (order instanceof IOrderObjective) {
94 ((IOrderObjective) order).setObjectiveFunction(obj);
95 }
96 }
97
98 public ObjectiveFunction getObjectiveFunction() {
99 return this.objf;
100 }
101
102 public IConstr addAtMost(IVecInt literals, IVecInt coeffs, int degree)
103 throws ContradictionException {
104
105 IVec<BigInteger> bcoeffs = new Vec<BigInteger>(coeffs.size());
106 for (int i = 0; i < coeffs.size(); i++) {
107 bcoeffs.push(BigInteger.valueOf(coeffs.get(i)));
108 }
109 return addAtMost(literals, bcoeffs, BigInteger.valueOf(degree));
110 }
111
112 public IConstr addAtMost(IVecInt literals, IVec<BigInteger> coeffs,
113 BigInteger degree) throws ContradictionException {
114 IVecInt vlits = dimacs2internal(literals);
115 assert vlits.size() == literals.size();
116 assert literals.size() == coeffs.size();
117 return addConstr(this.dsfactory.createPseudoBooleanConstraint(vlits,
118 coeffs, false, degree));
119 }
120
121 public IConstr addAtLeast(IVecInt literals, IVecInt coeffs, int degree)
122 throws ContradictionException {
123
124 IVec<BigInteger> bcoeffs = new Vec<BigInteger>(coeffs.size());
125 for (int i = 0; i < coeffs.size(); i++) {
126 bcoeffs.push(BigInteger.valueOf(coeffs.get(i)));
127 }
128 return addAtLeast(literals, bcoeffs, BigInteger.valueOf(degree));
129 }
130
131 public IConstr addAtLeast(IVecInt literals, IVec<BigInteger> coeffs,
132 BigInteger degree) throws ContradictionException {
133 IVecInt vlits = dimacs2internal(literals);
134 assert vlits.size() == literals.size();
135 assert literals.size() == coeffs.size();
136 return addConstr(this.dsfactory.createPseudoBooleanConstraint(vlits,
137 coeffs, true, degree));
138 }
139
140 public IConstr addExactly(IVecInt literals, IVecInt coeffs, int weight)
141 throws ContradictionException {
142
143 IVec<BigInteger> bcoeffs = new Vec<BigInteger>(coeffs.size());
144 for (int i = 0; i < coeffs.size(); i++) {
145 bcoeffs.push(BigInteger.valueOf(coeffs.get(i)));
146 }
147 return addExactly(literals, bcoeffs, BigInteger.valueOf(weight));
148 }
149
150 public IConstr addExactly(IVecInt literals, IVec<BigInteger> coeffs,
151 BigInteger weight) throws ContradictionException {
152 IVecInt vlits = dimacs2internal(literals);
153 assert vlits.size() == literals.size();
154 assert literals.size() == coeffs.size();
155 ConstrGroup group = new ConstrGroup(false);
156 group.add(addConstr(this.dsfactory.createPseudoBooleanConstraint(vlits,
157 coeffs, false, weight)));
158 group.add(addConstr(this.dsfactory.createPseudoBooleanConstraint(vlits,
159 coeffs, true, weight)));
160 return group;
161 }
162
163
164
165
166 public final LearnedConstraintsDeletionStrategy objectiveFunctionBased = new LearnedConstraintsDeletionStrategy() {
167
168 private static final long serialVersionUID = 1L;
169 private boolean[] inObjectiveFunction;
170
171 private final ConflictTimer clauseManagement = new ConflictTimerAdapter(
172 1000) {
173 private static final long serialVersionUID = 1L;
174 private int nbconflict = 0;
175 private static final int MAX_CLAUSE = 5000;
176 private static final int INC_CLAUSE = 1000;
177 private int nextbound = MAX_CLAUSE;
178
179 @Override
180 public void run() {
181 this.nbconflict += bound();
182 if (this.nbconflict >= this.nextbound) {
183 this.nextbound += INC_CLAUSE;
184 this.nbconflict = 0;
185 setNeedToReduceDB(true);
186 }
187 }
188
189 @Override
190 public void reset() {
191 super.reset();
192 this.nextbound = MAX_CLAUSE;
193 if (this.nbconflict >= this.nextbound) {
194 this.nbconflict = 0;
195 setNeedToReduceDB(true);
196 }
197 }
198 };
199
200 public void reduce(IVec<Constr> learnedConstrs) {
201 int i, j;
202 for (i = j = 0; i < learnedConstrs.size(); i++) {
203 Constr c = learnedConstrs.get(i);
204 if (c.locked() || c.getActivity() <= 2.0) {
205 learnedConstrs.set(j++, PBSolver.this.learnts.get(i));
206 } else {
207 c.remove(PBSolver.this);
208 }
209 }
210 if (isVerbose()) {
211 System.out
212 .println(getLogPrefix()
213 + "cleaning " + (learnedConstrs.size() - j)
214 + " clauses out of " + learnedConstrs.size() + "/" + PBSolver.this.stats.conflicts);
215 System.out.flush();
216 }
217 PBSolver.this.learnts.shrinkTo(j);
218
219 }
220
221 public ConflictTimer getTimer() {
222 return this.clauseManagement;
223 }
224
225 @Override
226 public String toString() {
227 return "Objective function driven learned constraints deletion strategy";
228 }
229
230 public void init() {
231 this.inObjectiveFunction = new boolean[nVars() + 1];
232 if (PBSolver.this.objf == null) {
233 throw new IllegalStateException(
234 "The strategy does not make sense if there is no objective function");
235 }
236 for (IteratorInt it = PBSolver.this.objf.getVars().iterator(); it
237 .hasNext();) {
238 this.inObjectiveFunction[Math.abs(it.next())] = true;
239 }
240 this.clauseManagement.reset();
241 }
242
243 public void onClauseLearning(Constr constr) {
244 boolean fullObj = true;
245
246 for (int i = 0; i < constr.size(); i++) {
247 fullObj = fullObj
248 && this.inObjectiveFunction[LiteralsUtils.var(constr
249 .get(i))];
250 }
251 if (fullObj) {
252 constr.incActivity(1.0);
253 } else {
254 constr.incActivity(constr.size());
255 }
256 }
257
258 public void onConflictAnalysis(Constr reason) {
259
260 }
261
262 public void onPropagation(Constr from) {
263
264 }
265 };
266 }