Uses of Interface

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

Classes in 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 that return ISolver
 ISolver SolverDecorator.decorated()

Methods in 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 with parameters of type ISolver
Minimal4CardinalityModel(ISolver solver)
Minimal4InclusionModel(ISolver solver)
ModelIterator(ISolver solver)
SolutionCounter(ISolver solver)
SolverDecorator(ISolver solver)