org.sat4j.minisat
Class SolverFactory

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

All Implemented Interfaces:

java.io.Serializable

public 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 Solver<MixedDataStructureDanielWL>	newBackjumping()
static Solver<DataStructureFactory>	newBestHT()
static Solver<DataStructureFactory>	newBestWL()
static ISolver	newDefault() Default solver of the SolverFactory.
static ISolver	newDimacsOutput()
static Solver<DataStructureFactory>	newGlucose()
static ISolver	newLight() Small footprint SAT solver.
static Solver<DataStructureFactory>	newMiniLearning(DataStructureFactory dsf, IOrder order)
static Solver<DataStructureFactory>	newMiniLearningCBWLPure()
static Solver<DataStructureFactory>	newMiniLearningHeap()
static Solver<DataStructureFactory>	newMiniLearningHeap(DataStructureFactory dsf)
static Solver<DataStructureFactory>	newMiniLearningHeapExpSimp()
static Solver<DataStructureFactory>	newMiniLearningHeapEZSimp()
static Solver<DataStructureFactory>	newMiniLearningHeapEZSimpLongRestarts()
static Solver<DataStructureFactory>	newMiniLearningHeapEZSimpNoRestarts()
static Solver<DataStructureFactory>	newMiniLearningHeapRsatExpSimp()
static Solver<DataStructureFactory>	newMiniLearningHeapRsatExpSimpBiere()
static Solver<DataStructureFactory>	newMiniLearningHeapRsatExpSimpLuby()
static Solver<DataStructureFactory>	newMiniLearningPure()
static Solver<DataStructureFactory>	newMiniSATHeap()
static Solver<DataStructureFactory>	newMiniSATHeap(DataStructureFactory dsf)
static Solver<DataStructureFactory>	newMiniSATHeapExpSimp()
static Solver<DataStructureFactory>	newMiniSATHeapEZSimp()
static ISolver	newMinOneSolver()
static Solver<MixedDataStructureDanielWL>	newRelsat()

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 Solver<DataStructureFactory> newMiniLearningHeapEZSimp()

newMiniLearningHeapExpSimp

public static Solver<DataStructureFactory> newMiniLearningHeapExpSimp()

newMiniLearningHeapRsatExpSimp

public static Solver<DataStructureFactory> newMiniLearningHeapRsatExpSimp()

newMiniLearningHeapRsatExpSimpBiere

public static Solver<DataStructureFactory> newMiniLearningHeapRsatExpSimpBiere()

newMiniLearningHeapRsatExpSimpLuby

public static Solver<DataStructureFactory> newMiniLearningHeapRsatExpSimpLuby()

newBestWL

public static Solver<DataStructureFactory> newBestWL()

Since:

2.1

newBestHT

public static Solver<DataStructureFactory> newBestHT()

Since:

2.1

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 Solver<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.)

newMiniLearningCBWLPure

public static Solver<DataStructureFactory> newMiniLearningCBWLPure()

Returns:

a default minilearning SAT solver choosing periodically to branch on literal "pure in the original set of clauses" if any.

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 Solver<DataStructureFactory> newMiniLearningHeapEZSimpNoRestarts()

Returns:

a default MiniLearning without restarts.

newMiniLearningHeapEZSimpLongRestarts

public static Solver<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 Solver<DataStructureFactory> newMiniSATHeapEZSimp()

Returns:

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

newMiniSATHeapExpSimp

public static Solver<DataStructureFactory> newMiniSATHeapExpSimp()

newMiniSATHeap

public static Solver<DataStructureFactory> newMiniSATHeap(DataStructureFactory dsf)

newRelsat

public static Solver<MixedDataStructureDanielWL> newRelsat()

Returns:

MiniSAT with decision UIP clause generator.

newBackjumping

public static Solver<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()