Clover Coverage Report
Coverage timestamp: mer. juin 27 2007 07:27:16 CEST
Overview   Package   File
    FRAMES   NO FRAMES     
220   881   3   3,14
4   462   0,33   70
70     1,03  
1    
 
  SolverFactory       Line # 82 220 3 98% 0.97959185
 
  (5)
 
1    /*
2    * SAT4J: a SATisfiability library for Java Copyright (C) 2004-2006 Daniel Le
3    * Berre
4    *
5    * Based on the original minisat specification from:
6    *
7    * An extensible SAT solver. Niklas E?n and Niklas S?rensson. Proceedings of the
8    * Sixth International Conference on Theory and Applications of Satisfiability
9    * Testing, LNCS 2919, pp 502-518, 2003.
10    *
11    * This library is free software; you can redistribute it and/or modify it under
12    * the terms of the GNU Lesser General Public License as published by the Free
13    * Software Foundation; either version 2.1 of the License, or (at your option)
14    * any later version.
15    *
16    * This library is distributed in the hope that it will be useful, but WITHOUT
17    * ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS
18    * FOR A PARTICULAR PURPOSE. See the GNU Lesser General Public License for more
19    * details.
20    *
21    * You should have received a copy of the GNU Lesser General Public License
22    * along with this library; if not, write to the Free Software Foundation, Inc.,
23    * 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
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    * User friendly access to pre-constructed solvers.
79    *
80    * @author leberre
81    */
 
82    public class SolverFactory extends ASolverFactory implements Serializable {
83   
84    /**
85    *
86    */
87    private static final long serialVersionUID = 1L;
88   
89    // thread safe implementation of the singleton design pattern
90    private static SolverFactory instance;
91   
92    /**
93    * Private contructor. Use singleton method instance() instead.
94    *
95    * @see #instance()
96    */
 
97  1 toggle private SolverFactory() {
98  1 super();
99    }
100   
 
101  1 toggle private static synchronized void createInstance() {
102  1 if (instance == null) {
103  1 instance = new SolverFactory();
104    }
105    }
106   
107    /**
108    * Access to the single instance of the factory.
109    *
110    * @return the singleton of that class.
111    */
 
112  1 toggle public static SolverFactory instance() {
113  1 if (instance == null) {
114  1 createInstance();
115    }
116  1 return instance;
117    }
118   
119    /**
120    * @return a "default" "minilearning" solver learning clauses of size
121    * smaller than 10 % of the total number of variables
122    */
 
123  106 toggle public static ISolver newMiniLearning() {
124  106 return newMiniLearning(10);
125    }
126   
127    /**
128    * @return a "default" "minilearning" solver learning clauses of size
129    * smaller than 10 % of the total number of variables with a heap
130    * based var order.
131    */
 
132  7 toggle public static ISolver newMiniLearningHeap() {
133  7 return newMiniLearningHeap(new MixedDataStructureDaniel());
134    }
135   
 
136  1 toggle public static ISolver newMiniLearningHeapEZSimp() {
137  1 Solver<?> solver = (Solver<?>) newMiniLearningHeap();
138  1 solver.setSimplifier(solver.SIMPLE_SIMPLIFICATION);
139  1 return solver;
140    }
141   
 
142  5 toggle public static ISolver newMiniLearningHeapExpSimp() {
143  5 Solver<?> solver = (Solver<?>) newMiniLearningHeap();
144  5 solver.setSimplifier(solver.EXPENSIVE_SIMPLIFICATION);
145  5 return solver;
146    }
147   
 
148  4 toggle public static ISolver newMiniLearningHeapRsatExpSimp() {
149  4 Solver<ILits> solver = (Solver<ILits>) newMiniLearningHeapExpSimp();
150  4 solver.setOrder(new VarOrderHeapRsat());
151  4 return solver;
152    }
153   
 
154  2 toggle 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   
 
161  1 toggle 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 n
169    * the maximal size of the clauses to learn as a percentage of
170    * the initial number of variables
171    * @return a "minilearning" solver learning clauses of size smaller than n
172    * of the total number of variables
173    */
 
174  106 toggle public static ISolver newMiniLearning(int n) {
175  106 return newMiniLearning(new MixedDataStructureDaniel(), n);
176    }
177   
178    /**
179    * @param dsf
180    * a specific data structure factory
181    * @return a default "minilearning" solver using a specific data structure
182    * factory, learning clauses of length smaller or equals to 10 % of
183    * the number of variables.
184    */
 
185  803 toggle public static <L extends ILits> ISolver newMiniLearning(DataStructureFactory<L> dsf) {
186  803 return newMiniLearning(dsf, 10);
187    }
188   
189    /**
190    * @param dsf
191    * a specific data structure factory
192    * @return a default "minilearning" solver using a specific data structure
193    * factory, learning clauses of length smaller or equals to 10 % of
194    * the number of variables and a heap based VSIDS heuristics
195    */
 
196  8 toggle public static <L extends ILits> ISolver newMiniLearningHeap(DataStructureFactory<L> dsf) {
197  8 return newMiniLearning(dsf, new VarOrderHeap<L>());
198    }
199   
200    /**
201    * @return a default minilearning solver using a specific data structure
202    * described in Lawrence Ryan thesis to handle binary clauses.
203    * @see #newMiniLearning
204    */
 
205  203 toggle public static ISolver newMiniLearning2() {
206  203 return newMiniLearning(new MixedDataStructureWithBinary());
207    }
208   
 
209  1 toggle public static ISolver newMiniLearning2Heap() {
210  1 return newMiniLearningHeap(new MixedDataStructureWithBinary());
211    }
212   
213    /**
214    * @return a default minilearning solver using a specific data structures
215    * described in Lawrence Ryan thesis to handle binary and ternary
216    * clauses.
217    * @see #newMiniLearning
218    */
 
219  1 toggle public static ISolver newMiniLearning23() {
220  1 return newMiniLearning(new MixedDataStructureWithBinaryAndTernary());
221    }
222   
223    /**
224    * @return a default minilearning SAT solver using counter-based clause
225    * representation (i.e. all the literals of a clause are watched)
226    */
 
227  102 toggle public static ISolver newMiniLearningCB() {
228  102 return newMiniLearning(new ClausalDataStructureCB());
229    }
230   
231    /**
232    * @return a default minilearning SAT solver using counter-based clause
233    * representation (i.e. all the literals of a clause are watched)
234    * for the ORIGINAL clauses and watched-literals clause
235    * representation for learnt clauses.
236    */
 
237  1 toggle public static ISolver newMiniLearningCBWL() {
238  1 return newMiniLearning(new ClausalDataStructureCBWL());
239    }
240   
 
241  1 toggle public static ISolver newMiniLearning2NewOrder() {
242  1 return newMiniLearning(new MixedDataStructureWithBinary(),
243    new MyOrder());
244    }
245   
246    /**
247    * @return a default minilearning SAT solver choosing periodically to branch
248    * on "pure watched" literals if any. (a pure watched literal l is a
249    * literal that is watched on at least one clause such that its
250    * negation is not watched at all. It is not necessarily a watched
251    * literal.)
252    */
 
253  1 toggle public static ISolver newMiniLearningPure() {
254  1 return newMiniLearning(new MixedDataStructureDaniel(), new PureOrder());
255    }
256   
257    /**
258    * @return a default minilearning SAT solver choosing periodically to branch
259    * on literal "pure in the original set of clauses" if any.
260    */
 
261  1 toggle public static ISolver newMiniLearningCBWLPure() {
262  1 return newMiniLearning(new ClausalDataStructureCBWL(), new PureOrder());
263    }
264   
265    /**
266    * @param dsf
267    * the data structure factory used to represent literals and
268    * clauses
269    * @param n
270    * the maximum size of learnt clauses as percentage of the
271    * original number of variables.
272    * @return a SAT solver with learning limited to clauses of length smaller
273    * or equal to n, the dsf data structure, the FirstUIP clause
274    * generator and a sort of VSIDS heuristics.
275    */
 
276  909 toggle 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 dsf
286    * the data structure factory used to represent literals and
287    * clauses
288    * @param order
289    * the heuristics
290    * @return a SAT solver with learning limited to clauses of length smaller
291    * or equal to 10 percent of the total number of variables, the dsf
292    * data structure, the FirstUIP clause generator and order as
293    * heuristics.
294    */
 
295  11 toggle 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   
 
302  1 toggle public static ISolver newMiniLearningEZSimp() {
303  1 return newMiniLearningEZSimp(new MixedDataStructureDaniel());
304    }
305   
306    // public static ISolver newMiniLearning2EZSimp() {
307    // return newMiniLearningEZSimp(new MixedDataStructureWithBinary());
308    // }
309   
 
310  1 toggle 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 a default MiniLearning without restarts.
321    */
 
322  1 toggle 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 a default MiniLearning with restarts beginning at 1000 conflicts.
334    */
 
335  1 toggle 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 a SAT solver using First UIP clause generator, watched literals,
347    * VSIDS like heuristics learning only clauses having a great number
348    * of active variables, i.e. variables with an activity strictly
349    * greater than one.
350    */
 
351  102 toggle 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 a SAT solver very close to the original MiniSAT sat solver.
362    */
 
363  104 toggle public static ISolver newMiniSAT() {
364  104 return newMiniSAT(new MixedDataStructureDaniel());
365    }
366   
367    /**
368    * @return MiniSAT without restarts.
369    */
 
370  1 toggle 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 MiniSAT with a special data structure from Lawrence Ryan thesis
383    * for managing binary clauses.
384    */
 
385  1 toggle public static ISolver newMiniSAT2() {
386  1 return newMiniSAT(new MixedDataStructureWithBinary());
387    }
388   
389    /**
390    * @return MiniSAT with a special data structure from Lawrence Ryan thesis
391    * for managing binary and ternary clauses.
392    */
 
393  1 toggle public static ISolver newMiniSAT23() {
394  1 return newMiniSAT(new MixedDataStructureWithBinaryAndTernary());
395    }
396   
397    /**
398    * @param dsf
399    * the data structure used for representing clauses and lits
400    * @return MiniSAT the data structure dsf.
401    */
 
402  107 toggle 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 a SAT solver very close to the original MiniSAT sat solver.
413    */
 
414  3 toggle public static ISolver newMiniSATHeap() {
415  3 return newMiniSATHeap(new MixedDataStructureDaniel());
416    }
417   
418    /**
419    * @return a SAT solver very close to the original MiniSAT sat solver
420    * including easy reason simplification.
421    */
 
422  1 toggle 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   
 
428  1 toggle 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 MiniSAT with a special data structure from Lawrence Ryan thesis
436    * for managing binary clauses.
437    */
 
438  1 toggle public static ISolver newMiniSAT2Heap() {
439  1 return newMiniSATHeap(new MixedDataStructureWithBinary());
440    }
441   
442    /**
443    * @return MiniSAT with a special data structure from Lawrence Ryan thesis
444    * for managing binary and ternary clauses.
445    */
 
446  1 toggle public static ISolver newMiniSAT23Heap() {
447  1 return newMiniSATHeap(new MixedDataStructureWithBinaryAndTernary());
448    }
449   
 
450  5 toggle 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 MiniSAT with data structures to handle cardinality constraints.
461    */
 
462  1 toggle public static ISolver newMiniCard() {
463  1 return newMiniSAT(new CardinalityDataStructure());
464    }
465   
466    /**
467    * @return MiniSAT with Counter-based pseudo boolean constraints and clause
468    * learning.
469    */
 
470  157 toggle 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 MiniSAT with Counter-based pseudo boolean constraints and
481    * constraint learning.
482    */
 
483  157 toggle 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 MiniSAT with Counter-based pseudo boolean constraints and
494    * constraint learning. Clauses and cardinalities with watched
495    * literals are also handled (and learnt).
496    */
 
497  54 toggle 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 MiniSAT with Counter-based pseudo boolean constraints and
508    * constraint learning. Clauses and cardinalities with watched
509    * literals are also handled (and learnt). A specific heuristics
510    * taking into account the objective value is used.
511    */
 
512  1 toggle 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 MiniLearning with Counter-based pseudo boolean constraints and
524    * constraint learning. Clauses and cardinalities with watched
525    * literals are also handled (and learnt). A specific heuristics
526    * taking into account the objective value is used.
527    * Conflict analysis with full cutting plane inference.
528    */
 
529  1 toggle public static ISolver newMiniLearningOPBClauseCardConstrMaxSpecificOrderIncremental() {
530    // LimitedLearning learning = new LimitedLearning(10);
531  1 MiniSATLearning<ILits> learning = new MiniSATLearning<ILits>();
532    // LearningStrategy learning = new NoLearningButHeuristics();
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 MiniLearning with Counter-based pseudo boolean constraints and
543    * constraint learning. Clauses and cardinalities with watched
544    * literals are also handled (and learnt). A specific heuristics
545    * taking into account the objective value is used.
546    * Conflict analysis reduces to clauses to avoid computations
547    */
 
548  1 toggle public static ISolver newMiniLearningOPBClauseCardConstrMaxSpecificOrderIncrementalReductionToClause() {
549    // LimitedLearning learning = new LimitedLearning(10);
550  1 MiniSATLearning<ILits> learning = new MiniSATLearning<ILits>();
551    // LearningStrategy learning = new NoLearningButHeuristics();
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 MiniLearning with Counter-based pseudo boolean constraints and
562    * constraint learning. Clauses and cardinalities with watched
563    * literals are also handled (and learnt). A specific heuristics
564    * taking into account the objective value is used.
565    * The PB constraints are not learnt (watched), just used for backjumping.
566    */
 
567  1 toggle public static ISolver newMiniLearningOPBClauseCardConstrMaxSpecificOrderIncrementalNoLearning() {
568  1 NoLearningButHeuristics<ILits> learning = new NoLearningButHeuristics<ILits>();
569    // SearchParams params = new SearchParams(1.1,100);
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 MiniLearning with Counter-based pseudo boolean constraints and
580    * constraint learning. Clauses and cardinalities with watched
581    * literals are also handled (and learnt). A specific heuristics
582    * taking into account the objective value is used.
583    * Conflict analysis uses fusion rule
584    */
 
585  1 toggle public static ISolver newMiniLearningOPBClauseCardConstrMaxSpecificOrderIncrementalMerging() {
586    // LimitedLearning learning = new LimitedLearning(10);
587  1 MiniSATLearning<ILits> learning = new MiniSATLearning<ILits>();
588    // LearningStrategy learning = new NoLearningButHeuristics();
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   
 
597  1 toggle 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 MiniSAT with Counter-based pseudo boolean constraints and
609    * constraint learning. Clauses and cardinalities with watched
610    * literals are also handled (and learnt). A reduction of
611    * PB-constraints to clauses is made in order to simplify cutting
612    * planes.
613    */
 
614  54 toggle 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 MiniSAT with Counter-based pseudo boolean constraints and
625    * constraint learning. Clauses and cardinalities with watched
626    * literals are also handled (and learnt). A reduction of
627    * PB-constraints to cardinalities is made in order to simplify
628    * cutting planes.
629    */
630    // public static ISolver newMiniOPBClauseCardConstrMaxReduceToCard() {
631    // MiniSATLearning learning = new MiniSATLearning();
632    // Solver solver = new PBSolverCard(new FirstUIP(), learning,
633    // new PBMaxClauseCardConstrDataStructure(), new VarOrderHeap());
634    // learning.setDataStructureFactory(solver.getDSFactory());
635    // learning.setVarActivityListener(solver);
636    // return solver;
637    // }
638    /**
639    * @return MiniSAT with Counter-based pseudo boolean constraints and
640    * constraint learning. Clauses and cardinalities with watched
641    * literals are also handled (and learnt). a pre-processing is
642    * applied which adds implied clauses from PB-constraints.
643    */
 
644  1 toggle 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 MiniSAT with Counter-based pseudo boolean constraints,
655    * counter-based cardinalities, watched clauses and constraint
656    * learning. methods isAssertive() and getBacktrackLevel() are
657    * totally incremental. Conflicts for PB-constraints use a Map
658    * structure
659    */
 
660  54 toggle 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 MiniSAT with Counter-based pseudo boolean constraints and
671    * clauses, watched cardinalities, and constraint learning.
672    */
 
673  54 toggle 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 MiniSAT with WL-based pseudo boolean constraints and clause
684    * learning.
685    */
 
686  157 toggle 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 MiniSAT with WL-based pseudo boolean constraints and constraint
697    * learning.
698    */
 
699  157 toggle 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 MiniSAT with WL-based pseudo boolean constraints and clause
710    * learning.
711    */
 
712  54 toggle 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 MiniSAT with WL-based pseudo boolean constraints and constraint
723    * learning.
724    */
 
725  54 toggle 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 MiniSAT with WL-based pseudo boolean constraints and clauses,
736    * cardinalities, and constraint learning.
737    */
 
738  54 toggle 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 MiniSAT with WL-based pseudo boolean constraints and clauses,
750    * cardinalities, and constraint learning.
751    */
 
752  1 toggle 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 MiniSAT with WL-based pseudo boolean constraints and clauses,
763    * counter-based cardinalities, and constraint learning.
764    */
 
765  54 toggle 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 MiniSAT with decision UIP clause generator.
777    */
 
778  102 toggle 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 MiniSAT with VSIDS heuristics, FirstUIP clause generator for
789    * backjumping but no learning.
790    */
 
791  102 toggle 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 a SAT solver with learning limited to clauses of length smaller
801    * or equals to 3, with a specific data structure for binary and
802    * ternary clauses as found in Lawrence Ryan thesis, without
803    * restarts, with a Jeroslow/Wang kind of heuristics.
804    */
 
805  103 toggle 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 a Mini3SAT with full learning.
816    * @see #newMini3SAT()
817    */
 
818  1 toggle 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    * Builds a SAT solver for the MAX sat evaluation. Full clause learning, no
830    * restarts,
831    *
832    * @return a
833    */
 
834  1 toggle 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    * Default solver of the SolverFactory. This solver is meant to be used on
846    * challenging SAT benchmarks.
847    *
848    * @return the best "general purpose" SAT solver available in the factory.
849    * @see #defaultSolver() the same method, polymorphic, to be called from an
850    * instance of ASolverFactory.
851    */
 
852  1 toggle public static ISolver newDefault() {
853  1 return newMiniLearningHeapRsatExpSimpBiere();
854    }
855   
 
856  0 toggle @Override
857    public ISolver defaultSolver() {
858  0 return newDefault();
859    }
860   
861    /**
862    * Small footprint SAT solver.
863    *
864    * @return a SAT solver suitable for solving small/easy SAT benchmarks.
865    * @see #lightSolver() the same method, polymorphic, to be called from an
866    * instance of ASolverFactory.
867    */
 
868  1 toggle public static ISolver newLight() {
869  1 return newMini3SAT();
870    }
871   
 
872  0 toggle @Override
873    public ISolver lightSolver() {
874  0 return newLight();
875    }
876   
 
877  1 toggle public static ISolver newDimacsOutput() {
878  1 return new DimacsOutputSolver();
879    }
880   
881    }
 
CloverReport generated by Clover Code Coverage v2.0a5
mer. juin 27 2007 07:27:33 CEST.		   Beta Testers License registered to clover-support@cenqua.com. This license of Clover2 is provided for beta testing only. You have 5 day(s) before your Beta Tester License expires.