org.sat4j.csp
Class SolverFactory

java.lang.Object
  org.sat4j.core.ASolverFactory<ISolver>
      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()