Uses of Class
org.sat4j.minisat.core.Solver

Packages that use Solver

org.sat4j.minisat	Implementation of the MiniSAT specification in Java.
org.sat4j.minisat.constraints.pb	Implementations of pseudo boolean contraints.
org.sat4j.minisat.core	Implementation of the MiniSAT solver skeleton.
org.sat4j.minisat.learning	Various learning strategies.

Uses of Solver in org.sat4j.minisat

Methods in org.sat4j.minisat that return Solver

static Solver<ILits>	SolverFactory.newActiveLearning()
static Solver<ILits>	SolverFactory.newBackjumping()
static Solver<ILits23>	SolverFactory.newMini3SAT()
static Solver<ILits23>	SolverFactory.newMini3SATb()
static Solver<ILits>	SolverFactory.newMiniCard()
static Solver<ILits>	SolverFactory.newMiniLearning()
static <L extends ILits> Solver<L>	SolverFactory.newMiniLearning(DataStructureFactory<L> dsf)
static <L extends ILits> Solver<L>	SolverFactory.newMiniLearning(DataStructureFactory<L> dsf, int n)
static <L extends ILits> Solver<L>	SolverFactory.newMiniLearning(DataStructureFactory<L> dsf, IOrder<L> order)
static Solver<ILits>	SolverFactory.newMiniLearning(int n)
static Solver<ILits2>	SolverFactory.newMiniLearning2()
static Solver<ILits23>	SolverFactory.newMiniLearning23()
static Solver<ILits2>	SolverFactory.newMiniLearning2Heap()
static Solver<ILits2>	SolverFactory.newMiniLearning2NewOrder()
static Solver<ILits>	SolverFactory.newMiniLearningCB()
static Solver<ILits>	SolverFactory.newMiniLearningCBWL()
static Solver<ILits>	SolverFactory.newMiniLearningCBWLPure()
static Solver<ILits>	SolverFactory.newMiniLearningEZSimp()
static <L extends ILits> Solver<L>	SolverFactory.newMiniLearningEZSimp(DataStructureFactory<L> dsf)
static Solver<ILits>	SolverFactory.newMiniLearningHeap()
static <L extends ILits> Solver<L>	SolverFactory.newMiniLearningHeap(DataStructureFactory<L> dsf)
static Solver<ILits>	SolverFactory.newMiniLearningHeapExpSimp()
static Solver<ILits>	SolverFactory.newMiniLearningHeapEZSimp()
static Solver<ILits>	SolverFactory.newMiniLearningHeapEZSimpLongRestarts()
static Solver<ILits>	SolverFactory.newMiniLearningHeapEZSimpNoRestarts()
static Solver<ILits>	SolverFactory.newMiniLearningHeapRsatExpSimp()
static Solver<ILits>	SolverFactory.newMiniLearningHeapRsatExpSimpBiere()
static Solver<ILits>	SolverFactory.newMiniLearningHeapRsatExpSimpLuby()
static Solver<ILits>	SolverFactory.newMiniLearningOPBClauseCardConstrMaxSpecificOrderIncremental()
static Solver<ILits>	SolverFactory.newMiniLearningOPBClauseCardConstrMaxSpecificOrderIncrementalLearnJustClauses()
static Solver<ILits>	SolverFactory.newMiniLearningOPBClauseCardConstrMaxSpecificOrderIncrementalMerging()
static Solver<ILits>	SolverFactory.newMiniLearningOPBClauseCardConstrMaxSpecificOrderIncrementalNoLearning()
static Solver<ILits>	SolverFactory.newMiniLearningOPBClauseCardConstrMaxSpecificOrderIncrementalReductionToClause()
static Solver<ILits>	SolverFactory.newMiniLearningPure()
static Solver<ILits>	SolverFactory.newMinimalOPBClauseCardConstrMaxSpecificOrder()
static Solver<ILits>	SolverFactory.newMinimalOPBMax()
static Solver<ILits>	SolverFactory.newMinimalOPBMin()
static Solver<ILits>	SolverFactory.newMinimalOPBMinPueblo()
static Solver<ILits>	SolverFactory.newMiniMaxSAT() Builds a SAT solver for the MAX sat evaluation.
static Solver<ILits>	SolverFactory.newMiniOPBClauseAtLeastConstrMax()
static Solver<ILits>	SolverFactory.newMiniOPBClauseAtLeastMinPueblo()
static Solver<ILits>	SolverFactory.newMiniOPBClauseCardConstrMax()
static Solver<ILits>	SolverFactory.newMiniOPBClauseCardConstrMaxImplied()
static Solver<ILits>	SolverFactory.newMiniOPBClauseCardConstrMaxReduceToClause()
static Solver<ILits>	SolverFactory.newMiniOPBClauseCardConstrMaxSpecificOrder()
static Solver<ILits>	SolverFactory.newMiniOPBClauseCardMin()
static Solver<ILits>	SolverFactory.newMiniOPBClauseCardMinPueblo()
static Solver<ILits>	SolverFactory.newMiniOPBCounterBasedClauseCardConstrMax()
static Solver<ILits>	SolverFactory.newMiniOPBMax()
static Solver<ILits>	SolverFactory.newMiniOPBMin()
static Solver<ILits>	SolverFactory.newMiniOPBMinPueblo()
static Solver<ILits>	SolverFactory.newMiniSAT()
static <L extends ILits> Solver<L>	SolverFactory.newMiniSAT(DataStructureFactory<L> dsf)
static Solver<ILits2>	SolverFactory.newMiniSAT2()
static Solver<ILits23>	SolverFactory.newMiniSAT23()
static Solver<ILits23>	SolverFactory.newMiniSAT23Heap()
static Solver<ILits2>	SolverFactory.newMiniSAT2Heap()
static Solver<ILits>	SolverFactory.newMiniSATHeap()
static <L extends ILits> Solver<L>	SolverFactory.newMiniSATHeap(DataStructureFactory<L> dsf)
static Solver<ILits>	SolverFactory.newMiniSATHeapExpSimp()
static Solver<ILits>	SolverFactory.newMiniSATHeapEZSimp()
static Solver<ILits>	SolverFactory.newMiniSATNoRestarts()
static Solver<ILits>	SolverFactory.newRelsat()

Uses of Solver in org.sat4j.minisat.constraints.pb

Subclasses of Solver in org.sat4j.minisat.constraints.pb

class	PBSolver<L extends ILits>
class	PBSolverClause
class	PBSolverMerging
class	PBSolverWithImpliedClause

Uses of Solver in org.sat4j.minisat.core

Methods in org.sat4j.minisat.core with parameters of type Solver

void	LearningStrategy.setSolver(Solver<L> s)

Uses of Solver in org.sat4j.minisat.learning

Methods in org.sat4j.minisat.learning with parameters of type Solver

void	ActiveLearning.setSolver(Solver<L> s)
void	MiniSATLearning.setSolver(Solver<L> s)
void	LimitedLearning.setSolver(Solver<L> s)