org.sat4j.minisat
Class SolverFactory

java.lang.Object
  extended by org.sat4j.core.ASolverFactory<ISolver>
      extended by 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
 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 ICDCL<DataStructureFactory> newBestSingleWL()
           
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> 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 ICDCL<DataStructureFactory> newMiniLearningPure()
           
static Solver<DataStructureFactory> newMiniSATHeap()
           
static Solver<DataStructureFactory> newMiniSATHeap(DataStructureFactory dsf)
           
static ICDCL<DataStructureFactory> newMiniSATHeapExpSimp()
           
static ICDCL<DataStructureFactory> newMiniSATHeapEZSimp()
           
static ISolver newMinOneSolver()
           
 
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()

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

newBestSingleWL

public static ICDCL<DataStructureFactory> newBestSingleWL()
Since:
2.2

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

newMiniLearningPure

public static ICDCL<DataStructureFactory> 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.)

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()


Copyright © 2012 Centre de Recherche en Informatique de Lens (CRIL). All Rights Reserved.