Clover coverage report -
Coverage timestamp: jeu. sept. 29 2005 23:57:39 CEST
Overview   Package   File
    FRAMES   NO FRAMES  
file stats: LOC: 471   Methods: 40
NCLOC: 233   Classes: 1
 
 Source file Conditionals Statements Methods TOTAL
SolverFactory.java - 98,1% 95% 97,2%
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 org.sat4j.core.ASolverFactory;
 28    import org.sat4j.minisat.constraints.CardinalityDataStructure;
 29    import org.sat4j.minisat.constraints.ClausalDataStructureCB;
 30    import org.sat4j.minisat.constraints.ClausalDataStructureCBWL;
 31    import org.sat4j.minisat.constraints.MixedDataStructureDaniel;
 32    import org.sat4j.minisat.constraints.MixedDataStructureWithBinary;
 33    import org.sat4j.minisat.constraints.MixedDataStructureWithBinaryAndTernary;
 34    import org.sat4j.minisat.constraints.PBMaxDataStructure;
 35    import org.sat4j.minisat.constraints.PBMinDataStructure;
 36    import org.sat4j.minisat.constraints.pb.PBSolver;
 37    import org.sat4j.minisat.core.DataStructureFactory;
 38    import org.sat4j.minisat.core.IOrder;
 39    import org.sat4j.minisat.core.SearchParams;
 40    import org.sat4j.minisat.core.Solver;
 41    import org.sat4j.minisat.learning.ActiveLearning;
 42    import org.sat4j.minisat.learning.FixedLengthLearning;
 43    import org.sat4j.minisat.learning.LimitedLearning;
 44    import org.sat4j.minisat.learning.MiniSATLearning;
 45    import org.sat4j.minisat.learning.NoLearningButHeuristics;
 46    import org.sat4j.minisat.orders.JWOrder;
 47    import org.sat4j.minisat.orders.MyOrder;
 48    import org.sat4j.minisat.orders.PureOrder;
 49    import org.sat4j.minisat.orders.VarOrder;
 50    import org.sat4j.minisat.orders.VarOrderHeap;
 51    import org.sat4j.minisat.uip.DecisionUIP;
 52    import org.sat4j.minisat.uip.FirstUIP;
 53    import org.sat4j.specs.ISolver;
 54   
 55    /**
 56    * User friendly access to pre-constructed solvers.
 57    *
 58    * @author leberre
 59    */
 60    public class SolverFactory extends ASolverFactory {
 61   
 62    /**
 63    * @return a "default" "minilearning" solver learning clauses of size
 64    * smaller than 10 % of the total number of variables
 65    */
 66  106 public static ISolver newMiniLearning() {
 67  106 return newMiniLearning(10);
 68    }
 69   
 70    /**
 71    * @return a "default" "minilearning" solver learning clauses of size
 72    * smaller than 10 % of the total number of variables with a heap
 73    * based var order.
 74    */
 75  1 public static ISolver newMiniLearningHeap() {
 76  1 return newMiniLearningHeap(new MixedDataStructureDaniel());
 77    }
 78   
 79  1 public static ISolver newMiniLearningHeapEZSimp() {
 80  1 LimitedLearning learning = new LimitedLearning(10);
 81  1 Solver solver = new Solver(new FirstUIP(), learning, new MixedDataStructureDaniel(),new VarOrderHeap());
 82  1 learning.setSolver(solver);
 83  1 solver.setSimplifier(solver.SIMPLE_SIMPLIFICATION);
 84  1 return solver;
 85    }
 86   
 87    /**
 88    * @param n
 89    * the maximal size of the clauses to learn as a percentage of
 90    * the initial number of variables
 91    * @return a "minilearning" solver learning clauses of size smaller than n
 92    * of the total number of variables
 93    */
 94  106 public static ISolver newMiniLearning(int n) {
 95  106 return newMiniLearning(new MixedDataStructureDaniel(), n);
 96    }
 97   
 98    /**
 99    * @param dsf
 100    * a specific data structure factory
 101    * @return a default "minilearning" solver using a specific data structure
 102    * factory, learning clauses of length smaller or equals to 10 % of
 103    * the number of variables.
 104    */
 105  771 public static ISolver newMiniLearning(DataStructureFactory dsf) {
 106  771 return newMiniLearning(dsf, 10);
 107    }
 108   
 109    /**
 110    * @param dsf
 111    * a specific data structure factory
 112    * @return a default "minilearning" solver using a specific data structure
 113    * factory, learning clauses of length smaller or equals to 10 % of
 114    * the number of variables and a heap based VSIDS heuristics
 115    */
 116  2 public static ISolver newMiniLearningHeap(DataStructureFactory dsf) {
 117  2 return newMiniLearning(dsf, new VarOrderHeap());
 118    }
 119   
 120    /**
 121    * @return a default minilearning solver using a specific data structure
 122    * described in Lawrence Ryan thesis to handle binary clauses.
 123    * @see #newMiniLearning
 124    */
 125  203 public static ISolver newMiniLearning2() {
 126  203 return newMiniLearning(new MixedDataStructureWithBinary());
 127    }
 128   
 129  1 public static ISolver newMiniLearning2Heap() {
 130  1 return newMiniLearningHeap(new MixedDataStructureWithBinary());
 131    }
 132   
 133    /**
 134    * @return a default minilearning solver using a specific data structures
 135    * described in Lawrence Ryan thesis to handle binary and ternary
 136    * clauses.
 137    * @see #newMiniLearning
 138    */
 139  1 public static ISolver newMiniLearning23() {
 140  1 return newMiniLearning(new MixedDataStructureWithBinaryAndTernary());
 141    }
 142   
 143    /**
 144    * @return a default minilearning SAT solver using counter-based clause
 145    * representation (i.e. all the literals of a clause are watched)
 146    */
 147  102 public static ISolver newMiniLearningCB() {
 148  102 return newMiniLearning(new ClausalDataStructureCB());
 149    }
 150   
 151    /**
 152    * @return a default minilearning SAT solver using counter-based clause
 153    * representation (i.e. all the literals of a clause are watched)
 154    * for the ORIGINAL clauses and watched-literals clause
 155    * representation for learnt clauses.
 156    */
 157  1 public static ISolver newMiniLearningCBWL() {
 158  1 return newMiniLearning(new ClausalDataStructureCBWL());
 159    }
 160   
 161  1 public static ISolver newMiniLearning2NewOrder() {
 162  1 return newMiniLearning(new MixedDataStructureWithBinary(),
 163    new MyOrder());
 164    }
 165   
 166    /**
 167    * @return a default minilearning SAT solver choosing periodically to branch
 168    * on "pure watched" literals if any. (a pure watched literal l is a
 169    * literal that is watched on at least one clause such that its
 170    * negation is not watched at all. It is not necessarily a watched
 171    * literal.)
 172    */
 173  1 public static ISolver newMiniLearningPure() {
 174  1 return newMiniLearning(new MixedDataStructureDaniel(), new PureOrder());
 175    }
 176   
 177    /**
 178    * @return a default minilearning SAT solver choosing periodically to branch
 179    * on literal "pure in the original set of clauses" if any.
 180    */
 181  1 public static ISolver newMiniLearningCBWLPure() {
 182  1 return newMiniLearning(new ClausalDataStructureCBWL(), new PureOrder());
 183    }
 184   
 185    /**
 186    * @param dsf
 187    * the data structure factory used to represent literals and
 188    * clauses
 189    * @param n
 190    * the maximum size of learnt clauses as percentage of the
 191    * original number of variables.
 192    * @return a SAT solver with learning limited to clauses of length smaller
 193    * or equal to n, the dsf data structure, the FirstUIP clause
 194    * generator and a sort of VSIDS heuristics.
 195    */
 196  877 public static ISolver newMiniLearning(DataStructureFactory dsf, int n) {
 197  877 LimitedLearning learning = new LimitedLearning(n);
 198  877 Solver solver = new Solver(new FirstUIP(), learning, dsf,new VarOrder());
 199  877 learning.setSolver(solver);
 200  877 return solver;
 201    }
 202   
 203    /**
 204    * @param dsf
 205    * the data structure factory used to represent literals and
 206    * clauses
 207    * @param order
 208    * the heuristics
 209    * @return a SAT solver with learning limited to clauses of length smaller
 210    * or equal to 10 percent of the total number of variables, the dsf
 211    * data structure, the FirstUIP clause generator and order as
 212    * heuristics.
 213    */
 214  5 public static ISolver newMiniLearning(DataStructureFactory dsf,
 215    IOrder order) {
 216  5 LimitedLearning learning = new LimitedLearning(10);
 217  5 Solver solver = new Solver(new FirstUIP(), learning, dsf, order);
 218  5 learning.setSolver(solver);
 219  5 return solver;
 220    }
 221   
 222  1 public static ISolver newMiniLearningEZSimp() {
 223  1 return newMiniLearningEZSimp(new MixedDataStructureDaniel());
 224    }
 225   
 226    // public static ISolver newMiniLearning2EZSimp() {
 227    // return newMiniLearningEZSimp(new MixedDataStructureWithBinary());
 228    // }
 229   
 230  1 public static ISolver newMiniLearningEZSimp(DataStructureFactory dsf) {
 231  1 LimitedLearning learning = new LimitedLearning(10);
 232  1 Solver solver = new Solver(new FirstUIP(), learning, dsf,new VarOrder());
 233  1 learning.setSolver(solver);
 234  1 solver.setSimplifier(solver.SIMPLE_SIMPLIFICATION);
 235  1 return solver;
 236    }
 237   
 238    /**
 239    * @return a default MiniLearning without restarts.
 240    */
 241  1 public static ISolver newMiniLearningNoRestarts() {
 242  1 LimitedLearning learning = new LimitedLearning(10);
 243  1 Solver solver = new Solver(new FirstUIP(), learning,
 244    new MixedDataStructureDaniel(), new SearchParams(
 245    Integer.MAX_VALUE),new VarOrder());
 246  1 learning.setSolver(solver);
 247  1 return solver;
 248    }
 249   
 250    /**
 251    * @return a SAT solver using First UIP clause generator, watched literals,
 252    * VSIDS like heuristics learning only clauses having a great number
 253    * of active variables, i.e. variables with an activity strictly
 254    * greater than one.
 255    */
 256  102 public static ISolver newActiveLearning() {
 257  102 ActiveLearning learning = new ActiveLearning();
 258  102 Solver s = new Solver(new FirstUIP(), learning,
 259    new MixedDataStructureDaniel(),new VarOrder());
 260  102 learning.setOrder(s.getOrder());
 261  102 learning.setSolver(s);
 262  102 return s;
 263    }
 264   
 265    /**
 266    * @return a SAT solver very close to the original MiniSAT sat solver.
 267    */
 268  102 public static ISolver newMiniSAT() {
 269  102 return newMiniSAT(new MixedDataStructureDaniel());
 270    }
 271   
 272    /**
 273    * @return MiniSAT without restarts.
 274    */
 275  1 public static ISolver newMiniSATNoRestarts() {
 276  1 MiniSATLearning learning = new MiniSATLearning();
 277  1 Solver solver = new Solver(new FirstUIP(), learning,
 278    new MixedDataStructureDaniel(), new SearchParams(
 279    Integer.MAX_VALUE),new VarOrder());
 280  1 learning.setDataStructureFactory(solver.getDSFactory());
 281  1 learning.setVarActivityListener(solver);
 282  1 return solver;
 283   
 284    }
 285   
 286    /**
 287    * @return MiniSAT with a special data structure from Lawrence Ryan thesis
 288    * for managing binary clauses.
 289    */
 290  1 public static ISolver newMiniSAT2() {
 291  1 return newMiniSAT(new MixedDataStructureWithBinary());
 292    }
 293   
 294    /**
 295    * @return MiniSAT with a special data structure from Lawrence Ryan thesis
 296    * for managing binary and ternary clauses.
 297    */
 298  1 public static ISolver newMiniSAT23() {
 299  1 return newMiniSAT(new MixedDataStructureWithBinaryAndTernary());
 300    }
 301   
 302    /**
 303    * @param dsf
 304    * the data structure used for representing clauses and lits
 305    * @return MiniSAT the data structure dsf.
 306    */
 307  105 public static ISolver newMiniSAT(DataStructureFactory dsf) {
 308  105 MiniSATLearning learning = new MiniSATLearning();
 309  105 Solver solver = new Solver(new FirstUIP(), learning, dsf,new VarOrder());
 310  105 learning.setDataStructureFactory(solver.getDSFactory());
 311  105 learning.setVarActivityListener(solver);
 312  105 return solver;
 313    }
 314   
 315    /**
 316    * @return a SAT solver very close to the original MiniSAT sat solver.
 317    */
 318  1 public static ISolver newMiniSATHeap() {
 319  1 return newMiniSATHeap(new MixedDataStructureDaniel());
 320    }
 321   
 322    /**
 323    * @return MiniSAT with a special data structure from Lawrence Ryan thesis
 324    * for managing binary clauses.
 325    */
 326  1 public static ISolver newMiniSAT2Heap() {
 327  1 return newMiniSATHeap(new MixedDataStructureWithBinary());
 328    }
 329   
 330    /**
 331    * @return MiniSAT with a special data structure from Lawrence Ryan thesis
 332    * for managing binary and ternary clauses.
 333    */
 334  1 public static ISolver newMiniSAT23Heap() {
 335  1 return newMiniSATHeap(new MixedDataStructureWithBinaryAndTernary());
 336    }
 337   
 338  3 public static ISolver newMiniSATHeap(DataStructureFactory dsf) {
 339  3 MiniSATLearning learning = new MiniSATLearning();
 340  3 Solver solver = new Solver(new FirstUIP(), learning, dsf,new VarOrderHeap());
 341  3 learning.setDataStructureFactory(solver.getDSFactory());
 342  3 learning.setVarActivityListener(solver);
 343  3 return solver;
 344    }
 345   
 346    /**
 347    * @return MiniSAT with data strcutures to handle cardinality constraints.
 348    */
 349  1 public static ISolver newMiniCard() {
 350  1 return newMiniSAT(new CardinalityDataStructure());
 351    }
 352   
 353    /**
 354    * @return MiniSAT with Counter-based pseudo boolean constraints and clause
 355    * learning.
 356    */
 357  157 public static ISolver newMinimalOPBMax() {
 358  157 MiniSATLearning learning = new MiniSATLearning();
 359  157 Solver solver = new Solver(new FirstUIP(), learning,
 360    new PBMaxDataStructure(),new VarOrder());
 361  157 learning.setDataStructureFactory(solver.getDSFactory());
 362  157 learning.setVarActivityListener(solver);
 363  157 return solver;
 364    }
 365   
 366    /**
 367    * @return MiniSAT with Counter-based pseudo boolean constraints and
 368    * constraint learning.
 369    */
 370  157 public static ISolver newMiniOPBMax() {
 371  157 MiniSATLearning learning = new MiniSATLearning();
 372  157 Solver solver = new PBSolver(new FirstUIP(), learning,
 373    new PBMaxDataStructure(),new VarOrder());
 374  157 learning.setDataStructureFactory(solver.getDSFactory());
 375  157 learning.setVarActivityListener(solver);
 376  157 return solver;
 377    }
 378   
 379    /**
 380    * @return MiniSAT with WL-based pseudo boolean constraints and clause
 381    * learning.
 382    */
 383  157 public static ISolver newMinimalOPBMin() {
 384  157 MiniSATLearning learning = new MiniSATLearning();
 385  157 Solver solver = new Solver(new FirstUIP(), learning,
 386    new PBMinDataStructure(),new VarOrder());
 387  157 learning.setDataStructureFactory(solver.getDSFactory());
 388  157 learning.setVarActivityListener(solver);
 389  157 return solver;
 390    }
 391   
 392    /**
 393    * @return MiniSAT with WL-based pseudo boolean constraints and constraint
 394    * learning.
 395    */
 396  157 public static ISolver newMiniOPBMin() {
 397  157 MiniSATLearning learning = new MiniSATLearning();
 398  157 Solver solver = new PBSolver(new FirstUIP(), learning,
 399    new PBMinDataStructure(),new VarOrder());
 400  157 learning.setDataStructureFactory(solver.getDSFactory());
 401  157 learning.setVarActivityListener(solver);
 402  157 return solver;
 403    }
 404   
 405    /**
 406    * @return MiniSAT with decision UIP clause generator.
 407    */
 408  102 public static ISolver newRelsat() {
 409  102 MiniSATLearning learning = new MiniSATLearning();
 410  102 Solver solver = new Solver(new DecisionUIP(), learning,
 411    new MixedDataStructureDaniel(),new VarOrder());
 412  102 learning.setDataStructureFactory(solver.getDSFactory());
 413  102 learning.setVarActivityListener(solver);
 414  102 return solver;
 415    }
 416   
 417    /**
 418    * @return MiniSAT with VSIDS heuristics, FirstUIP clause generator for
 419    * backjumping but no learning.
 420    */
 421  102 public static ISolver newBackjumping() {
 422  102 NoLearningButHeuristics learning = new NoLearningButHeuristics();
 423  102 Solver solver = new Solver(new FirstUIP(), learning,
 424    new MixedDataStructureDaniel(),new VarOrder());
 425  102 learning.setVarActivityListener(solver);
 426  102 return solver;
 427    }
 428   
 429    /**
 430    * @return a SAT solver with learning limited to clauses of length smaller
 431    * or equals to 3, with a specific data structure for binary and
 432    * ternary clauses as found in Lawrence Ryan thesis, without
 433    * restarts, with a Jeroslow/Wang kind of heuristics.
 434    */
 435  102 public static ISolver newMini3SAT() {
 436  102 LimitedLearning learning = new FixedLengthLearning(3);
 437  102 Solver solver = new Solver(new FirstUIP(), learning,
 438    new MixedDataStructureWithBinaryAndTernary(), new SearchParams(
 439    Integer.MAX_VALUE),new VarOrder());
 440  102 learning.setSolver(solver);
 441  102 solver.setOrder(new JWOrder());
 442  102 return solver;
 443    }
 444   
 445    /**
 446    * @return a Mini3SAT with full learning.
 447    * @see #newMini3SAT()
 448    */
 449  1 public static ISolver newMini3SATb() {
 450  1 MiniSATLearning learning = new MiniSATLearning();
 451  1 Solver solver = new Solver(new FirstUIP(), learning,
 452    new MixedDataStructureWithBinaryAndTernary(), new SearchParams(
 453    Integer.MAX_VALUE),new VarOrder());
 454  1 learning.setDataStructureFactory(solver.getDSFactory());
 455  1 learning.setVarActivityListener(solver);
 456  1 solver.setOrder(new JWOrder());
 457  1 return solver;
 458    }
 459   
 460  0 @Override
 461    public ISolver defaultSolver() {
 462  0 return newMiniLearning2Heap();
 463    }
 464   
 465  0 @Override
 466    public ISolver lightSolver() {
 467  0 return newMini3SAT();
 468    }
 469   
 470   
 471    }
 
CloverReport generated by Clover Code Coverage v1.3.9
jeu. sept. 29 2005 23:57:47 CEST.		   Open Source License registered to the OpenSAT Project. This license of Clover is provided to support the development of OpenSAT only.