org.sat4j
Class LightFactory

java.lang.Object
  extended by org.sat4j.core.ASolverFactory<ISolver>
      extended by org.sat4j.LightFactory
All Implemented Interfaces:
Serializable

public class LightFactory
extends ASolverFactory<ISolver>

That class is the entry point to the default, best performing configuration of SAT4J. Since there is only one concrete reference per strategy used inside the solver, it is a good start for people willing to reduce the library to the minimal number of classes needed to run a SAT solver. The main method allow to run the solver from the command line.

Since:
2.2
Author:
leberre
See Also:
Serialized Form

Constructor Summary
LightFactory()
           
 
Method Summary
 ISolver defaultSolver()
          To obtain the default solver of the library.
static LightFactory 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 void main(String[] args)
           
 
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
 

Constructor Detail

LightFactory

public LightFactory()
Method Detail

instance

public static LightFactory instance()
Access to the single instance of the factory.

Returns:
the singleton of that class.

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

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

main

public static void main(String[] args)


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