/*
    * SAT4J: a SATisfiability library for Java Copyright (C) 2004-2006 Daniel Le
    * Berre
    * 
    * Based on the original minisat specification from:
    * 
    * An extensible SAT solver. Niklas E?n and Niklas S?rensson. Proceedings of the
    * Sixth International Conference on Theory and Applications of Satisfiability
    * Testing, LNCS 2919, pp 502-518, 2003.
   * 
   * This library is free software; you can redistribute it and/or modify it under
   * the terms of the GNU Lesser General Public License as published by the Free
   * Software Foundation; either version 2.1 of the License, or (at your option)
   * any later version.
   * 
   * This library is distributed in the hope that it will be useful, but WITHOUT
   * ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS
   * FOR A PARTICULAR PURPOSE. See the GNU Lesser General Public License for more
   * details.
   * 
   * You should have received a copy of the GNU Lesser General Public License
   * along with this library; if not, write to the Free Software Foundation, Inc.,
   * 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
   * 
   */
  
  package org.sat4j.minisat;
  
  import java.io.Serializable;
  
  import org.sat4j.core.ASolverFactory;
  import org.sat4j.minisat.constraints.CardinalityDataStructure;
  import org.sat4j.minisat.constraints.ClausalDataStructureCB;
  import org.sat4j.minisat.constraints.ClausalDataStructureCBWL;
  import org.sat4j.minisat.constraints.MixedDataStructureDaniel;
  import org.sat4j.minisat.constraints.MixedDataStructureDanielCBWL;
  import org.sat4j.minisat.constraints.MixedDataStructureWithBinary;
  import org.sat4j.minisat.constraints.MixedDataStructureWithBinaryAndTernary;
  import org.sat4j.minisat.constraints.PBMaxCBClauseCardConstrDataStructure;
  import org.sat4j.minisat.constraints.PBMaxClauseAtLeastConstrDataStructure;
  import org.sat4j.minisat.constraints.PBMaxClauseCardConstrDataStructure;
  import org.sat4j.minisat.constraints.PBMaxDataStructure;
  import org.sat4j.minisat.constraints.PBMinClauseCardConstrDataStructure;
  import org.sat4j.minisat.constraints.PBMinDataStructure;
  import org.sat4j.minisat.constraints.PuebloPBMinClauseAtLeastConstrDataStructure;
  import org.sat4j.minisat.constraints.PuebloPBMinClauseCardConstrDataStructure;
  import org.sat4j.minisat.constraints.PuebloPBMinDataStructure;
  import org.sat4j.minisat.constraints.pb.PBSolver;
  import org.sat4j.minisat.constraints.pb.PBSolverClause;
  import org.sat4j.minisat.constraints.pb.PBSolverMerging;
  import org.sat4j.minisat.constraints.pb.PBSolverWithImpliedClause;
  import org.sat4j.minisat.core.DataStructureFactory;
  import org.sat4j.minisat.core.ILits;
  import org.sat4j.minisat.core.ILits2;
  import org.sat4j.minisat.core.ILits23;
  import org.sat4j.minisat.core.IOrder;
  import org.sat4j.minisat.core.SearchParams;
  import org.sat4j.minisat.core.Solver;
  import org.sat4j.minisat.learning.ActiveLearning;
  import org.sat4j.minisat.learning.ClauseOnlyLearning;
  import org.sat4j.minisat.learning.FixedLengthLearning;
  import org.sat4j.minisat.learning.LimitedLearning;
  import org.sat4j.minisat.learning.MiniSATLearning;
  import org.sat4j.minisat.learning.NoLearningButHeuristics;
  import org.sat4j.minisat.learning.PercentLengthLearning;
  import org.sat4j.minisat.orders.JWOrder;
  import org.sat4j.minisat.orders.MyOrder;
  import org.sat4j.minisat.orders.PureOrder;
  import org.sat4j.minisat.orders.VarOrder;
  import org.sat4j.minisat.orders.VarOrderHeap;
  import org.sat4j.minisat.orders.VarOrderHeapObjective;
  import org.sat4j.minisat.orders.VarOrderHeapRsat;
  import org.sat4j.minisat.restarts.ArminRestarts;
  import org.sat4j.minisat.restarts.LubyRestarts;
  import org.sat4j.minisat.restarts.MiniSATRestarts;
  import org.sat4j.minisat.uip.DecisionUIP;
  import org.sat4j.minisat.uip.FirstUIP;
  import org.sat4j.specs.ISolver;
  import org.sat4j.tools.DimacsOutputSolver;
  
  /**
   * User friendly access to pre-constructed solvers.
   * 
   * @author leberre
   */
  public class SolverFactory extends ASolverFactory implements Serializable {
  
      /**
       * 
       */
      private static final long serialVersionUID = 1L;
  
      // thread safe implementation of the singleton design pattern
      private static SolverFactory instance;
  
      /**
       * Private contructor. Use singleton method instance() instead.
       * 
       * @see #instance()
      */
     private SolverFactory() {
         super();
     }
 
     private static synchronized void createInstance() {
         if (instance == null) {
             instance = new SolverFactory();
         }
     }
 
     /**
      * Access to the single instance of the factory.
      * 
      * @return the singleton of that class.
      */
     public static SolverFactory instance() {
         if (instance == null) {
             createInstance();
         }
         return instance;
     }
 
     /**
      * @return a "default" "minilearning" solver learning clauses of size
      *         smaller than 10 % of the total number of variables
      */
     public static Solver<ILits> newMiniLearning() {
         return newMiniLearning(10);
     }
 
     /**
      * @return a "default" "minilearning" solver learning clauses of size
      *         smaller than 10 % of the total number of variables with a heap
      *         based var order.
      */
     public static Solver<ILits> newMiniLearningHeap() {
         return newMiniLearningHeap(new MixedDataStructureDaniel());
     }
 
     public static Solver<ILits> newMiniLearningHeapEZSimp() {
         Solver<ILits> solver = newMiniLearningHeap();
         solver.setSimplifier(solver.SIMPLE_SIMPLIFICATION);
         return solver;
     }
 
     public static Solver<ILits> newMiniLearningHeapExpSimp() {
         Solver<ILits> solver = newMiniLearningHeap();
         solver.setSimplifier(solver.EXPENSIVE_SIMPLIFICATION);
         return solver;
     }
 
     public static Solver<ILits> newMiniLearningHeapRsatExpSimp() {
         Solver<ILits> solver = newMiniLearningHeapExpSimp();
         solver.setOrder(new VarOrderHeapRsat());
         return solver;
     }
 
     public static Solver<ILits> newMiniLearningHeapRsatExpSimpBiere() {
         Solver<ILits> solver = newMiniLearningHeapRsatExpSimp();
         solver.setRestartStrategy(new ArminRestarts());
         solver.setSearchParams(new SearchParams(1.1, 100));
         return solver;
     }
 
     public static Solver<ILits> newMiniLearningHeapRsatExpSimpLuby() {
         Solver<ILits> solver = newMiniLearningHeapRsatExpSimp();
         solver.setRestartStrategy(new LubyRestarts());
         return solver;
     }
 
     /**
      * @param n
      *                the maximal size of the clauses to learn as a percentage
      *                of the initial number of variables
      * @return a "minilearning" solver learning clauses of size smaller than n
      *         of the total number of variables
      */
     public static Solver<ILits> newMiniLearning(int n) {
         return newMiniLearning(new MixedDataStructureDaniel(), n);
     }
 
     /**
      * @param dsf
      *                a specific data structure factory
      * @return a default "minilearning" solver using a specific data structure
      *         factory, learning clauses of length smaller or equals to 10 % of
      *         the number of variables.
      */
     public static <L extends ILits> Solver<L> newMiniLearning(
             DataStructureFactory<L> dsf) {
         return newMiniLearning(dsf, 10);
     }
 
     /**
      * @param dsf
      *                a specific data structure factory
      * @return a default "minilearning" solver using a specific data structure
      *         factory, learning clauses of length smaller or equals to 10 % of
      *         the number of variables and a heap based VSIDS heuristics
      */
     public static <L extends ILits> Solver<L> newMiniLearningHeap(
             DataStructureFactory<L> dsf) {
         return newMiniLearning(dsf, new VarOrderHeap<L>());
     }
 
     /**
      * @return a default minilearning solver using a specific data structure
      *         described in Lawrence Ryan thesis to handle binary clauses.
      * @see #newMiniLearning
      */
     public static Solver<ILits2> newMiniLearning2() {
         return newMiniLearning(new MixedDataStructureWithBinary());
     }
 
     public static Solver<ILits2> newMiniLearning2Heap() {
         return newMiniLearningHeap(new MixedDataStructureWithBinary());
     }
 
     /**
      * @return a default minilearning solver using a specific data structures
      *         described in Lawrence Ryan thesis to handle binary and ternary
      *         clauses.
      * @see #newMiniLearning
      */
     public static Solver<ILits23> newMiniLearning23() {
         return newMiniLearning(new MixedDataStructureWithBinaryAndTernary());
     }
 
     /**
      * @return a default minilearning SAT solver using counter-based clause
      *         representation (i.e. all the literals of a clause are watched)
      */
     public static Solver<ILits> newMiniLearningCB() {
         return newMiniLearning(new ClausalDataStructureCB());
     }
 
     /**
      * @return a default minilearning SAT solver using counter-based clause
      *         representation (i.e. all the literals of a clause are watched)
      *         for the ORIGINAL clauses and watched-literals clause
      *         representation for learnt clauses.
      */
     public static Solver<ILits> newMiniLearningCBWL() {
         return newMiniLearning(new ClausalDataStructureCBWL());
     }
 
     public static Solver<ILits2> newMiniLearning2NewOrder() {
         return newMiniLearning(new MixedDataStructureWithBinary(),
                 new MyOrder());
     }
 
     /**
      * @return a default minilearning SAT solver choosing periodically to branch
      *         on "pure watched" literals if any. (a pure watched literal l is a
      *         literal that is watched on at least one clause such that its
      *         negation is not watched at all. It is not necessarily a watched
      *         literal.)
      */
     public static Solver<ILits> newMiniLearningPure() {
         return newMiniLearning(new MixedDataStructureDaniel(), new PureOrder());
     }
 
     /**
      * @return a default minilearning SAT solver choosing periodically to branch
      *         on literal "pure in the original set of clauses" if any.
      */
     public static Solver<ILits> newMiniLearningCBWLPure() {
         return newMiniLearning(new ClausalDataStructureCBWL(), new PureOrder());
     }
 
     /**
      * @param dsf
      *                the data structure factory used to represent literals and
      *                clauses
      * @param n
      *                the maximum size of learnt clauses as percentage of the
      *                original number of variables.
      * @return a SAT solver with learning limited to clauses of length smaller
      *         or equal to n, the dsf data structure, the FirstUIP clause
      *         generator and a sort of VSIDS heuristics.
      */
     public static <L extends ILits> Solver<L> newMiniLearning(
             DataStructureFactory<L> dsf, int n) {
         LimitedLearning<L> learning = new PercentLengthLearning<L>(n);
         Solver<L> solver = new Solver<L>(new FirstUIP(), learning, dsf,
                 new VarOrder<L>(), new MiniSATRestarts());
         learning.setSolver(solver);
         return solver;
     }
 
     /**
      * @param dsf
      *                the data structure factory used to represent literals and
      *                clauses
      * @param order
      *                the heuristics
      * @return a SAT solver with learning limited to clauses of length smaller
      *         or equal to 10 percent of the total number of variables, the dsf
      *         data structure, the FirstUIP clause generator and order as
      *         heuristics.
      */
     public static <L extends ILits> Solver<L> newMiniLearning(
             DataStructureFactory<L> dsf, IOrder<L> order) {
         LimitedLearning<L> learning = new PercentLengthLearning<L>(10);
         Solver<L> solver = new Solver<L>(new FirstUIP(), learning, dsf, order,
                 new MiniSATRestarts());
         learning.setSolver(solver);
         return solver;
     }
 
     public static Solver<ILits> newMiniLearningEZSimp() {
         return newMiniLearningEZSimp(new MixedDataStructureDaniel());
     }
 
     // public static ISolver newMiniLearning2EZSimp() {
     // return newMiniLearningEZSimp(new MixedDataStructureWithBinary());
     // }
 
     public static <L extends ILits> Solver<L> newMiniLearningEZSimp(
             DataStructureFactory<L> dsf) {
         LimitedLearning<L> learning = new PercentLengthLearning<L>(10);
         Solver<L> solver = new Solver<L>(new FirstUIP(), learning, dsf,
                 new VarOrder<L>(), new MiniSATRestarts());
         learning.setSolver(solver);
         solver.setSimplifier(solver.SIMPLE_SIMPLIFICATION);
         return solver;
     }
 
     /**
      * @return a default MiniLearning without restarts.
      */
     public static Solver<ILits> newMiniLearningHeapEZSimpNoRestarts() {
         LimitedLearning<ILits> learning = new PercentLengthLearning<ILits>(10);
         Solver<ILits> solver = new Solver<ILits>(new FirstUIP(), learning,
                 new MixedDataStructureDaniel(), new SearchParams(
                         Integer.MAX_VALUE), new VarOrderHeap<ILits>(),
                 new MiniSATRestarts());
         learning.setSolver(solver);
         solver.setSimplifier(solver.SIMPLE_SIMPLIFICATION);
         return solver;
     }
 
     /**
      * @return a default MiniLearning with restarts beginning at 1000 conflicts.
      */
     public static Solver<ILits> newMiniLearningHeapEZSimpLongRestarts() {
         LimitedLearning<ILits> learning = new PercentLengthLearning<ILits>(10);
         Solver<ILits> solver = new Solver<ILits>(new FirstUIP(), learning,
                 new MixedDataStructureDaniel(), new SearchParams(1000),
                 new VarOrderHeap<ILits>(), new MiniSATRestarts());
         learning.setSolver(solver);
         solver.setSimplifier(solver.SIMPLE_SIMPLIFICATION);
         return solver;
     }
 
     /**
      * @return a SAT solver using First UIP clause generator, watched literals,
      *         VSIDS like heuristics learning only clauses having a great number
      *         of active variables, i.e. variables with an activity strictly
      *         greater than one.
      */
     public static Solver<ILits> newActiveLearning() {
         ActiveLearning<ILits> learning = new ActiveLearning<ILits>();
         Solver<ILits> s = new Solver<ILits>(new FirstUIP(), learning,
                 new MixedDataStructureDaniel(), new VarOrder<ILits>(),
                 new MiniSATRestarts());
         learning.setOrder(s.getOrder());
         learning.setSolver(s);
         return s;
     }
 
     /**
      * @return a SAT solver very close to the original MiniSAT sat solver.
      */
     public static Solver<ILits> newMiniSAT() {
         return newMiniSAT(new MixedDataStructureDaniel());
     }
 
     /**
      * @return MiniSAT without restarts.
      */
     public static Solver<ILits> newMiniSATNoRestarts() {
         MiniSATLearning<ILits> learning = new MiniSATLearning<ILits>();
         Solver<ILits> solver = new Solver<ILits>(new FirstUIP(), learning,
                 new MixedDataStructureDaniel(), new SearchParams(
                         Integer.MAX_VALUE), new VarOrder<ILits>(),
                 new MiniSATRestarts());
         learning.setDataStructureFactory(solver.getDSFactory());
         learning.setVarActivityListener(solver);
         return solver;
 
     }
 
     /**
      * @return MiniSAT with a special data structure from Lawrence Ryan thesis
      *         for managing binary clauses.
      */
     public static Solver<ILits2> newMiniSAT2() {
         return newMiniSAT(new MixedDataStructureWithBinary());
     }
 
     /**
      * @return MiniSAT with a special data structure from Lawrence Ryan thesis
      *         for managing binary and ternary clauses.
      */
     public static Solver<ILits23> newMiniSAT23() {
         return newMiniSAT(new MixedDataStructureWithBinaryAndTernary());
     }
 
     /**
      * @param dsf
      *                the data structure used for representing clauses and lits
      * @return MiniSAT the data structure dsf.
      */
     public static <L extends ILits> Solver<L> newMiniSAT(
             DataStructureFactory<L> dsf) {
         MiniSATLearning<L> learning = new MiniSATLearning<L>();
         Solver<L> solver = new Solver<L>(new FirstUIP(), learning, dsf,
                 new VarOrder<L>(), new MiniSATRestarts());
         learning.setDataStructureFactory(solver.getDSFactory());
         learning.setVarActivityListener(solver);
         return solver;
     }
 
     /**
      * @return a SAT solver very close to the original MiniSAT sat solver.
      */
     public static Solver<ILits> newMiniSATHeap() {
         return newMiniSATHeap(new MixedDataStructureDaniel());
     }
 
     /**
      * @return a SAT solver very close to the original MiniSAT sat solver
      *         including easy reason simplification.
      */
     public static Solver<ILits> newMiniSATHeapEZSimp() {
         Solver<ILits> solver = newMiniSATHeap();
         solver.setSimplifier(solver.SIMPLE_SIMPLIFICATION);
         return solver;
     }
 
     public static Solver<ILits> newMiniSATHeapExpSimp() {
         Solver<ILits> solver = newMiniSATHeap();
         solver.setSimplifier(solver.EXPENSIVE_SIMPLIFICATION);
         return solver;
     }
 
     /**
      * @return MiniSAT with a special data structure from Lawrence Ryan thesis
      *         for managing binary clauses.
      */
     public static Solver<ILits2> newMiniSAT2Heap() {
         return newMiniSATHeap(new MixedDataStructureWithBinary());
     }
 
     /**
      * @return MiniSAT with a special data structure from Lawrence Ryan thesis
      *         for managing binary and ternary clauses.
      */
     public static Solver<ILits23> newMiniSAT23Heap() {
         return newMiniSATHeap(new MixedDataStructureWithBinaryAndTernary());
     }
 
     public static <L extends ILits> Solver<L> newMiniSATHeap(
             DataStructureFactory<L> dsf) {
         MiniSATLearning<L> learning = new MiniSATLearning<L>();
         Solver<L> solver = new Solver<L>(new FirstUIP(), learning, dsf,
                 new VarOrderHeap<L>(), new MiniSATRestarts());
         learning.setDataStructureFactory(solver.getDSFactory());
         learning.setVarActivityListener(solver);
         return solver;
     }
 
     /**
      * @return MiniSAT with data structures to handle cardinality constraints.
      */
     public static Solver<ILits> newMiniCard() {
         return newMiniSAT(new CardinalityDataStructure());
     }
 
     /**
      * @return MiniSAT with Counter-based pseudo boolean constraints and clause
      *         learning.
      */
     public static Solver<ILits> newMinimalOPBMax() {
         MiniSATLearning<ILits> learning = new MiniSATLearning<ILits>();
         Solver<ILits> solver = new Solver<ILits>(new FirstUIP(), learning,
                 new PBMaxDataStructure(), new VarOrderHeap<ILits>(),
                 new MiniSATRestarts());
         learning.setDataStructureFactory(solver.getDSFactory());
         learning.setVarActivityListener(solver);
         return solver;
     }
 
     /**
      * @return MiniSAT with Counter-based pseudo boolean constraints and
      *         constraint learning.
      */
     public static Solver<ILits> newMiniOPBMax() {
         MiniSATLearning<ILits> learning = new MiniSATLearning<ILits>();
         Solver<ILits> solver = new PBSolver<ILits>(new FirstUIP(), learning,
                 new PBMaxDataStructure(), new VarOrderHeap<ILits>());
         learning.setDataStructureFactory(solver.getDSFactory());
         learning.setVarActivityListener(solver);
         return solver;
     }
 
     /**
      * @return MiniSAT with Counter-based pseudo boolean constraints and
      *         constraint learning. Clauses and cardinalities with watched
      *         literals are also handled (and learnt).
      */
     public static Solver<ILits> newMiniOPBClauseCardConstrMax() {
         MiniSATLearning<ILits> learning = new MiniSATLearning<ILits>();
         Solver<ILits> solver = new PBSolver<ILits>(new FirstUIP(), learning,
                 new PBMaxClauseCardConstrDataStructure(),
                 new VarOrderHeap<ILits>());
         learning.setDataStructureFactory(solver.getDSFactory());
         learning.setVarActivityListener(solver);
         return solver;
     }
 
     /**
      * @return MiniSAT with Counter-based pseudo boolean constraints and
      *         constraint learning. Clauses and cardinalities with watched
      *         literals are also handled (and learnt). A specific heuristics
      *         taking into account the objective value is used.
      */
     public static Solver<ILits> newMiniOPBClauseCardConstrMaxSpecificOrder() {
         MiniSATLearning<ILits> learning = new MiniSATLearning<ILits>();
         Solver<ILits> solver = new PBSolver<ILits>(new FirstUIP(), learning,
                 new PBMaxClauseCardConstrDataStructure(),
                 new VarOrderHeapObjective());
         learning.setDataStructureFactory(solver.getDSFactory());
         learning.setVarActivityListener(solver);
         return solver;
     }
 
     /**
      * @return MiniLearning with Counter-based pseudo boolean constraints and
      *         constraint learning. Clauses and cardinalities with watched
      *         literals are also handled (and learnt). A specific heuristics
      *         taking into account the objective value is used. Conflict
      *         analysis with full cutting plane inference.
      */
     public static Solver<ILits> newMiniLearningOPBClauseCardConstrMaxSpecificOrderIncremental() {
         // LimitedLearning learning = new LimitedLearning(10);
         MiniSATLearning<ILits> learning = new MiniSATLearning<ILits>();
         // LearningStrategy learning = new NoLearningButHeuristics();
         Solver<ILits> solver = new PBSolver<ILits>(new FirstUIP(), learning,
                 new PBMaxClauseCardConstrDataStructure(),
                 new VarOrderHeapObjective());
         learning.setDataStructureFactory(solver.getDSFactory());
         learning.setVarActivityListener(solver);
         return solver;
     }
 
     /**
      * @return MiniLearning with Counter-based pseudo boolean constraints and
      *         constraint learning. Clauses and cardinalities with watched
      *         literals are also handled (and learnt). A specific heuristics
      *         taking into account the objective value is used. Conflict
      *         analysis with full cutting plane inference. Only clauses are
      *         recorded.
      */
     public static Solver<ILits> newMiniLearningOPBClauseCardConstrMaxSpecificOrderIncrementalLearnJustClauses() {
         ClauseOnlyLearning<ILits> learning = new ClauseOnlyLearning<ILits>();
         Solver<ILits> solver = new PBSolver<ILits>(new FirstUIP(), learning,
                 new PBMaxClauseCardConstrDataStructure(),
                 new VarOrderHeapObjective());
         learning.setSolver(solver);
         return solver;
     }
 
     /**
      * @return MiniLearning with Counter-based pseudo boolean constraints and
      *         constraint learning. Clauses and cardinalities with watched
      *         literals are also handled (and learnt). A specific heuristics
      *         taking into account the objective value is used. Conflict
      *         analysis reduces to clauses to avoid computations
      */
     public static Solver<ILits> newMiniLearningOPBClauseCardConstrMaxSpecificOrderIncrementalReductionToClause() {
         // LimitedLearning learning = new LimitedLearning(10);
         MiniSATLearning<ILits> learning = new MiniSATLearning<ILits>();
         // LearningStrategy learning = new NoLearningButHeuristics();
         Solver<ILits> solver = new PBSolverClause(new FirstUIP(), learning,
                 new PBMaxClauseCardConstrDataStructure(),
                 new VarOrderHeapObjective());
         learning.setDataStructureFactory(solver.getDSFactory());
         learning.setVarActivityListener(solver);
         return solver;
     }
 
     /**
      * @return MiniLearning with Counter-based pseudo boolean constraints and
      *         constraint learning. Clauses and cardinalities with watched
      *         literals are also handled (and learnt). A specific heuristics
      *         taking into account the objective value is used. The PB
      *         constraints are not learnt (watched), just used for backjumping.
      */
     public static Solver<ILits> newMiniLearningOPBClauseCardConstrMaxSpecificOrderIncrementalNoLearning() {
         NoLearningButHeuristics<ILits> learning = new NoLearningButHeuristics<ILits>();
         // SearchParams params = new SearchParams(1.1,100);
         Solver<ILits> solver = new PBSolver<ILits>(new FirstUIP(), learning,
                 new PBMaxClauseCardConstrDataStructure(),
                 new VarOrderHeapObjective());
         learning.setSolver(solver);
         learning.setVarActivityListener(solver);
         return solver;
     }
 
     /**
      * @return MiniLearning with Counter-based pseudo boolean constraints and
      *         constraint learning. Clauses and cardinalities with watched
      *         literals are also handled (and learnt). A specific heuristics
      *         taking into account the objective value is used. Conflict
      *         analysis uses fusion rule
      */
     public static Solver<ILits> newMiniLearningOPBClauseCardConstrMaxSpecificOrderIncrementalMerging() {
         // LimitedLearning learning = new LimitedLearning(10);
         MiniSATLearning<ILits> learning = new MiniSATLearning<ILits>();
         // LearningStrategy learning = new NoLearningButHeuristics();
         Solver<ILits> solver = new PBSolverMerging(new FirstUIP(), learning,
                 new PBMaxClauseCardConstrDataStructure(),
                 new VarOrderHeapObjective());
         learning.setDataStructureFactory(solver.getDSFactory());
         learning.setVarActivityListener(solver);
         return solver;
     }
 
     public static Solver<ILits> newMinimalOPBClauseCardConstrMaxSpecificOrder() {
         MiniSATLearning<ILits> learning = new MiniSATLearning<ILits>();
         Solver<ILits> solver = new Solver<ILits>(new FirstUIP(), learning,
                 new PBMaxClauseCardConstrDataStructure(),
                 new VarOrderHeapObjective(), new MiniSATRestarts());
         learning.setDataStructureFactory(solver.getDSFactory());
         learning.setVarActivityListener(solver);
         return solver;
     }
 
     /**
      * @return MiniSAT with Counter-based pseudo boolean constraints and
      *         constraint learning. Clauses and cardinalities with watched
      *         literals are also handled (and learnt). A reduction of
      *         PB-constraints to clauses is made in order to simplify cutting
      *         planes.
      */
     public static Solver<ILits> newMiniOPBClauseCardConstrMaxReduceToClause() {
         MiniSATLearning<ILits> learning = new MiniSATLearning<ILits>();
         Solver<ILits> solver = new PBSolverClause(new FirstUIP(), learning,
                 new PBMaxClauseCardConstrDataStructure(),
                 new VarOrderHeap<ILits>());
         learning.setDataStructureFactory(solver.getDSFactory());
         learning.setVarActivityListener(solver);
         return solver;
     }
 
     /**
      * @return MiniSAT with Counter-based pseudo boolean constraints and
      *         constraint learning. Clauses and cardinalities with watched
      *         literals are also handled (and learnt). A reduction of
      *         PB-constraints to cardinalities is made in order to simplify
      *         cutting planes.
      */
     // public static ISolver newMiniOPBClauseCardConstrMaxReduceToCard() {
     // MiniSATLearning learning = new MiniSATLearning();
     // Solver solver = new PBSolverCard(new FirstUIP(), learning,
     // new PBMaxClauseCardConstrDataStructure(), new VarOrderHeap());
     // learning.setDataStructureFactory(solver.getDSFactory());
     // learning.setVarActivityListener(solver);
     // return solver;
     // }
     /**
      * @return MiniSAT with Counter-based pseudo boolean constraints and
      *         constraint learning. Clauses and cardinalities with watched
      *         literals are also handled (and learnt). a pre-processing is
      *         applied which adds implied clauses from PB-constraints.
      */
     public static Solver<ILits> newMiniOPBClauseCardConstrMaxImplied() {
         MiniSATLearning<ILits> learning = new MiniSATLearning<ILits>();
         Solver<ILits> solver = new PBSolverWithImpliedClause(new FirstUIP(),
                 learning, new PBMaxClauseCardConstrDataStructure(),
                 new VarOrderHeap<ILits>());
         learning.setDataStructureFactory(solver.getDSFactory());
         learning.setVarActivityListener(solver);
         return solver;
     }
 
     /**
      * @return MiniSAT with Counter-based pseudo boolean constraints,
      *         counter-based cardinalities, watched clauses and constraint
      *         learning. methods isAssertive() and getBacktrackLevel() are
      *         totally incremental. Conflicts for PB-constraints use a Map
      *         structure
      */
     public static Solver<ILits> newMiniOPBClauseAtLeastConstrMax() {
         MiniSATLearning<ILits> learning = new MiniSATLearning<ILits>();
         Solver<ILits> solver = new PBSolver<ILits>(new FirstUIP(), learning,
                 new PBMaxClauseAtLeastConstrDataStructure(),
                 new VarOrderHeap<ILits>());
         learning.setDataStructureFactory(solver.getDSFactory());
         learning.setVarActivityListener(solver);
         return solver;
     }
 
     /**
      * @return MiniSAT with Counter-based pseudo boolean constraints and
      *         clauses, watched cardinalities, and constraint learning.
      */
     public static Solver<ILits> newMiniOPBCounterBasedClauseCardConstrMax() {
         MiniSATLearning<ILits> learning = new MiniSATLearning<ILits>();
         Solver<ILits> solver = new PBSolver<ILits>(new FirstUIP(), learning,
                 new PBMaxCBClauseCardConstrDataStructure(),
                 new VarOrderHeap<ILits>());
         learning.setDataStructureFactory(solver.getDSFactory());
         learning.setVarActivityListener(solver);
         return solver;
     }
 
     /**
      * @return MiniSAT with WL-based pseudo boolean constraints and clause
      *         learning.
      */
     public static Solver<ILits> newMinimalOPBMin() {
         MiniSATLearning<ILits> learning = new MiniSATLearning<ILits>();
         Solver<ILits> solver = new Solver<ILits>(new FirstUIP(), learning,
                 new PBMinDataStructure(), new VarOrderHeap<ILits>(),
                 new MiniSATRestarts());
         learning.setDataStructureFactory(solver.getDSFactory());
         learning.setVarActivityListener(solver);
         return solver;
     }
 
     /**
      * @return MiniSAT with WL-based pseudo boolean constraints and constraint
      *         learning.
      */
     public static Solver<ILits> newMiniOPBMin() {
         MiniSATLearning<ILits> learning = new MiniSATLearning<ILits>();
         Solver<ILits> solver = new PBSolver<ILits>(new FirstUIP(), learning,
                 new PBMinDataStructure(), new VarOrderHeap<ILits>());
         learning.setDataStructureFactory(solver.getDSFactory());
         learning.setVarActivityListener(solver);
         return solver;
     }
 
     /**
      * @return MiniSAT with WL-based pseudo boolean constraints and clause
      *         learning.
      */
     public static Solver<ILits> newMinimalOPBMinPueblo() {
         MiniSATLearning<ILits> learning = new MiniSATLearning<ILits>();
         Solver<ILits> solver = new Solver<ILits>(new FirstUIP(), learning,
                 new PuebloPBMinDataStructure(), new VarOrderHeap<ILits>(),
                 new MiniSATRestarts());
         learning.setDataStructureFactory(solver.getDSFactory());
         learning.setVarActivityListener(solver);
         return solver;
     }
 
     /**
      * @return MiniSAT with WL-based pseudo boolean constraints and constraint
      *         learning.
      */
     public static Solver<ILits> newMiniOPBMinPueblo() {
         MiniSATLearning<ILits> learning = new MiniSATLearning<ILits>();
         Solver<ILits> solver = new PBSolver<ILits>(new FirstUIP(), learning,
                 new PuebloPBMinDataStructure(), new VarOrderHeap<ILits>());
         learning.setDataStructureFactory(solver.getDSFactory());
         learning.setVarActivityListener(solver);
         return solver;
     }
 
     /**
      * @return MiniSAT with WL-based pseudo boolean constraints and clauses,
      *         cardinalities, and constraint learning.
      */
     public static Solver<ILits> newMiniOPBClauseCardMinPueblo() {
         MiniSATLearning<ILits> learning = new MiniSATLearning<ILits>();
         Solver<ILits> solver = new PBSolver<ILits>(new FirstUIP(), learning,
                 new PuebloPBMinClauseCardConstrDataStructure(),
                 new VarOrderHeap<ILits>());
         learning.setDataStructureFactory(solver.getDSFactory());
         learning.setVarActivityListener(solver);
         return solver;
     }
 
     /**
      * @return MiniSAT with WL-based pseudo boolean constraints and clauses,
      *         cardinalities, and constraint learning.
      */
     public static Solver<ILits> newMiniOPBClauseCardMin() {
         MiniSATLearning<ILits> learning = new MiniSATLearning<ILits>();
         Solver<ILits> solver = new PBSolver<ILits>(new FirstUIP(), learning,
                 new PBMinClauseCardConstrDataStructure(),
                 new VarOrderHeap<ILits>());
         learning.setDataStructureFactory(solver.getDSFactory());
         learning.setVarActivityListener(solver);
         return solver;
     }
 
     /**
      * @return MiniSAT with WL-based pseudo boolean constraints and clauses,
      *         counter-based cardinalities, and constraint learning.
      */
     public static Solver<ILits> newMiniOPBClauseAtLeastMinPueblo() {
         MiniSATLearning<ILits> learning = new MiniSATLearning<ILits>();
         Solver<ILits> solver = new PBSolver<ILits>(new FirstUIP(), learning,
                 new PuebloPBMinClauseAtLeastConstrDataStructure(),
                 new VarOrderHeap<ILits>());
         learning.setDataStructureFactory(solver.getDSFactory());
         learning.setVarActivityListener(solver);
         return solver;
     }
 
     /**
      * @return MiniSAT with decision UIP clause generator.
      */
     public static Solver<ILits> newRelsat() {
         MiniSATLearning<ILits> learning = new MiniSATLearning<ILits>();
         Solver<ILits> solver = new Solver<ILits>(new DecisionUIP(), learning,
                 new MixedDataStructureDaniel(), new VarOrderHeap<ILits>(),
                 new MiniSATRestarts());
         learning.setDataStructureFactory(solver.getDSFactory());
         learning.setVarActivityListener(solver);
         return solver;
     }
 
     /**
      * @return MiniSAT with VSIDS heuristics, FirstUIP clause generator for
      *         backjumping but no learning.
      */
     public static Solver<ILits> newBackjumping() {
         NoLearningButHeuristics<ILits> learning = new NoLearningButHeuristics<ILits>();
         Solver<ILits> solver = new Solver<ILits>(new FirstUIP(), learning,
                 new MixedDataStructureDaniel(), new VarOrderHeap<ILits>(),
                 new MiniSATRestarts());
         learning.setVarActivityListener(solver);
         return solver;
     }
 
     /**
      * @return a SAT solver with learning limited to clauses of length smaller
      *         or equals to 3, with a specific data structure for binary and
      *         ternary clauses as found in Lawrence Ryan thesis, without
      *         restarts, with a Jeroslow/Wang kind of heuristics.
      */
     public static Solver<ILits23> newMini3SAT() {
         LimitedLearning<ILits23> learning = new FixedLengthLearning<ILits23>(3);
         Solver<ILits23> solver = new Solver<ILits23>(new FirstUIP(), learning,
                 new MixedDataStructureWithBinaryAndTernary(), new SearchParams(
                         Integer.MAX_VALUE), new JWOrder(),
                 new MiniSATRestarts());
         learning.setSolver(solver);
         return solver;
     }
 
     /**
      * @return a Mini3SAT with full learning.
      * @see #newMini3SAT()
      */
     public static Solver<ILits23> newMini3SATb() {
         MiniSATLearning<ILits23> learning = new MiniSATLearning<ILits23>();
         Solver<ILits23> solver = new Solver<ILits23>(new FirstUIP(), learning,
                 new MixedDataStructureWithBinaryAndTernary(), new SearchParams(
                         Integer.MAX_VALUE), new JWOrder(),
                 new MiniSATRestarts());
         learning.setDataStructureFactory(solver.getDSFactory());
         learning.setVarActivityListener(solver);
         return solver;
     }
 
     /**
      * Builds a SAT solver for the MAX sat evaluation. Full clause learning, no
      * restarts,
      * 
      * @return a
      */
     public static Solver<ILits> newMiniMaxSAT() {
         MiniSATLearning<ILits> learning = new MiniSATLearning<ILits>();
         Solver<ILits> solver = new Solver<ILits>(new FirstUIP(), learning,
                 new MixedDataStructureDanielCBWL(), new SearchParams(1.2,
                         100000), new VarOrderHeap<ILits>(),
                 new MiniSATRestarts());
         learning.setDataStructureFactory(solver.getDSFactory());
         learning.setVarActivityListener(solver);
         return solver;
     }
 
     /**
      * Default solver of the SolverFactory. This solver is meant to be used on
      * challenging SAT benchmarks.
      * 
      * @return the best "general purpose" SAT solver available in the factory.
      * @see #defaultSolver() the same method, polymorphic, to be called from an
      *      instance of ASolverFactory.
      */
     public static ISolver newDefault() {
         return newMiniLearningHeapRsatExpSimpBiere();
     }
 
     @Override
     public ISolver defaultSolver() {
         return newDefault();
     }
 
     /**
      * Small footprint SAT solver.
      * 
      * @return a SAT solver suitable for solving small/easy SAT benchmarks.
      * @see #lightSolver() the same method, polymorphic, to be called from an
      *      instance of ASolverFactory.
      */
     public static ISolver newLight() {
         return newMini3SAT();
     }
 
     @Override
     public ISolver lightSolver() {
         return newLight();
     }
 
     public static ISolver newDimacsOutput() {
         return new DimacsOutputSolver();
     }
 
 }