org.sat4j.maxsat

Class SolverFactory

java.lang.Object

org.sat4j.core.ASolverFactory<IPBSolver>

org.sat4j.maxsat.SolverFactory

All Implemented Interfaces:

Serializable

public class SolverFactory
extends ASolverFactory<IPBSolver>

See Also:

Serialized Form

Method Summary

Methods

Modifier and Type	Method and Description
IPBSolver	defaultSolver() To obtain the default solver of the library.
static SolverFactory	instance() Access to the single instance of the factory.
IPBSolver	lightSolver() To obtain a solver that is suitable for solving many small instances of SAT problems.
static IPBSolver	newDefault()
static IPBSolver	newLight()
static Solver<DataStructureFactory>	newMiniMaxSAT() Builds a SAT solver for the MAX sat evaluation.

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

Method Detail

newMiniMaxSAT

public static Solver<DataStructureFactory> newMiniMaxSAT()

Builds a SAT solver for the MAX sat evaluation. Full clause learning, no restarts,

Returns:

a

instance

public static SolverFactory instance()

Access to the single instance of the factory.

Returns:

the singleton of that class.

defaultSolver

public IPBSolver 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<IPBSolver>

Returns:

a solver from the factory

See Also:

ASolverFactory.lightSolver()

lightSolver

public IPBSolver 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<IPBSolver>

Returns:

a solver from the factory

See Also:

ASolverFactory.defaultSolver()

newDefault

public static IPBSolver newDefault()

newLight

public static IPBSolver newLight()