Uses of Interface
org.sat4j.specs.IProblem

Packages that use IProblem

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.specs	Those classes are intented for users dealing with SAT solvers as blackboxes.
org.sat4j.tools	Tools to be used on top of an ISolver.

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

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

class

PBSolver

Uses of IProblem in org.sat4j.minisat.core

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

class

Solver

Uses of IProblem in org.sat4j.reader

Methods in org.sat4j.reader that return IProblem

IProblem	OPBReader2005.parseInstance(java.lang.String filename)
IProblem	LecteurDimacs.parseInstance(java.lang.String nomFichier) lit la base de clauses et la met dans le vecteur donn?
IProblem	InstanceReader.parseInstance(java.lang.String filename)
IProblem	GoodOPBReader.parseInstance(java.lang.String filename)
IProblem	DimacsReader.parseInstance(java.lang.String filename) Remplit un prouveur ?
IProblem	CSPReader.parseInstance(java.lang.String filename)
IProblem	Reader.parseInstance(java.lang.String filename)

Uses of IProblem in org.sat4j.specs

Subinterfaces of IProblem in org.sat4j.specs

interface

ISolver That interface contains all the services available on a SAT solver.

Uses of IProblem in org.sat4j.tools

Classes in org.sat4j.tools that implement IProblem

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.