org.sat4j.csp
Class SolverFactory

java.lang.Object
  extended by org.sat4j.core.ASolverFactory<ISolver>
      extended by org.sat4j.csp.SolverFactory
All Implemented Interfaces:
java.io.Serializable

public class SolverFactory
extends ASolverFactory<ISolver>

User friendly access to pre-constructed solvers.

Author:
leberre
See Also:
Serialized Form

Method Summary
 ISolver defaultSolver()
           
static SolverFactory instance()
          Access to the single instance of the factory.
 ISolver lightSolver()
           
static ISolver newDefault()
          Default solver of the SolverFactory.
static ISolver newDimacsOutput()
           
static ISolver newLight()
          Small footprint SAT solver.
static
<L extends ILits>
Solver<L,DataStructureFactory<L>>
newMiniSAT(DataStructureFactory<L> dsf)
           
 
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.

newMiniSAT

public static <L extends ILits> Solver<L,DataStructureFactory<L>> newMiniSAT(DataStructureFactory<L> dsf)
Parameters:
dsf - the data structure used for representing clauses and lits
Returns:
MiniSAT the data structure dsf.

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()
Specified by:
defaultSolver in class ASolverFactory<ISolver>

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()
Specified by:
lightSolver in class ASolverFactory<ISolver>

newDimacsOutput

public static ISolver newDimacsOutput()


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