org.sat4j.csp
Class SolverFactory

java.lang.Object
  org.sat4j.core.ASolverFactory<org.sat4j.specs.ISolver>
      org.sat4j.csp.SolverFactory

All Implemented Interfaces:

java.io.Serializable

public class SolverFactory
extends org.sat4j.core.ASolverFactory<org.sat4j.specs.ISolver>
implements java.io.Serializable

User friendly access to pre-constructed solvers.

Author:

leberre

See Also:

Serialized Form

Method Summary

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

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