org.sat4j.csp

Class SolverFactory

java.lang.Object

org.sat4j.core.ASolverFactory<ISolver>

org.sat4j.csp.SolverFactory

All Implemented Interfaces:

Serializable

public class SolverFactory
extends ASolverFactory<ISolver>

User friendly access to pre-constructed solvers.

Author:

leberre

See Also:

Serialized Form

Method Summary

Methods

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> Solver<DataStructureFactory>	newMiniSAT(DataStructureFactory dsf)
static ISolver	newSAT()
static 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 ILits> Solver<DataStructureFactory> newMiniSAT(DataStructureFactory 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.

newSAT

public static ISolver newSAT()

newUNSAT

public static ISolver newUNSAT()

newCuttingPlanes

public static ISolver newCuttingPlanes()

defaultSolver

public ISolver defaultSolver()

Description copied from class: ASolverFactory

To obtain the default solver of the library. The solver is suitable to solve huge SAT benchmarks. It should reflect state-of-the-art SAT technologies. For solving small/easy SAT benchmarks, use lightSolver() instead.

Specified by:

defaultSolver in class ASolverFactory<ISolver>

Returns:

a solver from the factory

See Also:

ASolverFactory.lightSolver()

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

Description copied from class: ASolverFactory

To obtain a solver that is suitable for solving many small instances of SAT problems. The solver is not using sophisticated but costly reasoning and avoids to allocate too much memory. For solving bigger SAT benchmarks, use defaultSolver() instead.

Specified by:

lightSolver in class ASolverFactory<ISolver>

Returns:

a solver from the factory

See Also:

ASolverFactory.defaultSolver()

newDimacsOutput

public static ISolver newDimacsOutput()