Uses of Interface
org.sat4j.pb.IPBSolver

Packages that use IPBSolver

org.sat4j.maxsat	MAXSAT and Weighted Max SAT 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

Uses of IPBSolver in org.sat4j.maxsat

Classes in org.sat4j.maxsat that implement IPBSolver

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 IPBSolver

IPBSolver	SolverFactory.defaultSolver()
IPBSolver	SolverFactory.lightSolver()
static IPBSolver	SolverFactory.newDefault()
static IPBSolver	SolverFactory.newLight()

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

MinCostDecorator(IPBSolver solver)

WeightedMaxSatDecorator(IPBSolver solver)

WeightedMaxSatDecorator(IPBSolver solver, boolean equivalence)

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)