org.sat4j
Class LightFactory

java.lang.Object
  org.sat4j.core.ASolverFactory<ISolver>
      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)