public class SolverFactory extends ASolverFactory<ISolver>
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 ISolver |
newCuttingPlanes() |
static ISolver |
newDefault()
Default solver of the SolverFactory.
|
static ISolver |
newDimacsOutput() |
static ISolver |
newLight()
Small footprint SAT solver.
|
static <L extends ILits> |
newMiniSAT(DataStructureFactory dsf) |
static ISolver |
newSAT() |
static ISolver |
newUNSAT() |
createSolverByName, solverNames
public static SolverFactory instance()
public static <L extends ILits> Solver<DataStructureFactory> newMiniSAT(DataStructureFactory dsf)
dsf
- the data structure used for representing clauses and litspublic static ISolver newDefault()
the same method, polymorphic, to be called from an
instance of ASolverFactory.
public static ISolver newSAT()
public static ISolver newUNSAT()
public static ISolver newCuttingPlanes()
public ISolver defaultSolver()
ASolverFactory
defaultSolver
in class ASolverFactory<ISolver>
ASolverFactory.lightSolver()
public static ISolver newLight()
the same method, polymorphic, to be called from an
instance of ASolverFactory.
public ISolver lightSolver()
ASolverFactory
lightSolver
in class ASolverFactory<ISolver>
ASolverFactory.defaultSolver()
public static ISolver newDimacsOutput()
Copyright © 2013 Centre de Recherche en Informatique de Lens (CRIL). All Rights Reserved.