org.sat4j.core

Class ASolverFactory<T extends ISolver>

java.lang.Object

org.sat4j.core.ASolverFactory<T>

All Implemented Interfaces:

Serializable

Direct Known Subclasses:

LightFactory, SolverFactory

public abstract class ASolverFactory<T extends ISolver>
extends Object
implements Serializable

A solver factory is responsible for providing prebuilt solvers to the end user.

Author:

bourgeois

See Also:

Serialized Form

Constructor Summary

Constructors

Constructor and Description
ASolverFactory()

Method Summary

Methods

Modifier and Type	Method and Description
T	createSolverByName(String solvername) create a solver from its String name. the solvername Xxxx must map one of the newXxxx methods.
abstract T	defaultSolver() To obtain the default solver of the library.
abstract T	lightSolver() To obtain a solver that is suitable for solving many small instances of SAT problems.
String[]	solverNames() This methods returns names of solvers to be used with the method getSolverByName().

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

ASolverFactory

public ASolverFactory()

Method Detail

solverNames

public String[] solverNames()

This methods returns names of solvers to be used with the method getSolverByName().

Returns:

an array containing the names of all the solvers available in the library.

See Also:

createSolverByName(String)

createSolverByName

public T createSolverByName(String solvername)

create a solver from its String name. the solvername Xxxx must map one of the newXxxx methods.

Parameters:

solvername - the name of the solver

Returns:

an ISolver built using newSolvername. null if the solvername doesn't map one of the method of the factory.

defaultSolver

public abstract T defaultSolver()

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.

Returns:

a solver from the factory

See Also:

lightSolver()

lightSolver

public abstract T lightSolver()

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.

Returns:

a solver from the factory

See Also:

defaultSolver()