org.sat4j.core
Class ASolverFactory<T extends ISolver>

java.lang.Object
  extended by 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
ASolverFactory()
           
 
Method Summary
 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()


Copyright © 2012 Centre de Recherche en Informatique de Lens (CRIL). All Rights Reserved.