Clover coverage report -
Coverage timestamp: jeu. juin 15 2006 08:24:33 CEST
Overview   Package   File
    FRAMES   NO FRAMES  
file stats: LOC: 741   Methods: 59
NCLOC: 381   Classes: 1
 
 Source file Conditionals Statements Methods TOTAL
SolverFactory.java 50% 98,9% 96,6% 97,9%
coverage coverage
 1    /*
 2    * SAT4J: a SATisfiability library for Java Copyright (C) 2004 Daniel Le Berre
 3    *
 4    * Based on the original minisat specification from:
 5    *
 6    * An extensible SAT solver. Niklas E?n and Niklas S?rensson. Proceedings of the
 7    * Sixth International Conference on Theory and Applications of Satisfiability
 8    * Testing, LNCS 2919, pp 502-518, 2003.
 9    *
 10    * This library is free software; you can redistribute it and/or modify it under
 11    * the terms of the GNU Lesser General Public License as published by the Free
 12    * Software Foundation; either version 2.1 of the License, or (at your option)
 13    * any later version.
 14    *
 15    * This library is distributed in the hope that it will be useful, but WITHOUT
 16    * ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS
 17    * FOR A PARTICULAR PURPOSE. See the GNU Lesser General Public License for more
 18    * details.
 19    *
 20    * You should have received a copy of the GNU Lesser General Public License
 21    * along with this library; if not, write to the Free Software Foundation, Inc.,
 22    * 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
 23    *
 24    */
 25    package org.sat4j.minisat;
 26   
 27    import java.io.Serializable;
 28   
 29    import org.sat4j.core.ASolverFactory;
 30    import org.sat4j.minisat.constraints.CardinalityDataStructure;
 31    import org.sat4j.minisat.constraints.ClausalDataStructureCB;
 32    import org.sat4j.minisat.constraints.ClausalDataStructureCBWL;
 33    import org.sat4j.minisat.constraints.MixedDataStructureDaniel;
 34    import org.sat4j.minisat.constraints.MixedDataStructureWithBinary;
 35    import org.sat4j.minisat.constraints.MixedDataStructureWithBinaryAndTernary;
 36    import org.sat4j.minisat.constraints.PBMaxCBClauseCardConstrDataStructure;
 37    import org.sat4j.minisat.constraints.PBMaxClauseAtLeastConstrDataStructure;
 38    import org.sat4j.minisat.constraints.PBMaxClauseCardConstrDataStructure;
 39    import org.sat4j.minisat.constraints.PBMaxDataStructure;
 40    import org.sat4j.minisat.constraints.PBMinClauseCardConstrDataStructure;
 41    import org.sat4j.minisat.constraints.PBMinDataStructure;
 42    import org.sat4j.minisat.constraints.PuebloPBMinClauseAtLeastConstrDataStructure;
 43    import org.sat4j.minisat.constraints.PuebloPBMinClauseCardConstrDataStructure;
 44    import org.sat4j.minisat.constraints.PuebloPBMinDataStructure;
 45    import org.sat4j.minisat.constraints.pb.PBSolver;
 46    import org.sat4j.minisat.constraints.pb.PBSolverCard;
 47    import org.sat4j.minisat.constraints.pb.PBSolverClause;
 48    import org.sat4j.minisat.constraints.pb.PBSolverWithImpliedClause;
 49    import org.sat4j.minisat.core.DataStructureFactory;
 50    import org.sat4j.minisat.core.IOrder;
 51    import org.sat4j.minisat.core.SearchParams;
 52    import org.sat4j.minisat.core.Solver;
 53    import org.sat4j.minisat.learning.ActiveLearning;
 54    import org.sat4j.minisat.learning.FixedLengthLearning;
 55    import org.sat4j.minisat.learning.LimitedLearning;
 56    import org.sat4j.minisat.learning.MiniSATLearning;
 57    import org.sat4j.minisat.learning.NoLearningButHeuristics;
 58    import org.sat4j.minisat.orders.JWOrder;
 59    import org.sat4j.minisat.orders.MyOrder;
 60    import org.sat4j.minisat.orders.PureOrder;
 61    import org.sat4j.minisat.orders.VarOrder;
 62    import org.sat4j.minisat.orders.VarOrderHeap;
 63    import org.sat4j.minisat.orders.VarOrderHeapObjective;
 64    import org.sat4j.minisat.uip.DecisionUIP;
 65    import org.sat4j.minisat.uip.FirstUIP;
 66    import org.sat4j.specs.ISolver;
 67    import org.sat4j.tools.SATRaceDecorator;
 68   
 69    /**
 70    * User friendly access to pre-constructed solvers.
 71    *
 72    * @author leberre
 73    */
 74    public class SolverFactory extends ASolverFactory implements Serializable {
 75   
 76    /**
 77    *
 78    */
 79    private static final long serialVersionUID = 1L;
 80   
 81    // thread safe implementation of the singleton design pattern
 82    private static SolverFactory instance;
 83   
 84    /**
 85    * Private contructor. Use singleton method instance() instead.
 86    *
 87    * @see #instance()
 88    */
 89  1 private SolverFactory() {
 90  1 super();
 91    }
 92   
 93    /**
 94    * Access to the single instance of the factory.
 95    *
 96    * @return the singleton for that class.
 97    */
 98  1 public static synchronized SolverFactory instance() {
 99  1 if (instance == null) {
 100  1 instance = new SolverFactory();
 101    }
 102  1 return instance;
 103    }
 104   
 105    /**
 106    * @return a "default" "minilearning" solver learning clauses of size
 107    * smaller than 10 % of the total number of variables
 108    */
 109  106 public static ISolver newMiniLearning() {
 110  106 return newMiniLearning(10);
 111    }
 112   
 113    /**
 114    * @return a "default" "minilearning" solver learning clauses of size
 115    * smaller than 10 % of the total number of variables with a heap
 116    * based var order.
 117    */
 118  4 public static ISolver newMiniLearningHeap() {
 119  4 return newMiniLearningHeap(new MixedDataStructureDaniel());
 120    }
 121   
 122  3 public static ISolver newMiniLearningHeapEZSimp() {
 123  3 Solver solver = (Solver) newMiniLearningHeap();
 124  3 solver.setSimplifier(solver.SIMPLE_SIMPLIFICATION);
 125  3 return solver;
 126    }
 127   
 128    /**
 129    * @param n
 130    * the maximal size of the clauses to learn as a percentage of
 131    * the initial number of variables
 132    * @return a "minilearning" solver learning clauses of size smaller than n
 133    * of the total number of variables
 134    */
 135  106 public static ISolver newMiniLearning(int n) {
 136  106 return newMiniLearning(new MixedDataStructureDaniel(), n);
 137    }
 138   
 139    /**
 140    * @param dsf
 141    * a specific data structure factory
 142    * @return a default "minilearning" solver using a specific data structure
 143    * factory, learning clauses of length smaller or equals to 10 % of
 144    * the number of variables.
 145    */
 146  803 public static ISolver newMiniLearning(DataStructureFactory dsf) {
 147  803 return newMiniLearning(dsf, 10);
 148    }
 149   
 150    /**
 151    * @param dsf
 152    * a specific data structure factory
 153    * @return a default "minilearning" solver using a specific data structure
 154    * factory, learning clauses of length smaller or equals to 10 % of
 155    * the number of variables and a heap based VSIDS heuristics
 156    */
 157  5 public static ISolver newMiniLearningHeap(DataStructureFactory dsf) {
 158  5 return newMiniLearning(dsf, new VarOrderHeap());
 159    }
 160   
 161    /**
 162    * @return a default minilearning solver using a specific data structure
 163    * described in Lawrence Ryan thesis to handle binary clauses.
 164    * @see #newMiniLearning
 165    */
 166  203 public static ISolver newMiniLearning2() {
 167  203 return newMiniLearning(new MixedDataStructureWithBinary());
 168    }
 169   
 170  1 public static ISolver newMiniLearning2Heap() {
 171  1 return newMiniLearningHeap(new MixedDataStructureWithBinary());
 172    }
 173   
 174    /**
 175    * @return a default minilearning solver using a specific data structures
 176    * described in Lawrence Ryan thesis to handle binary and ternary
 177    * clauses.
 178    * @see #newMiniLearning
 179    */
 180  1 public static ISolver newMiniLearning23() {
 181  1 return newMiniLearning(new MixedDataStructureWithBinaryAndTernary());
 182    }
 183   
 184    /**
 185    * @return a default minilearning SAT solver using counter-based clause
 186    * representation (i.e. all the literals of a clause are watched)
 187    */
 188  102 public static ISolver newMiniLearningCB() {
 189  102 return newMiniLearning(new ClausalDataStructureCB());
 190    }
 191   
 192    /**
 193    * @return a default minilearning SAT solver using counter-based clause
 194    * representation (i.e. all the literals of a clause are watched)
 195    * for the ORIGINAL clauses and watched-literals clause
 196    * representation for learnt clauses.
 197    */
 198  1 public static ISolver newMiniLearningCBWL() {
 199  1 return newMiniLearning(new ClausalDataStructureCBWL());
 200    }
 201   
 202  1 public static ISolver newMiniLearning2NewOrder() {
 203  1 return newMiniLearning(new MixedDataStructureWithBinary(),
 204    new MyOrder());
 205    }
 206   
 207    /**
 208    * @return a default minilearning SAT solver choosing periodically to branch
 209    * on "pure watched" literals if any. (a pure watched literal l is a
 210    * literal that is watched on at least one clause such that its
 211    * negation is not watched at all. It is not necessarily a watched
 212    * literal.)
 213    */
 214  1 public static ISolver newMiniLearningPure() {
 215  1 return newMiniLearning(new MixedDataStructureDaniel(), new PureOrder());
 216    }
 217   
 218    /**
 219    * @return a default minilearning SAT solver choosing periodically to branch
 220    * on literal "pure in the original set of clauses" if any.
 221    */
 222  1 public static ISolver newMiniLearningCBWLPure() {
 223  1 return newMiniLearning(new ClausalDataStructureCBWL(), new PureOrder());
 224    }
 225   
 226    /**
 227    * @param dsf
 228    * the data structure factory used to represent literals and
 229    * clauses
 230    * @param n
 231    * the maximum size of learnt clauses as percentage of the
 232    * original number of variables.
 233    * @return a SAT solver with learning limited to clauses of length smaller
 234    * or equal to n, the dsf data structure, the FirstUIP clause
 235    * generator and a sort of VSIDS heuristics.
 236    */
 237  909 public static ISolver newMiniLearning(DataStructureFactory dsf, int n) {
 238  909 LimitedLearning learning = new LimitedLearning(n);
 239  909 Solver solver = new Solver(new FirstUIP(), learning, dsf,
 240    new VarOrder());
 241  909 learning.setSolver(solver);
 242  909 return solver;
 243    }
 244   
 245    /**
 246    * @param dsf
 247    * the data structure factory used to represent literals and
 248    * clauses
 249    * @param order
 250    * the heuristics
 251    * @return a SAT solver with learning limited to clauses of length smaller
 252    * or equal to 10 percent of the total number of variables, the dsf
 253    * data structure, the FirstUIP clause generator and order as
 254    * heuristics.
 255    */
 256  8 public static ISolver newMiniLearning(DataStructureFactory dsf, IOrder order) {
 257  8 LimitedLearning learning = new LimitedLearning(10);
 258  8 Solver solver = new Solver(new FirstUIP(), learning, dsf, order);
 259  8 learning.setSolver(solver);
 260  8 return solver;
 261    }
 262   
 263  1 public static ISolver newMiniLearningEZSimp() {
 264  1 return newMiniLearningEZSimp(new MixedDataStructureDaniel());
 265    }
 266   
 267    // public static ISolver newMiniLearning2EZSimp() {
 268    // return newMiniLearningEZSimp(new MixedDataStructureWithBinary());
 269    // }
 270   
 271  1 public static ISolver newMiniLearningEZSimp(DataStructureFactory dsf) {
 272  1 LimitedLearning learning = new LimitedLearning(10);
 273  1 Solver solver = new Solver(new FirstUIP(), learning, dsf,
 274    new VarOrder());
 275  1 learning.setSolver(solver);
 276  1 solver.setSimplifier(solver.SIMPLE_SIMPLIFICATION);
 277  1 return solver;
 278    }
 279   
 280    /**
 281    * @return a default MiniLearning without restarts.
 282    */
 283  1 public static ISolver newMiniLearningHeapEZSimpNoRestarts() {
 284  1 LimitedLearning learning = new LimitedLearning(10);
 285  1 Solver solver = new Solver(new FirstUIP(), learning,
 286    new MixedDataStructureDaniel(), new SearchParams(
 287    Integer.MAX_VALUE), new VarOrderHeap());
 288  1 learning.setSolver(solver);
 289  1 solver.setSimplifier(solver.SIMPLE_SIMPLIFICATION);
 290  1 return solver;
 291    }
 292   
 293    /**
 294    * @return a default MiniLearning with restarts beginning at 1000 conflicts.
 295    */
 296  1 public static ISolver newMiniLearningHeapEZSimpLongRestarts() {
 297  1 LimitedLearning learning = new LimitedLearning(10);
 298  1 Solver solver = new Solver(new FirstUIP(), learning,
 299    new MixedDataStructureDaniel(), new SearchParams(1000),
 300    new VarOrderHeap());
 301  1 learning.setSolver(solver);
 302  1 solver.setSimplifier(solver.SIMPLE_SIMPLIFICATION);
 303  1 return solver;
 304    }
 305   
 306    /**
 307    * @return a SAT solver using First UIP clause generator, watched literals,
 308    * VSIDS like heuristics learning only clauses having a great number
 309    * of active variables, i.e. variables with an activity strictly
 310    * greater than one.
 311    */
 312  102 public static ISolver newActiveLearning() {
 313  102 ActiveLearning learning = new ActiveLearning();
 314  102 Solver s = new Solver(new FirstUIP(), learning,
 315    new MixedDataStructureDaniel(), new VarOrder());
 316  102 learning.setOrder(s.getOrder());
 317  102 learning.setSolver(s);
 318  102 return s;
 319    }
 320   
 321    /**
 322    * @return a SAT solver very close to the original MiniSAT sat solver.
 323    */
 324  104 public static ISolver newMiniSAT() {
 325  104 return newMiniSAT(new MixedDataStructureDaniel());
 326    }
 327   
 328    /**
 329    * @return MiniSAT without restarts.
 330    */
 331  1 public static ISolver newMiniSATNoRestarts() {
 332  1 MiniSATLearning learning = new MiniSATLearning();
 333  1 Solver solver = new Solver(new FirstUIP(), learning,
 334    new MixedDataStructureDaniel(), new SearchParams(
 335    Integer.MAX_VALUE), new VarOrder());
 336  1 learning.setDataStructureFactory(solver.getDSFactory());
 337  1 learning.setVarActivityListener(solver);
 338  1 return solver;
 339   
 340    }
 341   
 342    /**
 343    * @return MiniSAT with a special data structure from Lawrence Ryan thesis
 344    * for managing binary clauses.
 345    */
 346  1 public static ISolver newMiniSAT2() {
 347  1 return newMiniSAT(new MixedDataStructureWithBinary());
 348    }
 349   
 350    /**
 351    * @return MiniSAT with a special data structure from Lawrence Ryan thesis
 352    * for managing binary and ternary clauses.
 353    */
 354  1 public static ISolver newMiniSAT23() {
 355  1 return newMiniSAT(new MixedDataStructureWithBinaryAndTernary());
 356    }
 357   
 358    /**
 359    * @param dsf
 360    * the data structure used for representing clauses and lits
 361    * @return MiniSAT the data structure dsf.
 362    */
 363  107 public static ISolver newMiniSAT(DataStructureFactory dsf) {
 364  107 MiniSATLearning learning = new MiniSATLearning();
 365  107 Solver solver = new Solver(new FirstUIP(), learning, dsf,
 366    new VarOrder());
 367  107 learning.setDataStructureFactory(solver.getDSFactory());
 368  107 learning.setVarActivityListener(solver);
 369  107 return solver;
 370    }
 371   
 372    /**
 373    * @return a SAT solver very close to the original MiniSAT sat solver.
 374    */
 375  2 public static ISolver newMiniSATHeap() {
 376  2 return newMiniSATHeap(new MixedDataStructureDaniel());
 377    }
 378   
 379    /**
 380    * @return a SAT solver very close to the original MiniSAT sat solver
 381    * including easy reason simplification.
 382    */
 383  1 public static ISolver newMiniSATHeapEZSimp() {
 384  1 Solver solver = (Solver) newMiniSATHeap();
 385  1 solver.setSimplifier(solver.SIMPLE_SIMPLIFICATION);
 386  1 return solver;
 387    }
 388   
 389    /**
 390    * @return MiniSAT with a special data structure from Lawrence Ryan thesis
 391    * for managing binary clauses.
 392    */
 393  1 public static ISolver newMiniSAT2Heap() {
 394  1 return newMiniSATHeap(new MixedDataStructureWithBinary());
 395    }
 396   
 397    /**
 398    * @return MiniSAT with a special data structure from Lawrence Ryan thesis
 399    * for managing binary and ternary clauses.
 400    */
 401  1 public static ISolver newMiniSAT23Heap() {
 402  1 return newMiniSATHeap(new MixedDataStructureWithBinaryAndTernary());
 403    }
 404   
 405  4 public static ISolver newMiniSATHeap(DataStructureFactory dsf) {
 406  4 MiniSATLearning learning = new MiniSATLearning();
 407  4 Solver solver = new Solver(new FirstUIP(), learning, dsf,
 408    new VarOrderHeap());
 409  4 learning.setDataStructureFactory(solver.getDSFactory());
 410  4 learning.setVarActivityListener(solver);
 411  4 return solver;
 412    }
 413   
 414    /**
 415    * @return MiniSAT with data structures to handle cardinality constraints.
 416    */
 417  1 public static ISolver newMiniCard() {
 418  1 return newMiniSAT(new CardinalityDataStructure());
 419    }
 420   
 421    /**
 422    * @return MiniSAT with Counter-based pseudo boolean constraints and clause
 423    * learning.
 424    */
 425  157 public static ISolver newMinimalOPBMax() {
 426  157 MiniSATLearning learning = new MiniSATLearning();
 427  157 Solver solver = new Solver(new FirstUIP(), learning,
 428    new PBMaxDataStructure(), new VarOrderHeap());
 429  157 learning.setDataStructureFactory(solver.getDSFactory());
 430  157 learning.setVarActivityListener(solver);
 431  157 return solver;
 432    }
 433   
 434    /**
 435    * @return MiniSAT with Counter-based pseudo boolean constraints and
 436    * constraint learning.
 437    */
 438  157 public static ISolver newMiniOPBMax() {
 439  157 MiniSATLearning learning = new MiniSATLearning();
 440  157 Solver solver = new PBSolver(new FirstUIP(), learning,
 441    new PBMaxDataStructure(), new VarOrderHeap());
 442  157 learning.setDataStructureFactory(solver.getDSFactory());
 443  157 learning.setVarActivityListener(solver);
 444  157 return solver;
 445    }
 446   
 447    /**
 448    * @return MiniSAT with Counter-based pseudo boolean constraints and
 449    * constraint learning. Clauses and cardinalities with watched
 450    * literals are also handled (and learnt).
 451    */
 452  54 public static ISolver newMiniOPBClauseCardConstrMax() {
 453  54 MiniSATLearning learning = new MiniSATLearning();
 454  54 Solver solver = new PBSolver(new FirstUIP(), learning,
 455    new PBMaxClauseCardConstrDataStructure(), new VarOrderHeap());
 456  54 learning.setDataStructureFactory(solver.getDSFactory());
 457  54 learning.setVarActivityListener(solver);
 458  54 return solver;
 459    }
 460   
 461    /**
 462    * @return MiniSAT with Counter-based pseudo boolean constraints and
 463    * constraint learning. Clauses and cardinalities with watched
 464    * literals are also handled (and learnt). A specific heuristics
 465    * taking into account the objective value is used.
 466    */
 467  1 public static ISolver newMiniOPBClauseCardConstrMaxSpecificOrder() {
 468  1 MiniSATLearning learning = new MiniSATLearning();
 469  1 Solver solver = new PBSolver(new FirstUIP(), learning,
 470    new PBMaxClauseCardConstrDataStructure(),
 471    new VarOrderHeapObjective());
 472  1 learning.setDataStructureFactory(solver.getDSFactory());
 473  1 learning.setVarActivityListener(solver);
 474  1 return solver;
 475    }
 476   
 477    /**
 478    * @return MiniSAT with Counter-based pseudo boolean constraints and
 479    * constraint learning. Clauses and cardinalities with watched
 480    * literals are also handled (and learnt). A reduction of
 481    * PB-constraints to clauses is made in order to simplify cutting
 482    * planes.
 483    */
 484  54 public static ISolver newMiniOPBClauseCardConstrMaxReduceToClause() {
 485  54 MiniSATLearning learning = new MiniSATLearning();
 486  54 Solver solver = new PBSolverClause(new FirstUIP(), learning,
 487    new PBMaxClauseCardConstrDataStructure(), new VarOrderHeap());
 488  54 learning.setDataStructureFactory(solver.getDSFactory());
 489  54 learning.setVarActivityListener(solver);
 490  54 return solver;
 491    }
 492   
 493    /**
 494    * @return MiniSAT with Counter-based pseudo boolean constraints and
 495    * constraint learning. Clauses and cardinalities with watched
 496    * literals are also handled (and learnt). A reduction of
 497    * PB-constraints to cardinalities is made in order to simplify
 498    * cutting planes.
 499    */
 500  1 public static ISolver newMiniOPBClauseCardConstrMaxReduceToCard() {
 501  1 MiniSATLearning learning = new MiniSATLearning();
 502  1 Solver solver = new PBSolverCard(new FirstUIP(), learning,
 503    new PBMaxClauseCardConstrDataStructure(), new VarOrderHeap());
 504  1 learning.setDataStructureFactory(solver.getDSFactory());
 505  1 learning.setVarActivityListener(solver);
 506  1 return solver;
 507    }
 508   
 509    /**
 510    * @return MiniSAT with Counter-based pseudo boolean constraints and
 511    * constraint learning. Clauses and cardinalities with watched
 512    * literals are also handled (and learnt). a pre-processing is
 513    * applied which adds implied clauses from PB-constraints.
 514    */
 515  1 public static ISolver newMiniOPBClauseCardConstrMaxImplied() {
 516  1 MiniSATLearning learning = new MiniSATLearning();
 517  1 Solver solver = new PBSolverWithImpliedClause(new FirstUIP(), learning,
 518    new PBMaxClauseCardConstrDataStructure(), new VarOrderHeap());
 519  1 learning.setDataStructureFactory(solver.getDSFactory());
 520  1 learning.setVarActivityListener(solver);
 521  1 return solver;
 522    }
 523   
 524    /**
 525    * @return MiniSAT with Counter-based pseudo boolean constraints,
 526    * counter-based cardinalities, watched clauses and constraint
 527    * learning.
 528    */
 529  54 public static ISolver newMiniOPBClauseAtLeastConstrMax() {
 530  54 MiniSATLearning learning = new MiniSATLearning();
 531  54 Solver solver = new PBSolver(new FirstUIP(), learning,
 532    new PBMaxClauseAtLeastConstrDataStructure(), new VarOrderHeap());
 533  54 learning.setDataStructureFactory(solver.getDSFactory());
 534  54 learning.setVarActivityListener(solver);
 535  54 return solver;
 536    }
 537   
 538    /**
 539    * @return MiniSAT with Counter-based pseudo boolean constraints and
 540    * clauses, watched cardinalities, and constraint learning.
 541    */
 542  54 public static ISolver newMiniOPBCounterBasedClauseCardConstrMax() {
 543  54 MiniSATLearning learning = new MiniSATLearning();
 544  54 Solver solver = new PBSolver(new FirstUIP(), learning,
 545    new PBMaxCBClauseCardConstrDataStructure(), new VarOrderHeap());
 546  54 learning.setDataStructureFactory(solver.getDSFactory());
 547  54 learning.setVarActivityListener(solver);
 548  54 return solver;
 549    }
 550   
 551    /**
 552    * @return MiniSAT with WL-based pseudo boolean constraints and clause
 553    * learning.
 554    */
 555  157 public static ISolver newMinimalOPBMin() {
 556  157 MiniSATLearning learning = new MiniSATLearning();
 557  157 Solver solver = new Solver(new FirstUIP(), learning,
 558    new PBMinDataStructure(), new VarOrderHeap());
 559  157 learning.setDataStructureFactory(solver.getDSFactory());
 560  157 learning.setVarActivityListener(solver);
 561  157 return solver;
 562    }
 563   
 564    /**
 565    * @return MiniSAT with WL-based pseudo boolean constraints and constraint
 566    * learning.
 567    */
 568  157 public static ISolver newMiniOPBMin() {
 569  157 MiniSATLearning learning = new MiniSATLearning();
 570  157 Solver solver = new PBSolver(new FirstUIP(), learning,
 571    new PBMinDataStructure(), new VarOrderHeap());
 572  157 learning.setDataStructureFactory(solver.getDSFactory());
 573  157 learning.setVarActivityListener(solver);
 574  157 return solver;
 575    }
 576   
 577    /**
 578    * @return MiniSAT with WL-based pseudo boolean constraints and clause
 579    * learning.
 580    */
 581  54 public static ISolver newMinimalOPBMinPueblo() {
 582  54 MiniSATLearning learning = new MiniSATLearning();
 583  54 Solver solver = new Solver(new FirstUIP(), learning,
 584    new PuebloPBMinDataStructure(), new VarOrderHeap());
 585  54 learning.setDataStructureFactory(solver.getDSFactory());
 586  54 learning.setVarActivityListener(solver);
 587  54 return solver;
 588    }
 589   
 590    /**
 591    * @return MiniSAT with WL-based pseudo boolean constraints and constraint
 592    * learning.
 593    */
 594  54 public static ISolver newMiniOPBMinPueblo() {
 595  54 MiniSATLearning learning = new MiniSATLearning();
 596  54 Solver solver = new PBSolver(new FirstUIP(), learning,
 597    new PuebloPBMinDataStructure(), new VarOrderHeap());
 598  54 learning.setDataStructureFactory(solver.getDSFactory());
 599  54 learning.setVarActivityListener(solver);
 600  54 return solver;
 601    }
 602   
 603    /**
 604    * @return MiniSAT with WL-based pseudo boolean constraints and clauses,
 605    * cardinalities, and constraint learning.
 606    */
 607  54 public static ISolver newMiniOPBClauseCardMinPueblo() {
 608  54 MiniSATLearning learning = new MiniSATLearning();
 609  54 Solver solver = new PBSolver(new FirstUIP(), learning,
 610    new PuebloPBMinClauseCardConstrDataStructure(),
 611    new VarOrderHeap());
 612  54 learning.setDataStructureFactory(solver.getDSFactory());
 613  54 learning.setVarActivityListener(solver);
 614  54 return solver;
 615    }
 616   
 617    /**
 618    * @return MiniSAT with WL-based pseudo boolean constraints and clauses,
 619    * cardinalities, and constraint learning.
 620    */
 621  1 public static ISolver newMiniOPBClauseCardMin() {
 622  1 MiniSATLearning learning = new MiniSATLearning();
 623  1 Solver solver = new PBSolver(new FirstUIP(), learning,
 624    new PBMinClauseCardConstrDataStructure(), new VarOrderHeap());
 625  1 learning.setDataStructureFactory(solver.getDSFactory());
 626  1 learning.setVarActivityListener(solver);
 627  1 return solver;
 628    }
 629   
 630    /**
 631    * @return MiniSAT with WL-based pseudo boolean constraints and clauses,
 632    * counter-based cardinalities, and constraint learning.
 633    */
 634  54 public static ISolver newMiniOPBClauseAtLeastMinPueblo() {
 635  54 MiniSATLearning learning = new MiniSATLearning();
 636  54 Solver solver = new PBSolver(new FirstUIP(), learning,
 637    new PuebloPBMinClauseAtLeastConstrDataStructure(),
 638    new VarOrderHeap());
 639  54 learning.setDataStructureFactory(solver.getDSFactory());
 640  54 learning.setVarActivityListener(solver);
 641  54 return solver;
 642    }
 643   
 644    /**
 645    * @return MiniSAT with decision UIP clause generator.
 646    */
 647  102 public static ISolver newRelsat() {
 648  102 MiniSATLearning learning = new MiniSATLearning();
 649  102 Solver solver = new Solver(new DecisionUIP(), learning,
 650    new MixedDataStructureDaniel(), new VarOrderHeap());
 651  102 learning.setDataStructureFactory(solver.getDSFactory());
 652  102 learning.setVarActivityListener(solver);
 653  102 return solver;
 654    }
 655   
 656    /**
 657    * @return MiniSAT with VSIDS heuristics, FirstUIP clause generator for
 658    * backjumping but no learning.
 659    */
 660  102 public static ISolver newBackjumping() {
 661  102 NoLearningButHeuristics learning = new NoLearningButHeuristics();
 662  102 Solver solver = new Solver(new FirstUIP(), learning,
 663    new MixedDataStructureDaniel(), new VarOrderHeap());
 664  102 learning.setVarActivityListener(solver);
 665  102 return solver;
 666    }
 667   
 668    /**
 669    * @return a SAT solver with learning limited to clauses of length smaller
 670    * or equals to 3, with a specific data structure for binary and
 671    * ternary clauses as found in Lawrence Ryan thesis, without
 672    * restarts, with a Jeroslow/Wang kind of heuristics.
 673    */
 674  103 public static ISolver newMini3SAT() {
 675  103 LimitedLearning learning = new FixedLengthLearning(3);
 676  103 Solver solver = new Solver(new FirstUIP(), learning,
 677    new MixedDataStructureWithBinaryAndTernary(), new SearchParams(
 678    Integer.MAX_VALUE), new VarOrderHeap());
 679  103 learning.setSolver(solver);
 680  103 solver.setOrder(new JWOrder());
 681  103 return solver;
 682    }
 683   
 684    /**
 685    * @return a Mini3SAT with full learning.
 686    * @see #newMini3SAT()
 687    */
 688  1 public static ISolver newMini3SATb() {
 689  1 MiniSATLearning learning = new MiniSATLearning();
 690  1 Solver solver = new Solver(new FirstUIP(), learning,
 691    new MixedDataStructureWithBinaryAndTernary(), new SearchParams(
 692    Integer.MAX_VALUE), new VarOrderHeap());
 693  1 learning.setDataStructureFactory(solver.getDSFactory());
 694  1 learning.setVarActivityListener(solver);
 695  1 solver.setOrder(new JWOrder());
 696  1 return solver;
 697    }
 698   
 699    /**
 700    * A SAT solver that adapts its data structures according to the problem
 701    * to solve.
 702    * @return a MiniLearningHeapEZSimp solver decorated with a SATRaceDecorator.
 703    */
 704  1 public static ISolver newAdaptiveSolver() {
 705  1 return new SATRaceDecorator(newMiniLearningHeapEZSimp());
 706    }
 707   
 708    /**
 709    * Default solver of the SolverFactory. This solver is meant to be used on
 710    * challenging SAT benchmarks.
 711    *
 712    * @return the best "general purpose" SAT solver available in the factory.
 713    * @see #defaultSolver() the same method, polymorphic, to be called from an
 714    * instance of ASolverFactory.
 715    */
 716  1 public static ISolver newDefault() {
 717  1 return newMiniLearningHeapEZSimp();
 718    }
 719   
 720  0 @Override
 721    public ISolver defaultSolver() {
 722  0 return newDefault();
 723    }
 724   
 725    /**
 726    * Small footprint SAT solver.
 727    *
 728    * @return a SAT solver suitable for solving small/easy SAT benchmarks.
 729    * @see #lightSolver() the same method, polymorphic, to be called from an
 730    * instance of ASolverFactory.
 731    */
 732  1 public static ISolver newLight() {
 733  1 return newMini3SAT();
 734    }
 735   
 736  0 @Override
 737    public ISolver lightSolver() {
 738  0 return newLight();
 739    }
 740   
 741    }
 
CloverReport generated by Clover Code Coverage v1.3.9
jeu. juin 15 2006 08:24:39 CEST.		   Open Source License registered to the OpenSAT Project. This license of Clover is provided to support the development of OpenSAT only.