Uses of Interface
org.sat4j.specs.IProblem

Packages that use IProblem

org.sat4j	Contain a command line launcher for the SAT solvers.
org.sat4j.minisat.constraints.pb	Implementations of pseudo boolean contraints.
org.sat4j.minisat.core	Implementation of the MiniSAT solver skeleton.
org.sat4j.opt	Built-in optimization framework.
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

Methods in org.sat4j that return IProblem

protected IProblem

AbstractLauncher.readProblem(java.lang.String problemname) Reads a problem file from the command line.

Methods in org.sat4j with parameters of type IProblem

protected void	LanceurPseudo2005.solve(IProblem problem)
protected void	AbstractOptimizationLauncher.solve(IProblem problem)
protected void	AbstractLauncher.solve(IProblem problem)

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

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

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

Uses of IProblem in org.sat4j.minisat.core

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

class

Solver<L extends ILits> The backbone of the library providing the modular implementation of a MiniSAT (Chaff) like solver.

Uses of IProblem in org.sat4j.opt

Classes in org.sat4j.opt that implement IProblem

class	AbstractSelectorVariablesDecorator
class	MaxSatDecorator
class	MinCostDecorator A decorator that computes minimal cost models.
class	MinOneDecorator Computes a solution with the smallest number of satisfied literals.
class	PseudoOptDecorator A decorator that computes minimal pseudo boolean models.
class	WeightedMaxSatDecorator

Uses of IProblem in org.sat4j.reader

Methods in org.sat4j.reader that return IProblem

IProblem	LecteurDimacs.parseInstance(java.io.InputStream in)
IProblem	AIGReader.parseInstance(java.io.InputStream in)
IProblem	Reader.parseInstance(java.io.InputStream in)
IProblem	CSPReader.parseInstance(java.io.Reader in)
IProblem	LecteurDimacs.parseInstance(java.io.Reader in)
IProblem	AAGReader.parseInstance(java.io.Reader in)
IProblem	InstanceReader.parseInstance(java.io.Reader in)
IProblem	XMLCSPReader.parseInstance(java.io.Reader in)
IProblem	AIGReader.parseInstance(java.io.Reader in)
IProblem	DimacsReader.parseInstance(java.io.Reader in)
IProblem	OPBReader2005.parseInstance(java.io.Reader in)
IProblem	GoodOPBReader.parseInstance(java.io.Reader in)
abstract IProblem	Reader.parseInstance(java.io.Reader in)
IProblem	InstanceReader.parseInstance(java.lang.String filename)
IProblem	XMLCSPReader.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	IOptimizationProblem
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	DimacsOutputSolver Solver used to display in a writer the CNF instance in Dimacs format.
class	GateTranslator Utility class to easily feed a SAT solver using logical gates.
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	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 IProblem

IProblem

DimacsArrayReader.parseInstance(int[] gateType, int[] outputs, int[][] inputs, int maxVar)