Uses of Interface
org.sat4j.specs.ISolver

Packages that use ISolver

org.sat4j.core	Implementation of the data structures available in org.sat4j.specs.
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.opt	Optimization extensions.
org.sat4j.reader	Some utility classes to read problems from plain text files.
org.sat4j.tools	Tools to be used on top of an ISolver.

Uses of ISolver in org.sat4j.core

Methods in org.sat4j.core that return ISolver

ISolver	ASolverFactory.createSolverByName(java.lang.String solvername) create a solver from its String name. the solvername Xxxx must map one of the newXxxx methods.
abstract ISolver	ASolverFactory.defaultSolver() To obtain the default solver of the library.
abstract ISolver	ASolverFactory.lightSolver() To obtain a solver that is suitable for solving many small instances of SAT problems.

Uses of ISolver in org.sat4j.minisat

Methods in org.sat4j.minisat that return ISolver

ISolver	SolverFactory.defaultSolver()
ISolver	SolverFactory.lightSolver()
static ISolver	SolverFactory.newActiveLearning()
static ISolver	SolverFactory.newAdaptiveSolver() A SAT solver that adapts its data structures according to the problem to solve.
static ISolver	SolverFactory.newBackjumping()
static ISolver	SolverFactory.newDefault() Default solver of the SolverFactory.
static ISolver	SolverFactory.newLight() Small footprint SAT solver.
static ISolver	SolverFactory.newMini3SAT()
static ISolver	SolverFactory.newMini3SATb()
static ISolver	SolverFactory.newMiniCard()
static ISolver	SolverFactory.newMiniLearning()
static ISolver	SolverFactory.newMiniLearning(DataStructureFactory dsf)
static ISolver	SolverFactory.newMiniLearning(DataStructureFactory dsf, int n)
static ISolver	SolverFactory.newMiniLearning(DataStructureFactory dsf, IOrder order)
static ISolver	SolverFactory.newMiniLearning(int n)
static ISolver	SolverFactory.newMiniLearning2()
static ISolver	SolverFactory.newMiniLearning23()
static ISolver	SolverFactory.newMiniLearning2Heap()
static ISolver	SolverFactory.newMiniLearning2NewOrder()
static ISolver	SolverFactory.newMiniLearningCB()
static ISolver	SolverFactory.newMiniLearningCBWL()
static ISolver	SolverFactory.newMiniLearningCBWLPure()
static ISolver	SolverFactory.newMiniLearningEZSimp()
static ISolver	SolverFactory.newMiniLearningEZSimp(DataStructureFactory dsf)
static ISolver	SolverFactory.newMiniLearningHeap()
static ISolver	SolverFactory.newMiniLearningHeap(DataStructureFactory dsf)
static ISolver	SolverFactory.newMiniLearningHeapEZSimp()
static ISolver	SolverFactory.newMiniLearningHeapEZSimpLongRestarts()
static ISolver	SolverFactory.newMiniLearningHeapEZSimpNoRestarts()
static ISolver	SolverFactory.newMiniLearningPure()
static ISolver	SolverFactory.newMinimalOPBMax()
static ISolver	SolverFactory.newMinimalOPBMin()
static ISolver	SolverFactory.newMinimalOPBMinPueblo()
static ISolver	SolverFactory.newMiniOPBClauseAtLeastConstrMax()
static ISolver	SolverFactory.newMiniOPBClauseAtLeastMinPueblo()
static ISolver	SolverFactory.newMiniOPBClauseCardConstrMax()
static ISolver	SolverFactory.newMiniOPBClauseCardConstrMaxImplied()
static ISolver	SolverFactory.newMiniOPBClauseCardConstrMaxReduceToCard()
static ISolver	SolverFactory.newMiniOPBClauseCardConstrMaxReduceToClause()
static ISolver	SolverFactory.newMiniOPBClauseCardConstrMaxSpecificOrder()
static ISolver	SolverFactory.newMiniOPBClauseCardMin()
static ISolver	SolverFactory.newMiniOPBClauseCardMinPueblo()
static ISolver	SolverFactory.newMiniOPBCounterBasedClauseCardConstrMax()
static ISolver	SolverFactory.newMiniOPBMax()
static ISolver	SolverFactory.newMiniOPBMin()
static ISolver	SolverFactory.newMiniOPBMinPueblo()
static ISolver	SolverFactory.newMiniSAT()
static ISolver	SolverFactory.newMiniSAT(DataStructureFactory dsf)
static ISolver	SolverFactory.newMiniSAT2()
static ISolver	SolverFactory.newMiniSAT23()
static ISolver	SolverFactory.newMiniSAT23Heap()
static ISolver	SolverFactory.newMiniSAT2Heap()
static ISolver	SolverFactory.newMiniSATHeap()
static ISolver	SolverFactory.newMiniSATHeap(DataStructureFactory dsf)
static ISolver	SolverFactory.newMiniSATHeapEZSimp()
static ISolver	SolverFactory.newMiniSATNoRestarts()
static ISolver	SolverFactory.newRelsat()

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

Classes in org.sat4j.minisat.constraints.pb that implement ISolver

class	PBSolver
class	PBSolverCard
class	PBSolverClause
class	PBSolverWithImpliedClause

Uses of ISolver in org.sat4j.minisat.core

Classes in org.sat4j.minisat.core that implement ISolver

class

Solver

Uses of ISolver in org.sat4j.opt

Classes in org.sat4j.opt that implement ISolver

class	MaxSatDecorator
class	MinOneDecorator Computes a solution with the smallest number of satisfied literals.
class	PseudoOptDecorator
class	WeightedMaxSatDecorator

Constructors in org.sat4j.opt with parameters of type ISolver

MaxSatDecorator(ISolver solver)

MinOneDecorator(ISolver solver)

PseudoOptDecorator(ISolver solver)

WeightedMaxSatDecorator(ISolver solver)

Uses of ISolver in org.sat4j.reader

Constructors in org.sat4j.reader with parameters of type ISolver

CardDimacsReader(ISolver solver)
Deprecated.

CSPExtSupportReader(ISolver solver)

CSPReader(ISolver solver)

CSPSupportReader(ISolver solver)

DimacsReader(ISolver solver)

DimacsReader(ISolver solver, java.lang.String format)

ExtendedDimacsReader(ISolver solver)

GoodOPBReader(ISolver solver)

InstanceReader(ISolver solver)

LecteurDimacs(ISolver s)

OPBReader2005(ISolver solver)

OPBReader2006(ISolver solver)

Uses of ISolver in org.sat4j.tools

Classes in org.sat4j.tools that implement ISolver

class	Minimal4CardinalityModel Computes models with a minimal number (with respect to cardinality) of negative literals.
class	Minimal4InclusionModel Computes models with a minimal subset (with respect to set inclusion) of negative literals.
class	ModelIterator That class allows to iterate through all the models (implicants) of a formula.
class	SATRaceDecorator
class	SingleSolutionDetector This solver decorator allows to detect whether or not the set of constraints available in the solver has only one solution or not.
class	SolutionCounter Another solver decorator that counts the number of solutions.
class	SolverDecorator The aim of that class is to allow adding dynamic responsabilities to SAT solvers using the Decorator design pattern.

Methods in org.sat4j.tools that return ISolver

ISolver

SolverDecorator.decorated()

Methods in org.sat4j.tools with parameters of type ISolver

static IVecInt

RemiUtils.backbone(ISolver s) Compute the set of literals common to all models of the formula.

Constructors in org.sat4j.tools with parameters of type ISolver

Minimal4CardinalityModel(ISolver solver)

Minimal4InclusionModel(ISolver solver)

ModelIterator(ISolver solver)

SATRaceDecorator(ISolver solver)

SingleSolutionDetector(ISolver solver)

SolutionCounter(ISolver solver)

SolverDecorator(ISolver solver)