org.sat4j.core
Class ASolverFactory

java.lang.Object
  extended by 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
clone, equals, finalize, 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()


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