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.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.newBackjumping()
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.newMiniLearningNoRestarts()
static ISolver	SolverFactory.newMiniLearningPure()
static ISolver	SolverFactory.newMinimalOPBMax()
static ISolver	SolverFactory.newMinimalOPBMin()
static ISolver	SolverFactory.newMiniOPBMax()
static ISolver	SolverFactory.newMiniOPBMin()
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.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

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.reader

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

CardDimacsReader(ISolver solver)
Deprecated.

CSPReader(ISolver solver)

DimacsReader(ISolver solver)

ExtendedDimacsReader(ISolver solver)

GoodOPBReader(ISolver solver)

InstanceReader(ISolver solver)

LecteurDimacs(ISolver s)

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

SolutionCounter(ISolver solver)

SolverDecorator(ISolver solver)