org.sat4j.csp

Class SolverFactory

java.lang.Object

org.sat4j.core.ASolverFactory<org.sat4j.specs.ISolver>

org.sat4j.csp.SolverFactory

All Implemented Interfaces:

Serializable

public class SolverFactory
extends org.sat4j.core.ASolverFactory<org.sat4j.specs.ISolver>

User friendly access to pre-constructed solvers.

Author:

leberre

See Also:

Serialized Form

Method Summary

Methods

Modifier and Type	Method and Description
org.sat4j.specs.ISolver	defaultSolver()
static SolverFactory	instance() Access to the single instance of the factory.
org.sat4j.specs.ISolver	lightSolver()
static org.sat4j.specs.ISolver	newCuttingPlanes()
static org.sat4j.specs.ISolver	newDefault() Default solver of the SolverFactory.
static org.sat4j.specs.ISolver	newDimacsOutput()
static org.sat4j.specs.ISolver	newLight() Small footprint SAT solver.
static <L extends org.sat4j.minisat.core.ILits> org.sat4j.minisat.core.Solver<org.sat4j.minisat.core.DataStructureFactory>	newMiniSAT(org.sat4j.minisat.core.DataStructureFactory dsf)
static org.sat4j.specs.ISolver	newSAT()
static org.sat4j.specs.ISolver	newUNSAT()

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 org.sat4j.minisat.core.ILits> org.sat4j.minisat.core.Solver<org.sat4j.minisat.core.DataStructureFactory> newMiniSAT(org.sat4j.minisat.core.DataStructureFactory dsf)

Parameters:

dsf - the data structure used for representing clauses and lits

Returns:

MiniSAT the data structure dsf.

newDefault

public static org.sat4j.specs.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.

newSAT

public static org.sat4j.specs.ISolver newSAT()

newUNSAT

public static org.sat4j.specs.ISolver newUNSAT()

newCuttingPlanes

public static org.sat4j.specs.ISolver newCuttingPlanes()

defaultSolver

public org.sat4j.specs.ISolver defaultSolver()

Specified by:

defaultSolver in class org.sat4j.core.ASolverFactory<org.sat4j.specs.ISolver>

newLight

public static org.sat4j.specs.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 org.sat4j.specs.ISolver lightSolver()

Specified by:

lightSolver in class org.sat4j.core.ASolverFactory<org.sat4j.specs.ISolver>

newDimacsOutput

public static org.sat4j.specs.ISolver newDimacsOutput()