org.sat4j.minisat
Class SolverFactory

java.lang.Object
  extended by org.sat4j.core.ASolverFactory
      extended by org.sat4j.minisat.SolverFactory

public class SolverFactory
extends ASolverFactory

User friendly access to pre-constructed solvers.

Author:
leberre

Constructor Summary
SolverFactory()
           
 
Method Summary
 ISolver defaultSolver()
          To obtain the default solver of the library.
 ISolver lightSolver()
          To obtain a solver that is suitable for solving many small instances of SAT problems.
static ISolver newActiveLearning()
           
static ISolver newBackjumping()
           
static ISolver newMini3SAT()
           
static ISolver newMini3SATb()
           
static ISolver newMiniCard()
           
static ISolver newMiniLearning()
           
static ISolver newMiniLearning(DataStructureFactory dsf)
           
static ISolver newMiniLearning(DataStructureFactory dsf, int n)
           
static ISolver newMiniLearning(DataStructureFactory dsf, IOrder order)
           
static ISolver newMiniLearning(int n)
           
static ISolver newMiniLearning2()
           
static ISolver newMiniLearning23()
           
static ISolver newMiniLearning2Heap()
           
static ISolver newMiniLearning2NewOrder()
           
static ISolver newMiniLearningCB()
           
static ISolver newMiniLearningCBWL()
           
static ISolver newMiniLearningCBWLPure()
           
static ISolver newMiniLearningEZSimp()
           
static ISolver newMiniLearningEZSimp(DataStructureFactory dsf)
           
static ISolver newMiniLearningHeap()
           
static ISolver newMiniLearningHeap(DataStructureFactory dsf)
           
static ISolver newMiniLearningHeapEZSimp()
           
static ISolver newMiniLearningNoRestarts()
           
static ISolver newMiniLearningPure()
           
static ISolver newMinimalOPBMax()
           
static ISolver newMinimalOPBMin()
           
static ISolver newMiniOPBMax()
           
static ISolver newMiniOPBMin()
           
static ISolver newMiniSAT()
           
static ISolver newMiniSAT(DataStructureFactory dsf)
           
static ISolver newMiniSAT2()
           
static ISolver newMiniSAT23()
           
static ISolver newMiniSAT23Heap()
           
static ISolver newMiniSAT2Heap()
           
static ISolver newMiniSATHeap()
           
static ISolver newMiniSATHeap(DataStructureFactory dsf)
           
static ISolver newMiniSATNoRestarts()
           
static ISolver newRelsat()
           
 
Methods inherited from class org.sat4j.core.ASolverFactory
createSolverByName, solverNames
 
Methods inherited from class java.lang.Object
equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Constructor Detail

SolverFactory

public SolverFactory()
Method Detail

newMiniLearning

public static ISolver newMiniLearning()
Returns:
a "default" "minilearning" solver learning clauses of size smaller than 10 % of the total number of variables

newMiniLearningHeap

public static ISolver newMiniLearningHeap()
Returns:
a "default" "minilearning" solver learning clauses of size smaller than 10 % of the total number of variables with a heap based var order.

newMiniLearningHeapEZSimp

public static ISolver newMiniLearningHeapEZSimp()

newMiniLearning

public static ISolver newMiniLearning(int n)
Parameters:
n - the maximal size of the clauses to learn as a percentage of the initial number of variables
Returns:
a "minilearning" solver learning clauses of size smaller than n of the total number of variables

newMiniLearning

public static ISolver newMiniLearning(DataStructureFactory dsf)
Parameters:
dsf - a specific data structure factory
Returns:
a default "minilearning" solver using a specific data structure factory, learning clauses of length smaller or equals to 10 % of the number of variables.

newMiniLearningHeap

public static ISolver newMiniLearningHeap(DataStructureFactory dsf)
Parameters:
dsf - a specific data structure factory
Returns:
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

newMiniLearning2

public static ISolver newMiniLearning2()
Returns:
a default minilearning solver using a specific data structure described in Lawrence Ryan thesis to handle binary clauses.
See Also:
newMiniLearning()

newMiniLearning2Heap

public static ISolver newMiniLearning2Heap()

newMiniLearning23

public static ISolver newMiniLearning23()
Returns:
a default minilearning solver using a specific data structures described in Lawrence Ryan thesis to handle binary and ternary clauses.
See Also:
newMiniLearning()

newMiniLearningCB

public static ISolver newMiniLearningCB()
Returns:
a default minilearning SAT solver using counter-based clause representation (i.e. all the literals of a clause are watched)

newMiniLearningCBWL

public static ISolver newMiniLearningCBWL()
Returns:
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.

newMiniLearning2NewOrder

public static ISolver newMiniLearning2NewOrder()

newMiniLearningPure

public static ISolver newMiniLearningPure()
Returns:
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.)

newMiniLearningCBWLPure

public static ISolver newMiniLearningCBWLPure()
Returns:
a default minilearning SAT solver choosing periodically to branch on literal "pure in the original set of clauses" if any.

newMiniLearning

public static ISolver newMiniLearning(DataStructureFactory dsf,
                                      int n)
Parameters:
dsf - the data structure factory used to represent literals and clauses
n - the maximum size of learnt clauses as percentage of the original number of variables.
Returns:
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.

newMiniLearning

public static ISolver newMiniLearning(DataStructureFactory dsf,
                                      IOrder order)
Parameters:
dsf - the data structure factory used to represent literals and clauses
order - the heuristics
Returns:
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.

newMiniLearningEZSimp

public static ISolver newMiniLearningEZSimp()

newMiniLearningEZSimp

public static ISolver newMiniLearningEZSimp(DataStructureFactory dsf)

newMiniLearningNoRestarts

public static ISolver newMiniLearningNoRestarts()
Returns:
a default MiniLearning without restarts.

newActiveLearning

public static ISolver newActiveLearning()
Returns:
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.

newMiniSAT

public static ISolver newMiniSAT()
Returns:
a SAT solver very close to the original MiniSAT sat solver.

newMiniSATNoRestarts

public static ISolver newMiniSATNoRestarts()
Returns:
MiniSAT without restarts.

newMiniSAT2

public static ISolver newMiniSAT2()
Returns:
MiniSAT with a special data structure from Lawrence Ryan thesis for managing binary clauses.

newMiniSAT23

public static ISolver newMiniSAT23()
Returns:
MiniSAT with a special data structure from Lawrence Ryan thesis for managing binary and ternary clauses.

newMiniSAT

public static ISolver newMiniSAT(DataStructureFactory dsf)
Parameters:
dsf - the data structure used for representing clauses and lits
Returns:
MiniSAT the data structure dsf.

newMiniSATHeap

public static ISolver newMiniSATHeap()
Returns:
a SAT solver very close to the original MiniSAT sat solver.

newMiniSAT2Heap

public static ISolver newMiniSAT2Heap()
Returns:
MiniSAT with a special data structure from Lawrence Ryan thesis for managing binary clauses.

newMiniSAT23Heap

public static ISolver newMiniSAT23Heap()
Returns:
MiniSAT with a special data structure from Lawrence Ryan thesis for managing binary and ternary clauses.

newMiniSATHeap

public static ISolver newMiniSATHeap(DataStructureFactory dsf)

newMiniCard

public static ISolver newMiniCard()
Returns:
MiniSAT with data strcutures to handle cardinality constraints.

newMinimalOPBMax

public static ISolver newMinimalOPBMax()
Returns:
MiniSAT with Counter-based pseudo boolean constraints and clause learning.

newMiniOPBMax

public static ISolver newMiniOPBMax()
Returns:
MiniSAT with Counter-based pseudo boolean constraints and constraint learning.

newMinimalOPBMin

public static ISolver newMinimalOPBMin()
Returns:
MiniSAT with WL-based pseudo boolean constraints and clause learning.

newMiniOPBMin

public static ISolver newMiniOPBMin()
Returns:
MiniSAT with WL-based pseudo boolean constraints and constraint learning.

newRelsat

public static ISolver newRelsat()
Returns:
MiniSAT with decision UIP clause generator.

newBackjumping

public static ISolver newBackjumping()
Returns:
MiniSAT with VSIDS heuristics, FirstUIP clause generator for backjumping but no learning.

newMini3SAT

public static ISolver newMini3SAT()
Returns:
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.

newMini3SATb

public static ISolver newMini3SATb()
Returns:
a Mini3SAT with full learning.
See Also:
newMini3SAT()

defaultSolver

public ISolver defaultSolver()
Description copied from class: ASolverFactory
To obtain the default solver of the library. The solver is suitable to solve huge SAT benchmarks. It should reflect state-of-the-art SAT technologies. For solving small/easy SAT benchmarks, use lightSolver() instead.

Specified by:
defaultSolver in class ASolverFactory
Returns:
a solver from the factory
See Also:
ASolverFactory.lightSolver()

lightSolver

public ISolver lightSolver()
Description copied from class: ASolverFactory
To obtain a solver that is suitable for solving many small instances of SAT problems. The solver is not using sophisticated but costly reasoning and avoids to allocate too much memory. For solving bigger SAT benchmarks, use defaultSolver() instead.

Specified by:
lightSolver in class ASolverFactory
Returns:
a solver from the factory
See Also:
ASolverFactory.defaultSolver()