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<ILits,DataStructureFactory<ILits>>	newActiveLearning()
static Solver<ILits,DataStructureFactory<ILits>>	newBackjumping()
static ISolver	newDefault() Default solver of the SolverFactory.
static ISolver	newDimacsOutput()
static ISolver	newLight() Small footprint SAT solver.
static Solver<ILits23,DataStructureFactory<ILits23>>	newMini3SAT()
static Solver<ILits23,DataStructureFactory<ILits23>>	newMini3SATb()
static Solver<ILits,DataStructureFactory<ILits>>	newMiniCard()
static Solver<ILits,DataStructureFactory<ILits>>	newMiniLearning()
static <L extends ILits> Solver<L,DataStructureFactory<L>>	newMiniLearning(DataStructureFactory<L> dsf)
static <L extends ILits> Solver<L,DataStructureFactory<L>>	newMiniLearning(DataStructureFactory<L> dsf, int n)
static <L extends ILits> Solver<L,DataStructureFactory<L>>	newMiniLearning(DataStructureFactory<L> dsf, IOrder<L> order)
static Solver<ILits,DataStructureFactory<ILits>>	newMiniLearning(int n)
static Solver<ILits2,DataStructureFactory<ILits2>>	newMiniLearning2()
static Solver<ILits23,DataStructureFactory<ILits23>>	newMiniLearning23()
static Solver<ILits2,DataStructureFactory<ILits2>>	newMiniLearning2Heap()
static Solver<ILits2,DataStructureFactory<ILits2>>	newMiniLearning2NewOrder()
static Solver<ILits,DataStructureFactory<ILits>>	newMiniLearningCB()
static Solver<ILits,DataStructureFactory<ILits>>	newMiniLearningCBWL()
static Solver<ILits,DataStructureFactory<ILits>>	newMiniLearningCBWLPure()
static Solver<ILits,DataStructureFactory<ILits>>	newMiniLearningEZSimp()
static <L extends ILits> Solver<L,DataStructureFactory<L>>	newMiniLearningEZSimp(DataStructureFactory<L> dsf)
static Solver<ILits,DataStructureFactory<ILits>>	newMiniLearningHeap()
static <L extends ILits> Solver<L,DataStructureFactory<L>>	newMiniLearningHeap(DataStructureFactory<L> dsf)
static Solver<ILits,DataStructureFactory<ILits>>	newMiniLearningHeapExpSimp()
static Solver<ILits,DataStructureFactory<ILits>>	newMiniLearningHeapEZSimp()
static Solver<ILits,DataStructureFactory<ILits>>	newMiniLearningHeapEZSimpLongRestarts()
static Solver<ILits,DataStructureFactory<ILits>>	newMiniLearningHeapEZSimpNoRestarts()
static Solver<ILits,DataStructureFactory<ILits>>	newMiniLearningHeapRsatExpSimp()
static Solver<ILits,DataStructureFactory<ILits>>	newMiniLearningHeapRsatExpSimpBiere()
static Solver<ILits,DataStructureFactory<ILits>>	newMiniLearningHeapRsatExpSimpLuby()
static Solver<ILits,DataStructureFactory<ILits>>	newMiniLearningPure()
static Solver<ILits,DataStructureFactory<ILits>>	newMiniSAT()
static <L extends ILits> Solver<L,DataStructureFactory<L>>	newMiniSAT(DataStructureFactory<L> dsf)
static Solver<ILits2,DataStructureFactory<ILits2>>	newMiniSAT2()
static Solver<ILits23,DataStructureFactory<ILits23>>	newMiniSAT23()
static Solver<ILits23,DataStructureFactory<ILits23>>	newMiniSAT23Heap()
static Solver<ILits2,DataStructureFactory<ILits2>>	newMiniSAT2Heap()
static Solver<ILits,DataStructureFactory<ILits>>	newMiniSATHeap()
static <L extends ILits> Solver<L,DataStructureFactory<L>>	newMiniSATHeap(DataStructureFactory<L> dsf)
static Solver<ILits,DataStructureFactory<ILits>>	newMiniSATHeapExpSimp()
static Solver<ILits,DataStructureFactory<ILits>>	newMiniSATHeapEZSimp()
static Solver<ILits,DataStructureFactory<ILits>>	newMiniSatHeapRsatExpSimpBiere()
static Solver<ILits,DataStructureFactory<ILits>>	newMiniSATNoRestarts()
static ISolver	newMinOneSolver()
static Solver<ILits,DataStructureFactory<ILits>>	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.

newMiniLearning

public static Solver<ILits,DataStructureFactory<ILits>> newMiniLearning()

Returns:

a "default" "minilearning" solver learning clauses of size smaller than 10 % of the total number of variables

newMiniLearningHeap

public static Solver<ILits,DataStructureFactory<ILits>> 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<ILits,DataStructureFactory<ILits>> newMiniLearningHeapEZSimp()

newMiniLearningHeapExpSimp

public static Solver<ILits,DataStructureFactory<ILits>> newMiniLearningHeapExpSimp()

newMiniLearningHeapRsatExpSimp

public static Solver<ILits,DataStructureFactory<ILits>> newMiniLearningHeapRsatExpSimp()

newMiniLearningHeapRsatExpSimpBiere

public static Solver<ILits,DataStructureFactory<ILits>> newMiniLearningHeapRsatExpSimpBiere()

newMiniSatHeapRsatExpSimpBiere

public static Solver<ILits,DataStructureFactory<ILits>> newMiniSatHeapRsatExpSimpBiere()

newMiniLearningHeapRsatExpSimpLuby

public static Solver<ILits,DataStructureFactory<ILits>> newMiniLearningHeapRsatExpSimpLuby()

newMiniLearning

public static Solver<ILits,DataStructureFactory<ILits>> newMiniLearning(int n)

Parameters:

n - the maximal size of the clauses to learn as a percentage of the initial number of variables

Returns:

a "minilearning" solver learning clauses of size smaller than n of the total number of variables

newMiniLearning

public static <L extends ILits> Solver<L,DataStructureFactory<L>> newMiniLearning(DataStructureFactory<L> 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.

newMiniLearningHeap

public static <L extends ILits> Solver<L,DataStructureFactory<L>> newMiniLearningHeap(DataStructureFactory<L> 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

newMiniLearning2

public static Solver<ILits2,DataStructureFactory<ILits2>> newMiniLearning2()

Returns:

a default minilearning solver using a specific data structure described in Lawrence Ryan thesis to handle binary clauses.

See Also:

newMiniLearning()

newMiniLearning2Heap

public static Solver<ILits2,DataStructureFactory<ILits2>> newMiniLearning2Heap()

newMiniLearning23

public static Solver<ILits23,DataStructureFactory<ILits23>> newMiniLearning23()

Returns:

a default minilearning solver using a specific data structures described in Lawrence Ryan thesis to handle binary and ternary clauses.

See Also:

newMiniLearning()

newMiniLearningCB

public static Solver<ILits,DataStructureFactory<ILits>> newMiniLearningCB()

Returns:

a default minilearning SAT solver using counter-based clause representation (i.e. all the literals of a clause are watched)

newMiniLearningCBWL

public static Solver<ILits,DataStructureFactory<ILits>> newMiniLearningCBWL()

Returns:

a default minilearning SAT solver using counter-based clause representation (i.e. all the literals of a clause are watched) for the ORIGINAL clauses and watched-literals clause representation for learnt clauses.

newMiniLearning2NewOrder

public static Solver<ILits2,DataStructureFactory<ILits2>> newMiniLearning2NewOrder()

newMiniLearningPure

public static Solver<ILits,DataStructureFactory<ILits>> 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<ILits,DataStructureFactory<ILits>> 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 <L extends ILits> Solver<L,DataStructureFactory<L>> newMiniLearning(DataStructureFactory<L> dsf,
                                                                                  int n)

Parameters:

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

n - the maximum size of learnt clauses as percentage of the original number of variables.

Returns:

a SAT solver with learning limited to clauses of length smaller or equal to n, the dsf data structure, the FirstUIP clause generator and a sort of VSIDS heuristics.

newMiniLearning

public static <L extends ILits> Solver<L,DataStructureFactory<L>> newMiniLearning(DataStructureFactory<L> dsf,
                                                                                  IOrder<L> 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.

newMiniLearningEZSimp

public static Solver<ILits,DataStructureFactory<ILits>> newMiniLearningEZSimp()

newMiniLearningEZSimp

public static <L extends ILits> Solver<L,DataStructureFactory<L>> newMiniLearningEZSimp(DataStructureFactory<L> dsf)

newMiniLearningHeapEZSimpNoRestarts

public static Solver<ILits,DataStructureFactory<ILits>> newMiniLearningHeapEZSimpNoRestarts()

Returns:

a default MiniLearning without restarts.

newMiniLearningHeapEZSimpLongRestarts

public static Solver<ILits,DataStructureFactory<ILits>> newMiniLearningHeapEZSimpLongRestarts()

Returns:

a default MiniLearning with restarts beginning at 1000 conflicts.

newActiveLearning

public static Solver<ILits,DataStructureFactory<ILits>> newActiveLearning()

Returns:

a SAT solver using First UIP clause generator, watched literals, VSIDS like heuristics learning only clauses having a great number of active variables, i.e. variables with an activity strictly greater than one.

newMiniSAT

public static Solver<ILits,DataStructureFactory<ILits>> newMiniSAT()

Returns:

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

newMiniSATNoRestarts

public static Solver<ILits,DataStructureFactory<ILits>> newMiniSATNoRestarts()

Returns:

MiniSAT without restarts.

newMiniSAT2

public static Solver<ILits2,DataStructureFactory<ILits2>> newMiniSAT2()

Returns:

MiniSAT with a special data structure from Lawrence Ryan thesis for managing binary clauses.

newMiniSAT23

public static Solver<ILits23,DataStructureFactory<ILits23>> newMiniSAT23()

Returns:

MiniSAT with a special data structure from Lawrence Ryan thesis for managing binary and ternary clauses.

newMiniSAT

public static <L extends ILits> Solver<L,DataStructureFactory<L>> newMiniSAT(DataStructureFactory<L> dsf)

Parameters:

dsf - the data structure used for representing clauses and lits

Returns:

MiniSAT the data structure dsf.

newMiniSATHeap

public static Solver<ILits,DataStructureFactory<ILits>> newMiniSATHeap()

Returns:

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

newMiniSATHeapEZSimp

public static Solver<ILits,DataStructureFactory<ILits>> newMiniSATHeapEZSimp()

Returns:

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

newMiniSATHeapExpSimp

public static Solver<ILits,DataStructureFactory<ILits>> newMiniSATHeapExpSimp()

newMiniSAT2Heap

public static Solver<ILits2,DataStructureFactory<ILits2>> newMiniSAT2Heap()

Returns:

MiniSAT with a special data structure from Lawrence Ryan thesis for managing binary clauses.

newMiniSAT23Heap

public static Solver<ILits23,DataStructureFactory<ILits23>> newMiniSAT23Heap()

Returns:

MiniSAT with a special data structure from Lawrence Ryan thesis for managing binary and ternary clauses.

newMiniSATHeap

public static <L extends ILits> Solver<L,DataStructureFactory<L>> newMiniSATHeap(DataStructureFactory<L> dsf)

newMiniCard

public static Solver<ILits,DataStructureFactory<ILits>> newMiniCard()

Returns:

MiniSAT with data structures to handle cardinality constraints.

newRelsat

public static Solver<ILits,DataStructureFactory<ILits>> newRelsat()

Returns:

MiniSAT with decision UIP clause generator.

newBackjumping

public static Solver<ILits,DataStructureFactory<ILits>> newBackjumping()

Returns:

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

newMini3SAT

public static Solver<ILits23,DataStructureFactory<ILits23>> newMini3SAT()

Returns:

a SAT solver with learning limited to clauses of length smaller or equals to 3, with a specific data structure for binary and ternary clauses as found in Lawrence Ryan thesis, without restarts, with a Jeroslow/Wang kind of heuristics.

newMini3SATb

public static Solver<ILits23,DataStructureFactory<ILits23>> newMini3SATb()

Returns:

a Mini3SAT with full learning.

See Also:

newMini3SAT()

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