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 |
|
package org.sat4j.minisat; |
28 |
|
|
29 |
|
import java.io.Serializable; |
30 |
|
|
31 |
|
import org.sat4j.core.ASolverFactory; |
32 |
|
import org.sat4j.minisat.constraints.CardinalityDataStructure; |
33 |
|
import org.sat4j.minisat.constraints.ClausalDataStructureCB; |
34 |
|
import org.sat4j.minisat.constraints.ClausalDataStructureCBWL; |
35 |
|
import org.sat4j.minisat.constraints.MixedDataStructureDaniel; |
36 |
|
import org.sat4j.minisat.constraints.MixedDataStructureDanielCBWL; |
37 |
|
import org.sat4j.minisat.constraints.MixedDataStructureWithBinary; |
38 |
|
import org.sat4j.minisat.constraints.MixedDataStructureWithBinaryAndTernary; |
39 |
|
import org.sat4j.minisat.constraints.PBMaxCBClauseCardConstrDataStructure; |
40 |
|
import org.sat4j.minisat.constraints.PBMaxClauseAtLeastConstrDataStructure; |
41 |
|
import org.sat4j.minisat.constraints.PBMaxClauseCardConstrDataStructure; |
42 |
|
import org.sat4j.minisat.constraints.PBMaxDataStructure; |
43 |
|
import org.sat4j.minisat.constraints.PBMinClauseCardConstrDataStructure; |
44 |
|
import org.sat4j.minisat.constraints.PBMinDataStructure; |
45 |
|
import org.sat4j.minisat.constraints.PuebloPBMinClauseAtLeastConstrDataStructure; |
46 |
|
import org.sat4j.minisat.constraints.PuebloPBMinClauseCardConstrDataStructure; |
47 |
|
import org.sat4j.minisat.constraints.PuebloPBMinDataStructure; |
48 |
|
import org.sat4j.minisat.constraints.pb.PBSolver; |
49 |
|
import org.sat4j.minisat.constraints.pb.PBSolverClause; |
50 |
|
import org.sat4j.minisat.constraints.pb.PBSolverMerging; |
51 |
|
import org.sat4j.minisat.constraints.pb.PBSolverWithImpliedClause; |
52 |
|
import org.sat4j.minisat.core.DataStructureFactory; |
53 |
|
import org.sat4j.minisat.core.ILits; |
54 |
|
import org.sat4j.minisat.core.ILits23; |
55 |
|
import org.sat4j.minisat.core.IOrder; |
56 |
|
import org.sat4j.minisat.core.SearchParams; |
57 |
|
import org.sat4j.minisat.core.Solver; |
58 |
|
import org.sat4j.minisat.learning.ActiveLearning; |
59 |
|
import org.sat4j.minisat.learning.FixedLengthLearning; |
60 |
|
import org.sat4j.minisat.learning.LimitedLearning; |
61 |
|
import org.sat4j.minisat.learning.MiniSATLearning; |
62 |
|
import org.sat4j.minisat.learning.NoLearningButHeuristics; |
63 |
|
import org.sat4j.minisat.orders.JWOrder; |
64 |
|
import org.sat4j.minisat.orders.MyOrder; |
65 |
|
import org.sat4j.minisat.orders.PureOrder; |
66 |
|
import org.sat4j.minisat.orders.VarOrder; |
67 |
|
import org.sat4j.minisat.orders.VarOrderHeap; |
68 |
|
import org.sat4j.minisat.orders.VarOrderHeapObjective; |
69 |
|
import org.sat4j.minisat.orders.VarOrderHeapRsat; |
70 |
|
import org.sat4j.minisat.restarts.ArminRestarts; |
71 |
|
import org.sat4j.minisat.restarts.LubyRestarts; |
72 |
|
import org.sat4j.minisat.uip.DecisionUIP; |
73 |
|
import org.sat4j.minisat.uip.FirstUIP; |
74 |
|
import org.sat4j.specs.ISolver; |
75 |
|
import org.sat4j.tools.DimacsOutputSolver; |
76 |
|
|
77 |
|
|
78 |
|
|
79 |
|
|
80 |
|
@author |
81 |
|
|
|
|
| 98% |
Uncovered Elements: 6 (294) |
Complexity: 3 |
Complexity Density: 0,33 |
|
82 |
|
public class SolverFactory extends ASolverFactory implements Serializable { |
83 |
|
|
84 |
|
|
85 |
|
|
86 |
|
|
87 |
|
private static final long serialVersionUID = 1L; |
88 |
|
|
89 |
|
|
90 |
|
private static SolverFactory instance; |
91 |
|
|
92 |
|
|
93 |
|
|
94 |
|
|
95 |
|
@see |
96 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
97 |
1
|
private SolverFactory() {... |
98 |
1
|
super(); |
99 |
|
} |
100 |
|
|
|
|
| 75% |
Uncovered Elements: 1 (4) |
Complexity: 2 |
Complexity Density: 1 |
|
101 |
1
|
private static synchronized void createInstance() {... |
102 |
1
|
if (instance == null) { |
103 |
1
|
instance = new SolverFactory(); |
104 |
|
} |
105 |
|
} |
106 |
|
|
107 |
|
|
108 |
|
|
109 |
|
|
110 |
|
@return |
111 |
|
|
|
|
| 80% |
Uncovered Elements: 1 (5) |
Complexity: 2 |
Complexity Density: 0,67 |
|
112 |
1
|
public static SolverFactory instance() {... |
113 |
1
|
if (instance == null) { |
114 |
1
|
createInstance(); |
115 |
|
} |
116 |
1
|
return instance; |
117 |
|
} |
118 |
|
|
119 |
|
|
120 |
|
@return |
121 |
|
|
122 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
123 |
106
|
public static ISolver newMiniLearning() {... |
124 |
106
|
return newMiniLearning(10); |
125 |
|
} |
126 |
|
|
127 |
|
|
128 |
|
@return |
129 |
|
|
130 |
|
|
131 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
132 |
7
|
public static ISolver newMiniLearningHeap() {... |
133 |
7
|
return newMiniLearningHeap(new MixedDataStructureDaniel()); |
134 |
|
} |
135 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (3) |
Complexity: 1 |
Complexity Density: 0,33 |
|
136 |
1
|
public static ISolver newMiniLearningHeapEZSimp() {... |
137 |
1
|
Solver<?> solver = (Solver<?>) newMiniLearningHeap(); |
138 |
1
|
solver.setSimplifier(solver.SIMPLE_SIMPLIFICATION); |
139 |
1
|
return solver; |
140 |
|
} |
141 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (3) |
Complexity: 1 |
Complexity Density: 0,33 |
|
142 |
5
|
public static ISolver newMiniLearningHeapExpSimp() {... |
143 |
5
|
Solver<?> solver = (Solver<?>) newMiniLearningHeap(); |
144 |
5
|
solver.setSimplifier(solver.EXPENSIVE_SIMPLIFICATION); |
145 |
5
|
return solver; |
146 |
|
} |
147 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (3) |
Complexity: 1 |
Complexity Density: 0,33 |
|
148 |
4
|
public static ISolver newMiniLearningHeapRsatExpSimp() {... |
149 |
4
|
Solver<ILits> solver = (Solver<ILits>) newMiniLearningHeapExpSimp(); |
150 |
4
|
solver.setOrder(new VarOrderHeapRsat()); |
151 |
4
|
return solver; |
152 |
|
} |
153 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (4) |
Complexity: 1 |
Complexity Density: 0,25 |
|
154 |
2
|
public static ISolver newMiniLearningHeapRsatExpSimpBiere() {... |
155 |
2
|
Solver<ILits> solver = (Solver<ILits>) newMiniLearningHeapRsatExpSimp(); |
156 |
2
|
solver.setRestartStrategy(new ArminRestarts()); |
157 |
2
|
solver.setSearchParams(new SearchParams(1.1,100)); |
158 |
2
|
return solver; |
159 |
|
} |
160 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (3) |
Complexity: 1 |
Complexity Density: 0,33 |
|
161 |
1
|
public static ISolver newMiniLearningHeapRsatExpSimpLuby() {... |
162 |
1
|
Solver<ILits> solver = (Solver<ILits>) newMiniLearningHeapRsatExpSimp(); |
163 |
1
|
solver.setRestartStrategy(new LubyRestarts()); |
164 |
1
|
return solver; |
165 |
|
} |
166 |
|
|
167 |
|
|
168 |
|
@param |
169 |
|
|
170 |
|
|
171 |
|
@return |
172 |
|
|
173 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
174 |
106
|
public static ISolver newMiniLearning(int n) {... |
175 |
106
|
return newMiniLearning(new MixedDataStructureDaniel(), n); |
176 |
|
} |
177 |
|
|
178 |
|
|
179 |
|
@param |
180 |
|
|
181 |
|
@return |
182 |
|
|
183 |
|
|
184 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
185 |
803
|
public static <L extends ILits> ISolver newMiniLearning(DataStructureFactory<L> dsf) {... |
186 |
803
|
return newMiniLearning(dsf, 10); |
187 |
|
} |
188 |
|
|
189 |
|
|
190 |
|
@param |
191 |
|
|
192 |
|
@return |
193 |
|
|
194 |
|
|
195 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
196 |
8
|
public static <L extends ILits> ISolver newMiniLearningHeap(DataStructureFactory<L> dsf) {... |
197 |
8
|
return newMiniLearning(dsf, new VarOrderHeap<L>()); |
198 |
|
} |
199 |
|
|
200 |
|
|
201 |
|
@return |
202 |
|
|
203 |
|
@see |
204 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
205 |
203
|
public static ISolver newMiniLearning2() {... |
206 |
203
|
return newMiniLearning(new MixedDataStructureWithBinary()); |
207 |
|
} |
208 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
209 |
1
|
public static ISolver newMiniLearning2Heap() {... |
210 |
1
|
return newMiniLearningHeap(new MixedDataStructureWithBinary()); |
211 |
|
} |
212 |
|
|
213 |
|
|
214 |
|
@return |
215 |
|
|
216 |
|
|
217 |
|
@see |
218 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
219 |
1
|
public static ISolver newMiniLearning23() {... |
220 |
1
|
return newMiniLearning(new MixedDataStructureWithBinaryAndTernary()); |
221 |
|
} |
222 |
|
|
223 |
|
|
224 |
|
@return |
225 |
|
|
226 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
227 |
102
|
public static ISolver newMiniLearningCB() {... |
228 |
102
|
return newMiniLearning(new ClausalDataStructureCB()); |
229 |
|
} |
230 |
|
|
231 |
|
|
232 |
|
@return |
233 |
|
|
234 |
|
|
235 |
|
|
236 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
237 |
1
|
public static ISolver newMiniLearningCBWL() {... |
238 |
1
|
return newMiniLearning(new ClausalDataStructureCBWL()); |
239 |
|
} |
240 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
241 |
1
|
public static ISolver newMiniLearning2NewOrder() {... |
242 |
1
|
return newMiniLearning(new MixedDataStructureWithBinary(), |
243 |
|
new MyOrder()); |
244 |
|
} |
245 |
|
|
246 |
|
|
247 |
|
@return |
248 |
|
|
249 |
|
|
250 |
|
|
251 |
|
|
252 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
253 |
1
|
public static ISolver newMiniLearningPure() {... |
254 |
1
|
return newMiniLearning(new MixedDataStructureDaniel(), new PureOrder()); |
255 |
|
} |
256 |
|
|
257 |
|
|
258 |
|
@return |
259 |
|
|
260 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
261 |
1
|
public static ISolver newMiniLearningCBWLPure() {... |
262 |
1
|
return newMiniLearning(new ClausalDataStructureCBWL(), new PureOrder()); |
263 |
|
} |
264 |
|
|
265 |
|
|
266 |
|
@param |
267 |
|
|
268 |
|
|
269 |
|
@param |
270 |
|
|
271 |
|
|
272 |
|
@return |
273 |
|
|
274 |
|
|
275 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (4) |
Complexity: 1 |
Complexity Density: 0,25 |
|
276 |
909
|
public static <L extends ILits> ISolver newMiniLearning(DataStructureFactory<L> dsf, int n) {... |
277 |
909
|
LimitedLearning<L> learning = new LimitedLearning<L>(n); |
278 |
909
|
Solver<L> solver = new Solver<L>(new FirstUIP(), learning, dsf, |
279 |
|
new VarOrder<L>()); |
280 |
909
|
learning.setSolver(solver); |
281 |
909
|
return solver; |
282 |
|
} |
283 |
|
|
284 |
|
|
285 |
|
@param |
286 |
|
|
287 |
|
|
288 |
|
@param |
289 |
|
|
290 |
|
@return |
291 |
|
|
292 |
|
|
293 |
|
|
294 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (4) |
Complexity: 1 |
Complexity Density: 0,25 |
|
295 |
11
|
public static <L extends ILits> ISolver newMiniLearning(DataStructureFactory<L> dsf, IOrder<L> order) {... |
296 |
11
|
LimitedLearning<L> learning = new LimitedLearning<L>(10); |
297 |
11
|
Solver<L> solver = new Solver<L>(new FirstUIP(), learning, dsf, order); |
298 |
11
|
learning.setSolver(solver); |
299 |
11
|
return solver; |
300 |
|
} |
301 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
302 |
1
|
public static ISolver newMiniLearningEZSimp() {... |
303 |
1
|
return newMiniLearningEZSimp(new MixedDataStructureDaniel()); |
304 |
|
} |
305 |
|
|
306 |
|
|
307 |
|
|
308 |
|
|
309 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (5) |
Complexity: 1 |
Complexity Density: 0,2 |
|
310 |
1
|
public static <L extends ILits> ISolver newMiniLearningEZSimp(DataStructureFactory<L> dsf) {... |
311 |
1
|
LimitedLearning<L> learning = new LimitedLearning<L>(10); |
312 |
1
|
Solver<L> solver = new Solver<L>(new FirstUIP(), learning, dsf, |
313 |
|
new VarOrder<L>()); |
314 |
1
|
learning.setSolver(solver); |
315 |
1
|
solver.setSimplifier(solver.SIMPLE_SIMPLIFICATION); |
316 |
1
|
return solver; |
317 |
|
} |
318 |
|
|
319 |
|
|
320 |
|
@return |
321 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (5) |
Complexity: 1 |
Complexity Density: 0,2 |
|
322 |
1
|
public static ISolver newMiniLearningHeapEZSimpNoRestarts() {... |
323 |
1
|
LimitedLearning<ILits> learning = new LimitedLearning<ILits>(10); |
324 |
1
|
Solver<ILits> solver = new Solver<ILits>(new FirstUIP(), learning, |
325 |
|
new MixedDataStructureDaniel(), new SearchParams( |
326 |
|
Integer.MAX_VALUE), new VarOrderHeap<ILits>()); |
327 |
1
|
learning.setSolver(solver); |
328 |
1
|
solver.setSimplifier(solver.SIMPLE_SIMPLIFICATION); |
329 |
1
|
return solver; |
330 |
|
} |
331 |
|
|
332 |
|
|
333 |
|
@return |
334 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (5) |
Complexity: 1 |
Complexity Density: 0,2 |
|
335 |
1
|
public static ISolver newMiniLearningHeapEZSimpLongRestarts() {... |
336 |
1
|
LimitedLearning<ILits> learning = new LimitedLearning<ILits>(10); |
337 |
1
|
Solver<ILits> solver = new Solver<ILits>(new FirstUIP(), learning, |
338 |
|
new MixedDataStructureDaniel(), new SearchParams(1000), |
339 |
|
new VarOrderHeap<ILits>()); |
340 |
1
|
learning.setSolver(solver); |
341 |
1
|
solver.setSimplifier(solver.SIMPLE_SIMPLIFICATION); |
342 |
1
|
return solver; |
343 |
|
} |
344 |
|
|
345 |
|
|
346 |
|
@return |
347 |
|
|
348 |
|
|
349 |
|
|
350 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (5) |
Complexity: 1 |
Complexity Density: 0,2 |
|
351 |
102
|
public static ISolver newActiveLearning() {... |
352 |
102
|
ActiveLearning<ILits> learning = new ActiveLearning<ILits>(); |
353 |
102
|
Solver<ILits> s = new Solver<ILits>(new FirstUIP(), learning, |
354 |
|
new MixedDataStructureDaniel(), new VarOrder<ILits>()); |
355 |
102
|
learning.setOrder(s.getOrder()); |
356 |
102
|
learning.setSolver(s); |
357 |
102
|
return s; |
358 |
|
} |
359 |
|
|
360 |
|
|
361 |
|
@return |
362 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
363 |
104
|
public static ISolver newMiniSAT() {... |
364 |
104
|
return newMiniSAT(new MixedDataStructureDaniel()); |
365 |
|
} |
366 |
|
|
367 |
|
|
368 |
|
@return |
369 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (5) |
Complexity: 1 |
Complexity Density: 0,2 |
|
370 |
1
|
public static ISolver newMiniSATNoRestarts() {... |
371 |
1
|
MiniSATLearning<ILits> learning = new MiniSATLearning<ILits>(); |
372 |
1
|
Solver<ILits> solver = new Solver<ILits>(new FirstUIP(), learning, |
373 |
|
new MixedDataStructureDaniel(), new SearchParams( |
374 |
|
Integer.MAX_VALUE), new VarOrder<ILits>()); |
375 |
1
|
learning.setDataStructureFactory(solver.getDSFactory()); |
376 |
1
|
learning.setVarActivityListener(solver); |
377 |
1
|
return solver; |
378 |
|
|
379 |
|
} |
380 |
|
|
381 |
|
|
382 |
|
@return |
383 |
|
|
384 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
385 |
1
|
public static ISolver newMiniSAT2() {... |
386 |
1
|
return newMiniSAT(new MixedDataStructureWithBinary()); |
387 |
|
} |
388 |
|
|
389 |
|
|
390 |
|
@return |
391 |
|
|
392 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
393 |
1
|
public static ISolver newMiniSAT23() {... |
394 |
1
|
return newMiniSAT(new MixedDataStructureWithBinaryAndTernary()); |
395 |
|
} |
396 |
|
|
397 |
|
|
398 |
|
@param |
399 |
|
|
400 |
|
@return |
401 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (5) |
Complexity: 1 |
Complexity Density: 0,2 |
|
402 |
107
|
public static <L extends ILits> ISolver newMiniSAT(DataStructureFactory<L> dsf) {... |
403 |
107
|
MiniSATLearning<L> learning = new MiniSATLearning<L>(); |
404 |
107
|
Solver<L> solver = new Solver<L>(new FirstUIP(), learning, dsf, |
405 |
|
new VarOrder<L>()); |
406 |
107
|
learning.setDataStructureFactory(solver.getDSFactory()); |
407 |
107
|
learning.setVarActivityListener(solver); |
408 |
107
|
return solver; |
409 |
|
} |
410 |
|
|
411 |
|
|
412 |
|
@return |
413 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
414 |
3
|
public static ISolver newMiniSATHeap() {... |
415 |
3
|
return newMiniSATHeap(new MixedDataStructureDaniel()); |
416 |
|
} |
417 |
|
|
418 |
|
|
419 |
|
@return |
420 |
|
|
421 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (3) |
Complexity: 1 |
Complexity Density: 0,33 |
|
422 |
1
|
public static ISolver newMiniSATHeapEZSimp() {... |
423 |
1
|
Solver<ILits> solver = (Solver<ILits>) newMiniSATHeap(); |
424 |
1
|
solver.setSimplifier(solver.SIMPLE_SIMPLIFICATION); |
425 |
1
|
return solver; |
426 |
|
} |
427 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (3) |
Complexity: 1 |
Complexity Density: 0,33 |
|
428 |
1
|
public static ISolver newMiniSATHeapExpSimp() {... |
429 |
1
|
Solver<ILits> solver = (Solver<ILits>) newMiniSATHeap(); |
430 |
1
|
solver.setSimplifier(solver.EXPENSIVE_SIMPLIFICATION); |
431 |
1
|
return solver; |
432 |
|
} |
433 |
|
|
434 |
|
|
435 |
|
@return |
436 |
|
|
437 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
438 |
1
|
public static ISolver newMiniSAT2Heap() {... |
439 |
1
|
return newMiniSATHeap(new MixedDataStructureWithBinary()); |
440 |
|
} |
441 |
|
|
442 |
|
|
443 |
|
@return |
444 |
|
|
445 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
446 |
1
|
public static ISolver newMiniSAT23Heap() {... |
447 |
1
|
return newMiniSATHeap(new MixedDataStructureWithBinaryAndTernary()); |
448 |
|
} |
449 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (5) |
Complexity: 1 |
Complexity Density: 0,2 |
|
450 |
5
|
public static <L extends ILits> ISolver newMiniSATHeap(DataStructureFactory<L> dsf) {... |
451 |
5
|
MiniSATLearning<L> learning = new MiniSATLearning<L>(); |
452 |
5
|
Solver<L> solver = new Solver<L>(new FirstUIP(), learning, dsf, |
453 |
|
new VarOrderHeap<L>()); |
454 |
5
|
learning.setDataStructureFactory(solver.getDSFactory()); |
455 |
5
|
learning.setVarActivityListener(solver); |
456 |
5
|
return solver; |
457 |
|
} |
458 |
|
|
459 |
|
|
460 |
|
@return |
461 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
462 |
1
|
public static ISolver newMiniCard() {... |
463 |
1
|
return newMiniSAT(new CardinalityDataStructure()); |
464 |
|
} |
465 |
|
|
466 |
|
|
467 |
|
@return |
468 |
|
|
469 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (5) |
Complexity: 1 |
Complexity Density: 0,2 |
|
470 |
157
|
public static ISolver newMinimalOPBMax() {... |
471 |
157
|
MiniSATLearning<ILits> learning = new MiniSATLearning<ILits>(); |
472 |
157
|
Solver<ILits> solver = new Solver<ILits>(new FirstUIP(), learning, |
473 |
|
new PBMaxDataStructure(), new VarOrderHeap<ILits>()); |
474 |
157
|
learning.setDataStructureFactory(solver.getDSFactory()); |
475 |
157
|
learning.setVarActivityListener(solver); |
476 |
157
|
return solver; |
477 |
|
} |
478 |
|
|
479 |
|
|
480 |
|
@return |
481 |
|
|
482 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (5) |
Complexity: 1 |
Complexity Density: 0,2 |
|
483 |
157
|
public static ISolver newMiniOPBMax() {... |
484 |
157
|
MiniSATLearning<ILits> learning = new MiniSATLearning<ILits>(); |
485 |
157
|
Solver<ILits> solver = new PBSolver<ILits>(new FirstUIP(), learning, |
486 |
|
new PBMaxDataStructure(), new VarOrderHeap<ILits>()); |
487 |
157
|
learning.setDataStructureFactory(solver.getDSFactory()); |
488 |
157
|
learning.setVarActivityListener(solver); |
489 |
157
|
return solver; |
490 |
|
} |
491 |
|
|
492 |
|
|
493 |
|
@return |
494 |
|
|
495 |
|
|
496 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (5) |
Complexity: 1 |
Complexity Density: 0,2 |
|
497 |
54
|
public static ISolver newMiniOPBClauseCardConstrMax() {... |
498 |
54
|
MiniSATLearning<ILits> learning = new MiniSATLearning<ILits>(); |
499 |
54
|
Solver<ILits> solver = new PBSolver<ILits>(new FirstUIP(), learning, |
500 |
|
new PBMaxClauseCardConstrDataStructure(), new VarOrderHeap<ILits>()); |
501 |
54
|
learning.setDataStructureFactory(solver.getDSFactory()); |
502 |
54
|
learning.setVarActivityListener(solver); |
503 |
54
|
return solver; |
504 |
|
} |
505 |
|
|
506 |
|
|
507 |
|
@return |
508 |
|
|
509 |
|
|
510 |
|
|
511 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (5) |
Complexity: 1 |
Complexity Density: 0,2 |
|
512 |
1
|
public static ISolver newMiniOPBClauseCardConstrMaxSpecificOrder() {... |
513 |
1
|
MiniSATLearning<ILits> learning = new MiniSATLearning<ILits>(); |
514 |
1
|
Solver<ILits> solver = new PBSolver<ILits>(new FirstUIP(), learning, |
515 |
|
new PBMaxClauseCardConstrDataStructure(), |
516 |
|
new VarOrderHeapObjective()); |
517 |
1
|
learning.setDataStructureFactory(solver.getDSFactory()); |
518 |
1
|
learning.setVarActivityListener(solver); |
519 |
1
|
return solver; |
520 |
|
} |
521 |
|
|
522 |
|
|
523 |
|
@return |
524 |
|
|
525 |
|
|
526 |
|
|
527 |
|
|
528 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (5) |
Complexity: 1 |
Complexity Density: 0,2 |
|
529 |
1
|
public static ISolver newMiniLearningOPBClauseCardConstrMaxSpecificOrderIncremental() {... |
530 |
|
|
531 |
1
|
MiniSATLearning<ILits> learning = new MiniSATLearning<ILits>(); |
532 |
|
|
533 |
1
|
Solver<ILits> solver = new PBSolver<ILits>(new FirstUIP(), learning, |
534 |
|
new PBMaxClauseCardConstrDataStructure(), |
535 |
|
new VarOrderHeapObjective()); |
536 |
1
|
learning.setDataStructureFactory(solver.getDSFactory()); |
537 |
1
|
learning.setVarActivityListener(solver); |
538 |
1
|
return solver; |
539 |
|
} |
540 |
|
|
541 |
|
|
542 |
|
@return |
543 |
|
|
544 |
|
|
545 |
|
|
546 |
|
|
547 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (5) |
Complexity: 1 |
Complexity Density: 0,2 |
|
548 |
1
|
public static ISolver newMiniLearningOPBClauseCardConstrMaxSpecificOrderIncrementalReductionToClause() {... |
549 |
|
|
550 |
1
|
MiniSATLearning<ILits> learning = new MiniSATLearning<ILits>(); |
551 |
|
|
552 |
1
|
Solver<ILits> solver = new PBSolverClause(new FirstUIP(), learning, |
553 |
|
new PBMaxClauseCardConstrDataStructure(), |
554 |
|
new VarOrderHeapObjective()); |
555 |
1
|
learning.setDataStructureFactory(solver.getDSFactory()); |
556 |
1
|
learning.setVarActivityListener(solver); |
557 |
1
|
return solver; |
558 |
|
} |
559 |
|
|
560 |
|
|
561 |
|
@return |
562 |
|
|
563 |
|
|
564 |
|
|
565 |
|
|
566 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (5) |
Complexity: 1 |
Complexity Density: 0,2 |
|
567 |
1
|
public static ISolver newMiniLearningOPBClauseCardConstrMaxSpecificOrderIncrementalNoLearning() {... |
568 |
1
|
NoLearningButHeuristics<ILits> learning = new NoLearningButHeuristics<ILits>(); |
569 |
|
|
570 |
1
|
Solver<ILits> solver = new PBSolver<ILits>(new FirstUIP(), learning, |
571 |
|
new PBMaxClauseCardConstrDataStructure(), |
572 |
|
new VarOrderHeapObjective()); |
573 |
1
|
learning.setSolver(solver); |
574 |
1
|
learning.setVarActivityListener(solver); |
575 |
1
|
return solver; |
576 |
|
} |
577 |
|
|
578 |
|
|
579 |
|
@return |
580 |
|
|
581 |
|
|
582 |
|
|
583 |
|
|
584 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (5) |
Complexity: 1 |
Complexity Density: 0,2 |
|
585 |
1
|
public static ISolver newMiniLearningOPBClauseCardConstrMaxSpecificOrderIncrementalMerging() {... |
586 |
|
|
587 |
1
|
MiniSATLearning<ILits> learning = new MiniSATLearning<ILits>(); |
588 |
|
|
589 |
1
|
Solver<ILits> solver = new PBSolverMerging(new FirstUIP(), learning, |
590 |
|
new PBMaxClauseCardConstrDataStructure(), |
591 |
|
new VarOrderHeapObjective()); |
592 |
1
|
learning.setDataStructureFactory(solver.getDSFactory()); |
593 |
1
|
learning.setVarActivityListener(solver); |
594 |
1
|
return solver; |
595 |
|
} |
596 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (5) |
Complexity: 1 |
Complexity Density: 0,2 |
|
597 |
1
|
public static ISolver newMinimalOPBClauseCardConstrMaxSpecificOrder() {... |
598 |
1
|
MiniSATLearning<ILits> learning = new MiniSATLearning<ILits>(); |
599 |
1
|
Solver<ILits> solver = new Solver<ILits>(new FirstUIP(), learning, |
600 |
|
new PBMaxClauseCardConstrDataStructure(), |
601 |
|
new VarOrderHeapObjective()); |
602 |
1
|
learning.setDataStructureFactory(solver.getDSFactory()); |
603 |
1
|
learning.setVarActivityListener(solver); |
604 |
1
|
return solver; |
605 |
|
} |
606 |
|
|
607 |
|
|
608 |
|
@return |
609 |
|
|
610 |
|
|
611 |
|
|
612 |
|
|
613 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (5) |
Complexity: 1 |
Complexity Density: 0,2 |
|
614 |
54
|
public static ISolver newMiniOPBClauseCardConstrMaxReduceToClause() {... |
615 |
54
|
MiniSATLearning<ILits> learning = new MiniSATLearning<ILits>(); |
616 |
54
|
Solver<ILits> solver = new PBSolverClause(new FirstUIP(), learning, |
617 |
|
new PBMaxClauseCardConstrDataStructure(), new VarOrderHeap<ILits>()); |
618 |
54
|
learning.setDataStructureFactory(solver.getDSFactory()); |
619 |
54
|
learning.setVarActivityListener(solver); |
620 |
54
|
return solver; |
621 |
|
} |
622 |
|
|
623 |
|
|
624 |
|
@return |
625 |
|
|
626 |
|
|
627 |
|
|
628 |
|
|
629 |
|
|
630 |
|
|
631 |
|
|
632 |
|
|
633 |
|
|
634 |
|
|
635 |
|
|
636 |
|
|
637 |
|
|
638 |
|
|
639 |
|
@return |
640 |
|
|
641 |
|
|
642 |
|
|
643 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (5) |
Complexity: 1 |
Complexity Density: 0,2 |
|
644 |
1
|
public static ISolver newMiniOPBClauseCardConstrMaxImplied() {... |
645 |
1
|
MiniSATLearning<ILits> learning = new MiniSATLearning<ILits>(); |
646 |
1
|
Solver<ILits> solver = new PBSolverWithImpliedClause(new FirstUIP(), learning, |
647 |
|
new PBMaxClauseCardConstrDataStructure(), new VarOrderHeap<ILits>()); |
648 |
1
|
learning.setDataStructureFactory(solver.getDSFactory()); |
649 |
1
|
learning.setVarActivityListener(solver); |
650 |
1
|
return solver; |
651 |
|
} |
652 |
|
|
653 |
|
|
654 |
|
@return |
655 |
|
|
656 |
|
|
657 |
|
|
658 |
|
|
659 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (5) |
Complexity: 1 |
Complexity Density: 0,2 |
|
660 |
54
|
public static ISolver newMiniOPBClauseAtLeastConstrMax() {... |
661 |
54
|
MiniSATLearning<ILits> learning = new MiniSATLearning<ILits>(); |
662 |
54
|
Solver<ILits> solver = new PBSolver<ILits>(new FirstUIP(), learning, |
663 |
|
new PBMaxClauseAtLeastConstrDataStructure(), new VarOrderHeap<ILits>()); |
664 |
54
|
learning.setDataStructureFactory(solver.getDSFactory()); |
665 |
54
|
learning.setVarActivityListener(solver); |
666 |
54
|
return solver; |
667 |
|
} |
668 |
|
|
669 |
|
|
670 |
|
@return |
671 |
|
|
672 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (5) |
Complexity: 1 |
Complexity Density: 0,2 |
|
673 |
54
|
public static ISolver newMiniOPBCounterBasedClauseCardConstrMax() {... |
674 |
54
|
MiniSATLearning<ILits> learning = new MiniSATLearning<ILits>(); |
675 |
54
|
Solver<ILits> solver = new PBSolver<ILits>(new FirstUIP(), learning, |
676 |
|
new PBMaxCBClauseCardConstrDataStructure(), new VarOrderHeap<ILits>()); |
677 |
54
|
learning.setDataStructureFactory(solver.getDSFactory()); |
678 |
54
|
learning.setVarActivityListener(solver); |
679 |
54
|
return solver; |
680 |
|
} |
681 |
|
|
682 |
|
|
683 |
|
@return |
684 |
|
|
685 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (5) |
Complexity: 1 |
Complexity Density: 0,2 |
|
686 |
157
|
public static ISolver newMinimalOPBMin() {... |
687 |
157
|
MiniSATLearning<ILits> learning = new MiniSATLearning<ILits>(); |
688 |
157
|
Solver<ILits> solver = new Solver<ILits>(new FirstUIP(), learning, |
689 |
|
new PBMinDataStructure(), new VarOrderHeap<ILits>()); |
690 |
157
|
learning.setDataStructureFactory(solver.getDSFactory()); |
691 |
157
|
learning.setVarActivityListener(solver); |
692 |
157
|
return solver; |
693 |
|
} |
694 |
|
|
695 |
|
|
696 |
|
@return |
697 |
|
|
698 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (5) |
Complexity: 1 |
Complexity Density: 0,2 |
|
699 |
157
|
public static ISolver newMiniOPBMin() {... |
700 |
157
|
MiniSATLearning<ILits> learning = new MiniSATLearning<ILits>(); |
701 |
157
|
Solver<ILits> solver = new PBSolver<ILits>(new FirstUIP(), learning, |
702 |
|
new PBMinDataStructure(), new VarOrderHeap<ILits>()); |
703 |
157
|
learning.setDataStructureFactory(solver.getDSFactory()); |
704 |
157
|
learning.setVarActivityListener(solver); |
705 |
157
|
return solver; |
706 |
|
} |
707 |
|
|
708 |
|
|
709 |
|
@return |
710 |
|
|
711 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (5) |
Complexity: 1 |
Complexity Density: 0,2 |
|
712 |
54
|
public static ISolver newMinimalOPBMinPueblo() {... |
713 |
54
|
MiniSATLearning<ILits> learning = new MiniSATLearning<ILits>(); |
714 |
54
|
Solver<ILits> solver = new Solver<ILits>(new FirstUIP(), learning, |
715 |
|
new PuebloPBMinDataStructure(), new VarOrderHeap<ILits>()); |
716 |
54
|
learning.setDataStructureFactory(solver.getDSFactory()); |
717 |
54
|
learning.setVarActivityListener(solver); |
718 |
54
|
return solver; |
719 |
|
} |
720 |
|
|
721 |
|
|
722 |
|
@return |
723 |
|
|
724 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (5) |
Complexity: 1 |
Complexity Density: 0,2 |
|
725 |
54
|
public static ISolver newMiniOPBMinPueblo() {... |
726 |
54
|
MiniSATLearning<ILits> learning = new MiniSATLearning<ILits>(); |
727 |
54
|
Solver<ILits> solver = new PBSolver<ILits>(new FirstUIP(), learning, |
728 |
|
new PuebloPBMinDataStructure(), new VarOrderHeap<ILits>()); |
729 |
54
|
learning.setDataStructureFactory(solver.getDSFactory()); |
730 |
54
|
learning.setVarActivityListener(solver); |
731 |
54
|
return solver; |
732 |
|
} |
733 |
|
|
734 |
|
|
735 |
|
@return |
736 |
|
|
737 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (5) |
Complexity: 1 |
Complexity Density: 0,2 |
|
738 |
54
|
public static ISolver newMiniOPBClauseCardMinPueblo() {... |
739 |
54
|
MiniSATLearning<ILits> learning = new MiniSATLearning<ILits>(); |
740 |
54
|
Solver<ILits> solver = new PBSolver<ILits>(new FirstUIP(), learning, |
741 |
|
new PuebloPBMinClauseCardConstrDataStructure(), |
742 |
|
new VarOrderHeap<ILits>()); |
743 |
54
|
learning.setDataStructureFactory(solver.getDSFactory()); |
744 |
54
|
learning.setVarActivityListener(solver); |
745 |
54
|
return solver; |
746 |
|
} |
747 |
|
|
748 |
|
|
749 |
|
@return |
750 |
|
|
751 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (5) |
Complexity: 1 |
Complexity Density: 0,2 |
|
752 |
1
|
public static ISolver newMiniOPBClauseCardMin() {... |
753 |
1
|
MiniSATLearning<ILits> learning = new MiniSATLearning<ILits>(); |
754 |
1
|
Solver<ILits> solver = new PBSolver<ILits>(new FirstUIP(), learning, |
755 |
|
new PBMinClauseCardConstrDataStructure(), new VarOrderHeap<ILits>()); |
756 |
1
|
learning.setDataStructureFactory(solver.getDSFactory()); |
757 |
1
|
learning.setVarActivityListener(solver); |
758 |
1
|
return solver; |
759 |
|
} |
760 |
|
|
761 |
|
|
762 |
|
@return |
763 |
|
|
764 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (5) |
Complexity: 1 |
Complexity Density: 0,2 |
|
765 |
54
|
public static ISolver newMiniOPBClauseAtLeastMinPueblo() {... |
766 |
54
|
MiniSATLearning<ILits> learning = new MiniSATLearning<ILits>(); |
767 |
54
|
Solver<ILits> solver = new PBSolver<ILits>(new FirstUIP(), learning, |
768 |
|
new PuebloPBMinClauseAtLeastConstrDataStructure(), |
769 |
|
new VarOrderHeap<ILits>()); |
770 |
54
|
learning.setDataStructureFactory(solver.getDSFactory()); |
771 |
54
|
learning.setVarActivityListener(solver); |
772 |
54
|
return solver; |
773 |
|
} |
774 |
|
|
775 |
|
|
776 |
|
@return |
777 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (5) |
Complexity: 1 |
Complexity Density: 0,2 |
|
778 |
102
|
public static ISolver newRelsat() {... |
779 |
102
|
MiniSATLearning<ILits> learning = new MiniSATLearning<ILits>(); |
780 |
102
|
Solver<ILits> solver = new Solver<ILits>(new DecisionUIP(), learning, |
781 |
|
new MixedDataStructureDaniel(), new VarOrderHeap<ILits>()); |
782 |
102
|
learning.setDataStructureFactory(solver.getDSFactory()); |
783 |
102
|
learning.setVarActivityListener(solver); |
784 |
102
|
return solver; |
785 |
|
} |
786 |
|
|
787 |
|
|
788 |
|
@return |
789 |
|
|
790 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (4) |
Complexity: 1 |
Complexity Density: 0,25 |
|
791 |
102
|
public static ISolver newBackjumping() {... |
792 |
102
|
NoLearningButHeuristics<ILits> learning = new NoLearningButHeuristics<ILits>(); |
793 |
102
|
Solver<ILits> solver = new Solver<ILits>(new FirstUIP(), learning, |
794 |
|
new MixedDataStructureDaniel(), new VarOrderHeap<ILits>()); |
795 |
102
|
learning.setVarActivityListener(solver); |
796 |
102
|
return solver; |
797 |
|
} |
798 |
|
|
799 |
|
|
800 |
|
@return |
801 |
|
|
802 |
|
|
803 |
|
|
804 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (4) |
Complexity: 1 |
Complexity Density: 0,25 |
|
805 |
103
|
public static ISolver newMini3SAT() {... |
806 |
103
|
LimitedLearning<ILits23> learning = new FixedLengthLearning<ILits23>(3); |
807 |
103
|
Solver<ILits23> solver = new Solver<ILits23>(new FirstUIP(), learning, |
808 |
|
new MixedDataStructureWithBinaryAndTernary(), new SearchParams( |
809 |
|
Integer.MAX_VALUE), new JWOrder()); |
810 |
103
|
learning.setSolver(solver); |
811 |
103
|
return solver; |
812 |
|
} |
813 |
|
|
814 |
|
|
815 |
|
@return |
816 |
|
@see |
817 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (5) |
Complexity: 1 |
Complexity Density: 0,2 |
|
818 |
1
|
public static ISolver newMini3SATb() {... |
819 |
1
|
MiniSATLearning<ILits23> learning = new MiniSATLearning<ILits23>(); |
820 |
1
|
Solver<ILits23> solver = new Solver<ILits23>(new FirstUIP(), learning, |
821 |
|
new MixedDataStructureWithBinaryAndTernary(), new SearchParams( |
822 |
|
Integer.MAX_VALUE), new JWOrder()); |
823 |
1
|
learning.setDataStructureFactory(solver.getDSFactory()); |
824 |
1
|
learning.setVarActivityListener(solver); |
825 |
1
|
return solver; |
826 |
|
} |
827 |
|
|
828 |
|
|
829 |
|
|
830 |
|
|
831 |
|
|
832 |
|
@return |
833 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (5) |
Complexity: 1 |
Complexity Density: 0,2 |
|
834 |
1
|
public static ISolver newMiniMaxSAT() {... |
835 |
1
|
MiniSATLearning<ILits> learning = new MiniSATLearning<ILits>(); |
836 |
1
|
Solver<ILits> solver = new Solver<ILits>(new FirstUIP(), learning, |
837 |
|
new MixedDataStructureDanielCBWL(), new SearchParams(1.2, |
838 |
|
100000), new VarOrderHeap<ILits>()); |
839 |
1
|
learning.setDataStructureFactory(solver.getDSFactory()); |
840 |
1
|
learning.setVarActivityListener(solver); |
841 |
1
|
return solver; |
842 |
|
} |
843 |
|
|
844 |
|
|
845 |
|
|
846 |
|
|
847 |
|
|
848 |
|
@return |
849 |
|
@see |
850 |
|
|
851 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
852 |
1
|
public static ISolver newDefault() {... |
853 |
1
|
return newMiniLearningHeapRsatExpSimpBiere(); |
854 |
|
} |
855 |
|
|
|
|
| 0% |
Uncovered Elements: 1 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
856 |
0
|
@Override... |
857 |
|
public ISolver defaultSolver() { |
858 |
0
|
return newDefault(); |
859 |
|
} |
860 |
|
|
861 |
|
|
862 |
|
|
863 |
|
|
864 |
|
@return |
865 |
|
@see |
866 |
|
|
867 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
868 |
1
|
public static ISolver newLight() {... |
869 |
1
|
return newMini3SAT(); |
870 |
|
} |
871 |
|
|
|
|
| 0% |
Uncovered Elements: 1 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
872 |
0
|
@Override... |
873 |
|
public ISolver lightSolver() { |
874 |
0
|
return newLight(); |
875 |
|
} |
876 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
877 |
1
|
public static ISolver newDimacsOutput() {... |
878 |
1
|
return new DimacsOutputSolver(); |
879 |
|
} |
880 |
|
|
881 |
|
} |