SolverFactory (SAT4J core 2.3.4 API)

java.lang.Object
- org.sat4j.core.ASolverFactory<ISolver>
- - org.sat4j.minisat.SolverFactory

All Implemented Interfaces:

Serializable
```
public final class SolverFactory
extends ASolverFactory<ISolver>
```
User friendly access to pre-constructed solvers.

Author:

leberre

See Also:
Serialized Form

Method Summary

Methods
Modifier and Type	Method and Description
`ISolver`	`defaultSolver()` To obtain the default solver of the library.
`static SolverFactory`	`instance()` Access to the single instance of the factory.
`ISolver`	`lightSolver()` To obtain a solver that is suitable for solving many small instances of SAT problems.
`static ICDCL<MixedDataStructureDanielWL>`	`newBackjumping()`
`static ICDCL<DataStructureFactory>`	`newBest17()`
`static ICDCL<DataStructureFactory>`	`newBestHT()`
`static Solver<DataStructureFactory>`	`newBestWL()`
`static ISolver`	`newDefault()` Default solver of the SolverFactory.
`static ICDCL<DataStructureFactory>`	`newDefaultAutoErasePhaseSaving()`
`static ICDCL<DataStructureFactory>`	`newDefaultMS21PhaseSaving()`
`static ISolver`	`newDimacsOutput()`
`static Solver<DataStructureFactory>`	`newGlucose()`
`static ICDCL<DataStructureFactory>`	`newGlucose21()`
`static ICDCL<DataStructureFactory>`	`newGreedySolver()`
`static ISolver`	`newLight()` Small footprint SAT solver.
`static Solver<DataStructureFactory>`	`newMiniLearning(DataStructureFactory dsf, IOrder order)`
`static Solver<DataStructureFactory>`	`newMiniLearningHeap()`
`static Solver<DataStructureFactory>`	`newMiniLearningHeap(DataStructureFactory dsf)`
`static Solver<DataStructureFactory>`	`newMiniLearningHeapExpSimp()`
`static ICDCL<DataStructureFactory>`	`newMiniLearningHeapEZSimp()`
`static ICDCL<DataStructureFactory>`	`newMiniLearningHeapEZSimpLongRestarts()`
`static ICDCL<DataStructureFactory>`	`newMiniLearningHeapEZSimpNoRestarts()`
`static Solver<DataStructureFactory>`	`newMiniLearningHeapRsatExpSimp()`
`static Solver<DataStructureFactory>`	`newMiniLearningHeapRsatExpSimpBiere()`
`static ICDCL<DataStructureFactory>`	`newMiniLearningHeapRsatExpSimpLuby()`
`static Solver<DataStructureFactory>`	`newMiniSATHeap()`
`static Solver<DataStructureFactory>`	`newMiniSATHeap(DataStructureFactory dsf)`
`static ICDCL<DataStructureFactory>`	`newMiniSATHeapExpSimp()`
`static ICDCL<DataStructureFactory>`	`newMiniSATHeapEZSimp()`
`static ISolver`	`newMinOneSolver()`
`static ISolver`	`newParallel()`
`static Solver`	`newSAT()` That solver is expected to perform better on satisfiable benchmarks.
`static ISolver`	`newSATUNSAT()` Two solvers are running in //: one for solving SAT instances, the other one for solving unsat instances.
`static ISolver`	`newStatistics()`
`static Solver`	`newUNSAT()` That solver is expected to perform better on unsatisfiable benchmarks.

Methods inherited from class org.sat4j.core.ASolverFactory
createSolverByName, solverNames

Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

- Method Detail
  - instance
```
public static SolverFactory instance()
```
    Access to the single instance of the factory.
    
    Returns:
    the singleton of that class.
  - newMiniLearningHeap
```
public static Solver<DataStructureFactory> 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 ICDCL<DataStructureFactory> newMiniLearningHeapEZSimp()
```
  - newMiniLearningHeapExpSimp
```
public static Solver<DataStructureFactory> newMiniLearningHeapExpSimp()
```
  - newMiniLearningHeapRsatExpSimp
```
public static Solver<DataStructureFactory> newMiniLearningHeapRsatExpSimp()
```
  - newMiniLearningHeapRsatExpSimpBiere
```
public static Solver<DataStructureFactory> newMiniLearningHeapRsatExpSimpBiere()
```
  - newMiniLearningHeapRsatExpSimpLuby
```
public static ICDCL<DataStructureFactory> newMiniLearningHeapRsatExpSimpLuby()
```
  - newGlucose21
```
public static ICDCL<DataStructureFactory> newGlucose21()
```
  - newGreedySolver
```
public static ICDCL<DataStructureFactory> newGreedySolver()
```
    Since:
    
    2.2
  - newDefaultAutoErasePhaseSaving
```
public static ICDCL<DataStructureFactory> newDefaultAutoErasePhaseSaving()
```
    Since:
    
    2.2
  - newDefaultMS21PhaseSaving
```
public static ICDCL<DataStructureFactory> newDefaultMS21PhaseSaving()
```
    Since:
    
    2.2.3
  - newBestWL
```
public static Solver<DataStructureFactory> newBestWL()
```
    Since:
    
    2.1
  - newBestHT
```
public static ICDCL<DataStructureFactory> newBestHT()
```
    Since:
    
    2.1
  - newBest17
```
public static ICDCL<DataStructureFactory> newBest17()
```
    Since:
    
    2.2
  - newGlucose
```
public static Solver<DataStructureFactory> newGlucose()
```
    Since:
    
    2.1
  - newMiniLearningHeap
```
public static Solver<DataStructureFactory> 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
  - newMiniLearning
```
public static Solver<DataStructureFactory> 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.
  - newMiniLearningHeapEZSimpNoRestarts
```
public static ICDCL<DataStructureFactory> newMiniLearningHeapEZSimpNoRestarts()
```
    Returns:
    a default MiniLearning without restarts.
  - newMiniLearningHeapEZSimpLongRestarts
```
public static ICDCL<DataStructureFactory> newMiniLearningHeapEZSimpLongRestarts()
```
    Returns:
    a default MiniLearning with restarts beginning at 1000 conflicts.
  - newMiniSATHeap
```
public static Solver<DataStructureFactory> newMiniSATHeap()
```
    Returns:
    a SAT solver very close to the original MiniSAT sat solver.
  - newMiniSATHeapEZSimp
```
public static ICDCL<DataStructureFactory> newMiniSATHeapEZSimp()
```
    Returns:
    a SAT solver very close to the original MiniSAT sat solver including easy reason simplification.
  - newMiniSATHeapExpSimp
```
public static ICDCL<DataStructureFactory> newMiniSATHeapExpSimp()
```
  - newMiniSATHeap
```
public static Solver<DataStructureFactory> newMiniSATHeap(DataStructureFactory dsf)
```
  - newBackjumping
```
public static ICDCL<MixedDataStructureDanielWL> newBackjumping()
```
    Returns:
    MiniSAT with VSIDS heuristics, FirstUIP clause generator for backjumping but no learning.
  - newMinOneSolver
```
public static ISolver newMinOneSolver()
```
    Returns:
    a solver computing models with a minimum number of satisfied literals.
  - newDefault
```
public static ISolver newDefault()
```
    Default solver of the SolverFactory. This solver is meant to be used on challenging SAT benchmarks.
    
    Returns:
    the best "general purpose" SAT solver available in the factory.
    See Also:
    the same method, polymorphic, to be called from an instance of ASolverFactory.
  - 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<ISolver>
    
    Returns:
    a solver from the factory
    See Also:
    ASolverFactory.lightSolver()
  - newLight
```
public static ISolver newLight()
```
    Small footprint SAT solver.
    
    Returns:
    a SAT solver suitable for solving small/easy SAT benchmarks.
    See Also:
    the same method, polymorphic, to be called from an instance of ASolverFactory.
  - 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<ISolver>
    
    Returns:
    a solver from the factory
    See Also:
    ASolverFactory.defaultSolver()
  - newDimacsOutput
```
public static ISolver newDimacsOutput()
```
  - newStatistics
```
public static ISolver newStatistics()
```
  - newParallel
```
public static ISolver newParallel()
```
  - newSATUNSAT
```
public static ISolver newSATUNSAT()
```
    Two solvers are running in //: one for solving SAT instances, the other one for solving unsat instances.
    
    Returns:
    a parallel solver for both SAT and UNSAT problems.
  - newSAT
```
public static Solver newSAT()
```
    That solver is expected to perform better on satisfiable benchmarks.
    
    Returns:
    a solver for satisfiable benchmarks.
  - newUNSAT
```
public static Solver newUNSAT()
```
    That solver is expected to perform better on unsatisfiable benchmarks.
    
    Returns:
    a solver for unsatisfiable benchmarks.

Class SolverFactory

Method Summary

Methods inherited from class org.sat4j.core.ASolverFactory

Methods inherited from class java.lang.Object

Method Detail

instance

newMiniLearningHeap

newMiniLearningHeapEZSimp

newMiniLearningHeapExpSimp

newMiniLearningHeapRsatExpSimp

newMiniLearningHeapRsatExpSimpBiere

newMiniLearningHeapRsatExpSimpLuby

newGlucose21

newGreedySolver

newDefaultAutoErasePhaseSaving

newDefaultMS21PhaseSaving

newBestWL

newBestHT

newBest17

newGlucose

newMiniLearningHeap

newMiniLearning

newMiniLearningHeapEZSimpNoRestarts

newMiniLearningHeapEZSimpLongRestarts

newMiniSATHeap

newMiniSATHeapEZSimp

newMiniSATHeapExpSimp

newMiniSATHeap

newBackjumping

newMinOneSolver

newDefault

defaultSolver

newLight

lightSolver

newDimacsOutput

newStatistics

newParallel

newSATUNSAT

newSAT

newUNSAT