|
||||||||||
PREV NEXT | FRAMES NO FRAMES |
Packages that use IPBSolver | |
---|---|
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 | |
---|---|
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 | |
---|---|
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.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 | |
---|---|
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 | |
---|---|
LanceurPseudo2007(ASolverFactory<IPBSolver> factory)
|
Uses of IPBSolver in org.sat4j.pb.core |
---|
Subinterfaces of IPBSolver in org.sat4j.pb.core | |
---|---|
interface |
IPBCDCLSolver<D extends PBDataStructureFactory>
Abstraction for Conflict Driven Clause Learning PBSolver. |
Classes in org.sat4j.pb.core that implement IPBSolver | |
---|---|
class |
PBSolver
|
class |
PBSolverCautious
|
class |
PBSolverClause
|
class |
PBSolverCP
|
class |
PBSolverResCP
|
class |
PBSolverResolution
|
class |
PBSolverWithImpliedClause
|
Uses of IPBSolver in org.sat4j.pb.reader |
---|
Fields in org.sat4j.pb.reader declared as IPBSolver | |
---|---|
protected IPBSolver |
OPBReader2005.solver
|
Constructors in org.sat4j.pb.reader with parameters of type IPBSolver | |
---|---|
OPBEclipseReader2007(IPBSolver solver)
|
|
OPBReader2005(IPBSolver solver)
|
|
OPBReader2006(IPBSolver solver)
|
|
OPBReader2007(IPBSolver solver)
|
|
OPBReader2010(IPBSolver solver)
|
|
PBInstanceReader(IPBSolver solver)
|
Uses of IPBSolver in org.sat4j.pb.tools |
---|
Classes in org.sat4j.pb.tools that implement IPBSolver | |
---|---|
class |
ClausalConstraintsDecorator
|
class |
LexicoDecoratorPB
|
class |
ManyCorePB
|
class |
XplainPB
|
Methods in org.sat4j.pb.tools that return IPBSolver | |
---|---|
IPBSolver |
DependencyHelper.getSolver()
|
Constructors in org.sat4j.pb.tools with parameters of type IPBSolver | |
---|---|
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)
|
|
XplainPB(IPBSolver solver)
|
Constructor parameters in org.sat4j.pb.tools with type arguments of type IPBSolver | |
---|---|
ManyCorePB(ASolverFactory<IPBSolver> factory,
String... solverNames)
|
|
||||||||||
PREV NEXT | FRAMES NO FRAMES |