Uses of Class
org.sat4j.tools.SolverDecorator

Packages that use SolverDecorator

Package	Description
org.sat4j.maxsat	MAXSAT and Weighted Max SAT framework.
org.sat4j.opt	Built-in optimization framework.
org.sat4j.pb	Implementations of pseudo boolean solvers
org.sat4j.pb.tools	Implementation of different tools for pseudo boolean solvers
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 SolverDecorator in org.sat4j.maxsat

Subclasses of SolverDecorator in org.sat4j.maxsat

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.

Uses of SolverDecorator in org.sat4j.opt

Subclasses of SolverDecorator in org.sat4j.opt

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 SolverDecorator in org.sat4j.pb

Subclasses of SolverDecorator in org.sat4j.pb

Modifier and Type	Class and Description
class	ConstraintRelaxingPseudoOptDecorator
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.

Uses of SolverDecorator in org.sat4j.pb.tools

Subclasses of SolverDecorator in org.sat4j.pb.tools

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

Uses of SolverDecorator in org.sat4j.tools

Subclasses of SolverDecorator in org.sat4j.tools

Modifier and Type	Class and Description
class	AbstractClauseSelectorSolver<T extends ISolver>
class	AbstractMinimalModel
class	ClausalCardinalitiesDecorator<T extends ISolver> A decorator for clausal cardinalities constraints.
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	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.

Uses of SolverDecorator in org.sat4j.tools.xplain

Subclasses of SolverDecorator in org.sat4j.tools.xplain

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.