Uses of Interface
org.sat4j.pb.IPBSolver

Packages that use IPBSolver

Package	Description
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

Uses of IPBSolver in org.sat4j.pb

Classes in org.sat4j.pb that implement IPBSolver

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 IPBSolver

Modifier and Type	Method and Description
IPBSolver	SolverFactory.lightSolver()
static IPBSolver	SolverFactory.newBoth() Resolution and CuttingPlanes based solvers running in parallel.
static IPBSolver	SolverFactory.newCuttingPlanes() Cutting Planes based solver.
static IPBSolver	SolverFactory.newCuttingPlanesAggressiveCleanup() Cutting Planes based solver.
static IPBSolver	SolverFactory.newDefaultNonNormalized() Default solver of the SolverFactory for instances not normalized.
static IPBSolver	SolverFactory.newDefaultOptimizer() Provides the best available PB solver of the library ready to solve optimization problems.
static IPBSolver	SolverFactory.newEclipseP2()
static IPBSolver	SolverFactory.newLight() Small footprint SAT solver.
static IPBSolver	SolverFactory.newOPBStringSolver()
static IPBSolver	SolverFactory.newResolution() Resolution based solver (i.e. classic SAT solver able to handle generic constraints.
static IPBSolver	SolverFactory.newResolutionMaxMemory() Resolution based solver (i.e. classic SAT solver able to handle generic constraints.
static IPBSolver	SolverFactory.newResolutionSimpleRestarts() Resolution based solver (i.e. classic SAT solver able to handle generic constraints.
static IPBSolver	SolverFactory.newSATUNSAT() Two solvers are running in //: one for solving SAT instances, the other one for solving unsat instances.
static IPBSolver	SolverFactory.newSimpleSimplification() Resolution based solver (i.e. classic SAT solver able to handle generic constraints.

Constructors in org.sat4j.pb with parameters of type IPBSolver

Constructor and Description
ConstraintRelaxingPseudoOptDecorator(IPBSolver solver)
PBSolverDecorator(IPBSolver solver)
PseudoBitsAdderDecorator(IPBSolver solver)
PseudoIteratorDecorator(IPBSolver solver)
PseudoOptDecorator(IPBSolver solver) Create a PB decorator for which a non optimal solution means that the problem is satisfiable.
PseudoOptDecorator(IPBSolver solver, boolean nonOptimalMeansSatisfiable) Create a PB decorator with a specific semantic of non optimal solution.
PseudoOptDecorator(IPBSolver solver, boolean nonOptimalMeansSatisfiable, boolean useAnImplicantForEvaluation) Create a PB decorator with a specific semantic of non optimal solution.

Constructor parameters in org.sat4j.pb with type arguments of type IPBSolver

Constructor and Description
LanceurPseudo2007(ASolverFactory<IPBSolver> factory)

Uses of IPBSolver in org.sat4j.pb.core

Subinterfaces of IPBSolver 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 IPBSolver

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

Constructors in org.sat4j.pb.core with parameters of type IPBSolver

Constructor and Description
ObjectiveReducerPBSolverDecorator(IPBSolver decorated)

Uses of IPBSolver in org.sat4j.pb.reader

Fields in org.sat4j.pb.reader declared as IPBSolver

Modifier and Type	Field and Description
protected IPBSolver	OPBReader2005.solver

Constructors in org.sat4j.pb.reader with parameters of type IPBSolver

Constructor and Description
JSONPBReader(IPBSolver solver)
OPBEclipseReader2007(IPBSolver solver)
OPBReader2005(IPBSolver solver)
OPBReader2006(IPBSolver solver)
OPBReader2007(IPBSolver solver)
OPBReader2010(IPBSolver solver)
OPBReader2012(IPBSolver solver)
PBInstanceReader(IPBSolver solver)

Uses of IPBSolver in org.sat4j.pb.tools

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

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

Methods in org.sat4j.pb.tools that return IPBSolver

Modifier and Type	Method and Description
IPBSolver	DependencyHelper.getSolver()

Constructors in org.sat4j.pb.tools with parameters of type IPBSolver

Constructor and Description
ClausalConstraintsDecorator(IPBSolver solver)
ClausalConstraintsDecorator(IPBSolver solver, EncodingStrategyAdapter encodingAd)
DependencyHelper(IPBSolver solver)
DependencyHelper(IPBSolver solver, boolean explanationEnabled)
DependencyHelper(IPBSolver solver, boolean explanationEnabled, boolean canonicalOptFunctionEnabled)
LexicoDecoratorPB(IPBSolver solver)
LexicoHelper(IPBSolver solver)
LexicoHelper(IPBSolver solver, boolean explanationEnabled)
LexicoHelper(IPBSolver solver, boolean explanationEnabled, boolean canonicalOptFunctionEnabled)
ManyCorePB(IPBSolver... iSolver)
SteppedTimeoutLexicoDecoratorPB(IPBSolver solver)
SteppedTimeoutLexicoHelper(IPBSolver solver)
SteppedTimeoutLexicoHelper(IPBSolver solver, boolean explanationEnabled)
SteppedTimeoutLexicoHelper(IPBSolver solver, boolean explanationEnabled, boolean canonicalOptFunctionEnabled)
XplainPB(IPBSolver solver)

Constructor parameters in org.sat4j.pb.tools with type arguments of type IPBSolver

Constructor and Description
ManyCorePB(ASolverFactory<IPBSolver> factory, String... solverNames)