org.sat4j.core
Class ASolverFactory

java.lang.Object
  org.sat4j.core.ASolverFactory

Direct Known Subclasses:

SolverFactory

public abstract class ASolverFactory
extends java.lang.Object

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

Author:

bourgeois

Constructor Summary

ASolverFactory()

Method Summary

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

Methods inherited from class java.lang.Object

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

Constructor Detail

ASolverFactory

public ASolverFactory()

Method Detail

solverNames

public java.lang.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 ISolver createSolverByName(java.lang.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 ISolver 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 ISolver 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()