org.sat4j.minisat
Class SolverFactory

java.lang.Object
  org.sat4j.core.ASolverFactory<ISolver>
      org.sat4j.minisat.SolverFactory

All Implemented Interfaces:

Serializable

public final class SolverFactory
extends ASolverFactory<ISolver>

User friendly access to pre-constructed solvers.

Author:

leberre

See Also:

Serialized Form

Method Summary

ISolver	defaultSolver() To obtain the default solver of the library.
static SolverFactory	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 ICDCL<MixedDataStructureDanielWL>	newBackjumping()
static ICDCL<DataStructureFactory>	newBest17()
static ICDCL<DataStructureFactory>	newBestHT()
static ICDCL<DataStructureFactory>	newBestSingleWL()
static Solver<DataStructureFactory>	newBestWL()
static ISolver	newDefault() Default solver of the SolverFactory.
static ICDCL<DataStructureFactory>	newDefaultAutoErasePhaseSaving()
static ICDCL<DataStructureFactory>	newDefaultMS21PhaseSaving()
static ISolver	newDimacsOutput()
static Solver<DataStructureFactory>	newGlucose()
static ICDCL<DataStructureFactory>	newGreedySolver()
static ISolver	newLight() Small footprint SAT solver.
static Solver<DataStructureFactory>	newMiniLearning(DataStructureFactory dsf, IOrder order)
static Solver<DataStructureFactory>	newMiniLearningHeap()
static Solver<DataStructureFactory>	newMiniLearningHeap(DataStructureFactory dsf)
static Solver<DataStructureFactory>	newMiniLearningHeapExpSimp()
static ICDCL<DataStructureFactory>	newMiniLearningHeapEZSimp()
static ICDCL<DataStructureFactory>	newMiniLearningHeapEZSimpLongRestarts()
static ICDCL<DataStructureFactory>	newMiniLearningHeapEZSimpNoRestarts()
static Solver<DataStructureFactory>	newMiniLearningHeapRsatExpSimp()
static Solver<DataStructureFactory>	newMiniLearningHeapRsatExpSimpBiere()
static ICDCL<DataStructureFactory>	newMiniLearningHeapRsatExpSimpLuby()
static ICDCL<DataStructureFactory>	newMiniLearningPure()
static Solver<DataStructureFactory>	newMiniSATHeap()
static Solver<DataStructureFactory>	newMiniSATHeap(DataStructureFactory dsf)
static ICDCL<DataStructureFactory>	newMiniSATHeapExpSimp()
static ICDCL<DataStructureFactory>	newMiniSATHeapEZSimp()
static ISolver	newMinOneSolver()

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

instance

public static SolverFactory instance()

Access to the single instance of the factory.

Returns:

the singleton of that class.

newMiniLearningHeap

public static Solver<DataStructureFactory> newMiniLearningHeap()

Returns:

a "default" "minilearning" solver learning clauses of size smaller than 10 % of the total number of variables with a heap based var order.

newMiniLearningHeapEZSimp

public static ICDCL<DataStructureFactory> newMiniLearningHeapEZSimp()

newMiniLearningHeapExpSimp

public static Solver<DataStructureFactory> newMiniLearningHeapExpSimp()

newMiniLearningHeapRsatExpSimp

public static Solver<DataStructureFactory> newMiniLearningHeapRsatExpSimp()

newMiniLearningHeapRsatExpSimpBiere

public static Solver<DataStructureFactory> newMiniLearningHeapRsatExpSimpBiere()

newMiniLearningHeapRsatExpSimpLuby

public static ICDCL<DataStructureFactory> newMiniLearningHeapRsatExpSimpLuby()

newGreedySolver

public static ICDCL<DataStructureFactory> newGreedySolver()

Since:

2.2

newDefaultAutoErasePhaseSaving

public static ICDCL<DataStructureFactory> newDefaultAutoErasePhaseSaving()

Since:

2.2

newDefaultMS21PhaseSaving

public static ICDCL<DataStructureFactory> newDefaultMS21PhaseSaving()

Since:

2.2.3

newBestWL

public static Solver<DataStructureFactory> newBestWL()

Since:

2.1

newBestHT

public static ICDCL<DataStructureFactory> newBestHT()

Since:

2.1

newBestSingleWL

public static ICDCL<DataStructureFactory> newBestSingleWL()

Since:

2.2

newBest17

public static ICDCL<DataStructureFactory> newBest17()

Since:

2.2

newGlucose

public static Solver<DataStructureFactory> newGlucose()

Since:

2.1

newMiniLearningHeap

public static Solver<DataStructureFactory> newMiniLearningHeap(DataStructureFactory dsf)

Parameters:

dsf - a specific data structure factory

Returns:

a default "minilearning" solver using a specific data structure factory, learning clauses of length smaller or equals to 10 % of the number of variables and a heap based VSIDS heuristics

newMiniLearningPure

public static ICDCL<DataStructureFactory> newMiniLearningPure()

Returns:

a default minilearning SAT solver choosing periodically to branch on "pure watched" literals if any. (a pure watched literal l is a literal that is watched on at least one clause such that its negation is not watched at all. It is not necessarily a watched literal.)

newMiniLearning

public static Solver<DataStructureFactory> newMiniLearning(DataStructureFactory dsf,
                                                           IOrder order)

Parameters:

dsf - the data structure factory used to represent literals and clauses

order - the heuristics

Returns:

a SAT solver with learning limited to clauses of length smaller or equal to 10 percent of the total number of variables, the dsf data structure, the FirstUIP clause generator and order as heuristics.

newMiniLearningHeapEZSimpNoRestarts

public static ICDCL<DataStructureFactory> newMiniLearningHeapEZSimpNoRestarts()

Returns:

a default MiniLearning without restarts.

newMiniLearningHeapEZSimpLongRestarts

public static ICDCL<DataStructureFactory> newMiniLearningHeapEZSimpLongRestarts()

Returns:

a default MiniLearning with restarts beginning at 1000 conflicts.

newMiniSATHeap

public static Solver<DataStructureFactory> newMiniSATHeap()

Returns:

a SAT solver very close to the original MiniSAT sat solver.

newMiniSATHeapEZSimp

public static ICDCL<DataStructureFactory> newMiniSATHeapEZSimp()

Returns:

a SAT solver very close to the original MiniSAT sat solver including easy reason simplification.

newMiniSATHeapExpSimp

public static ICDCL<DataStructureFactory> newMiniSATHeapExpSimp()

newMiniSATHeap

public static Solver<DataStructureFactory> newMiniSATHeap(DataStructureFactory dsf)

newBackjumping

public static ICDCL<MixedDataStructureDanielWL> newBackjumping()

Returns:

MiniSAT with VSIDS heuristics, FirstUIP clause generator for backjumping but no learning.

newMinOneSolver

public static ISolver newMinOneSolver()

Returns:

a solver computing models with a minimum number of satisfied literals.

newDefault

public static ISolver newDefault()

Default solver of the SolverFactory. This solver is meant to be used on challenging SAT benchmarks.

Returns:

the best "general purpose" SAT solver available in the factory.

See Also:

the same method, polymorphic, to be called from an instance of ASolverFactory.

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

newLight

public static ISolver newLight()

Small footprint SAT solver.

Returns:

a SAT solver suitable for solving small/easy SAT benchmarks.

See Also:

the same method, polymorphic, to be called from an instance of ASolverFactory.

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

newDimacsOutput

public static ISolver newDimacsOutput()