Uses of Interface
org.sat4j.specs.IProblem

Packages that use IProblem

Package	Description
org.sat4j	Contains a command line launcher for the SAT solvers.
org.sat4j.maxsat	MAXSAT and Weighted Max SAT framework.
org.sat4j.minisat.core	Implementation of the MiniSAT solver skeleton.
org.sat4j.opt	Built-in optimization framework.
org.sat4j.pb	Implementations of pseudo boolean solvers
org.sat4j.pb.core	Implementations of pseudo boolean solvers
org.sat4j.pb.reader	Readers for opb instances.
org.sat4j.pb.tools	Implementation of different tools for pseudo boolean solvers
org.sat4j.reader	Some utility classes to read problems from plain text files.
org.sat4j.sat	Implementation of a sat4j Launcher.
org.sat4j.specs	Those classes are intended for users dealing with SAT solvers as black boxes.
org.sat4j.tools	Tools to be used on top of an ISolver.
org.sat4j.tools.xplain	Implementation of an explanation engine in case of unsatisfiability.

Uses of IProblem in org.sat4j

Fields in org.sat4j declared as IProblem

Modifier and Type	Field and Description
protected IProblem	AbstractLauncher.problem

Methods in org.sat4j that return IProblem

Modifier and Type	Method and Description
protected IProblem	AbstractLauncher.readProblem(String problemname) Reads a problem file from the command line.

Methods in org.sat4j with parameters of type IProblem

Modifier and Type	Method and Description
void	ILauncherMode.displayResult(ISolver solver, IProblem problem, ILogAble logger, PrintWriter out, Reader reader, long beginTime, boolean displaySolutionLine) Output of the launcher when the solver stops
protected void	AbstractLauncher.solve(IProblem problem)
protected void	AbstractOptimizationLauncher.solve(IProblem problem) Deprecated.
void	ILauncherMode.solve(IProblem problem, Reader reader, ILogAble logger, PrintWriter out, long beginTime) Main solver call: one call for a decision problem, a loop for an optimization problem.

Uses of IProblem in org.sat4j.maxsat

Classes in org.sat4j.maxsat that implement IProblem

Modifier and Type	Class and Description
class	MinCostDecorator A decorator that computes minimal cost models.
class	WeightedMaxSatDecorator A decorator for solving weighted MAX SAT problems.

Methods in org.sat4j.maxsat that return IProblem

Modifier and Type	Method and Description
protected IProblem	GenericOptLauncher.readProblem(String problemname)

Uses of IProblem in org.sat4j.minisat.core

Subinterfaces of IProblem in org.sat4j.minisat.core

Modifier and Type	Interface and Description
interface	ICDCL<D extends DataStructureFactory> Abstraction for Conflict Driven Clause Learning Solver.

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

Modifier and Type	Class and Description
class	Solver<D extends DataStructureFactory> 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

Modifier and Type	Class and Description
class	AbstractSelectorVariablesDecorator Abstract class which adds a new "selector" variable for each clause entered in the solver.
class	MaxSatDecorator Computes a solution that satisfies the maximum of clauses.
class	MinOneDecorator Computes a solution with the smallest number of satisfied literals.

Uses of IProblem in org.sat4j.pb

Subinterfaces of IProblem in org.sat4j.pb

Modifier and Type	Interface and Description
interface	IPBSolver A solver able to deal with pseudo boolean constraints.

Classes in org.sat4j.pb that implement IProblem

Modifier and Type	Class and Description
class	ConstraintRelaxingPseudoOptDecorator
class	LPStringSolver Solver used to display in a string the pb-instance in OPB format.
class	OPBStringSolver Solver used to display in a string the pb-instance in OPB format.
class	OptToPBSATAdapter Utility class to use optimization solvers instead of simple SAT solvers in code meant for SAT solvers.
class	PBSolverDecorator A decorator for the PB solvers.
class	PseudoBitsAdderDecorator A decorator that computes minimal pseudo boolean models.
class	PseudoIteratorDecorator A decorator that computes all pseudo boolean models.
class	PseudoOptDecorator A decorator that computes minimal pseudo boolean models.
class	UserFriendlyPBStringSolver<T> Solver to display SAT instances using domain objects names instead of Dimacs numbers.

Methods in org.sat4j.pb that return IProblem

Modifier and Type	Method and Description
protected IProblem	LanceurPseudo2005.readProblem(String problemname)

Uses of IProblem in org.sat4j.pb.core

Subinterfaces of IProblem in org.sat4j.pb.core

Modifier and Type	Interface and Description
interface	IPBCDCLSolver<D extends PBDataStructureFactory> Abstraction for Conflict Driven Clause Learning PBSolver.

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

Modifier and Type	Class and Description
class	ObjectiveReducerPBSolverDecorator
class	PBSolver
class	PBSolverCautious
class	PBSolverClause
class	PBSolverCP
class	PBSolverResCP
class	PBSolverResolution
class	PBSolverWithImpliedClause

Uses of IProblem in org.sat4j.pb.reader

Methods in org.sat4j.pb.reader that return IProblem

Modifier and Type	Method and Description
IProblem	OPBReader2005.parseInstance(InputStream in)
protected IProblem	OPBReader2005.parseInstance(LineNumberReader input)
IProblem	OPBReader2012.parseInstance(Reader input)
IProblem	OPBReader2005.parseInstance(Reader input)
IProblem	OPBReader2010.parseInstance(Reader input)

Uses of IProblem in org.sat4j.pb.tools

Classes in org.sat4j.pb.tools that implement IProblem

Modifier and Type	Class and Description
class	ClausalConstraintsDecorator
class	LexicoDecoratorPB
class	ManyCorePB
class	PBAdapter Allow to put a ISolver when an IPBSolver is required.
class	SteppedTimeoutLexicoDecoratorPB
class	XplainPB

Uses of IProblem in org.sat4j.reader

Methods in org.sat4j.reader that return IProblem

Modifier and Type	Method and Description
IProblem	CSPReader.parseInstance(InputStream in)
IProblem	XMLCSPReader.parseInstance(InputStream in)
IProblem	InstanceReader.parseInstance(InputStream in)
IProblem	AAGReader.parseInstance(InputStream in)
IProblem	JSONReader.parseInstance(InputStream in)
IProblem	LecteurDimacs.parseInstance(InputStream input)
abstract IProblem	Reader.parseInstance(InputStream in) Read a file from a stream.
IProblem	AIGReader.parseInstance(InputStream in)
IProblem	DimacsReader.parseInstance(InputStream in)
IProblem	CSPReader.parseInstance(Reader in)
IProblem	CSPInstanceReader.parseInstance(Reader in)
IProblem	XMLCSPReader.parseInstance(Reader in)
IProblem	Reader.parseInstance(Reader in) Deprecated.
IProblem	CSPInstanceReader.parseInstance(String filename)
IProblem	XMLCSPReader.parseInstance(String filename)
IProblem	InstanceReader.parseInstance(String filename)
IProblem	Reader.parseInstance(String filename) This is the usual method to feed a solver with a benchmark.

Uses of IProblem in org.sat4j.sat

Methods in org.sat4j.sat that return IProblem

Modifier and Type	Method and Description
protected IProblem	Lanceur.readProblem(String problemname) Deprecated.

Methods in org.sat4j.sat with parameters of type IProblem

Modifier and Type	Method and Description
protected void	Lanceur.solve(IProblem problem) Deprecated.

Uses of IProblem in org.sat4j.specs

Subinterfaces of IProblem in org.sat4j.specs

Modifier and Type	Interface and Description
interface	IGroupSolver Represents a CNF in which clauses are grouped into levels.
interface	IOptimizationProblem Represents an optimization problem.
interface	ISolver This interface contains all services provided by a SAT solver.

Uses of IProblem in org.sat4j.tools

Classes in org.sat4j.tools that implement IProblem

Modifier and Type	Class and Description
class	AbstractClauseSelectorSolver<T extends ISolver>
class	AbstractMinimalModel
class	AbstractOutputSolver
class	ClausalCardinalitiesDecorator<T extends ISolver> A decorator for clausal cardinalities constraints.
class	DimacsOutputSolver Solver used to display in a writer the CNF instance in Dimacs format.
class	DimacsStringSolver Solver used to write down a CNF into a String.
class	FullClauseSelectorSolver<T extends ISolver>
class	GateTranslator Utility class to easily feed a SAT solver using logical gates.
class	GroupClauseSelectorSolver<T extends ISolver>
class	LexicoDecorator<T extends ISolver>
class	ManyCore<S extends ISolver> A class allowing to run several solvers in parallel.
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	ModelIteratorToSATAdapter This class allow to use the ModelIterator class as a solver.
class	NegationDecorator<T extends ISolver> Negates the formula inside a solver.
class	OptToSatAdapter
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<T extends ISolver> The aim of that class is to allow adding dynamic responsibilities to SAT solvers using the Decorator design pattern.
class	StatisticsSolver

Uses of IProblem in org.sat4j.tools.xplain

Classes in org.sat4j.tools.xplain that implement IProblem

Modifier and Type	Class and Description
class	HighLevelXplain<T extends ISolver> Computation of MUS in a structured CNF, i.e. the clauses belong to components, the explanation is to be extracted in terms of components.
class	Xplain<T extends ISolver> Explanation framework for SAT4J.