smtrat::TotalizerEncoder Class Reference

TotalizerEncoder implements the Totalizer encoding as described in "Incremental Cardinality Constraints for MaxSAT" by Martins et al https://doi.org/10.1007/978-3-319-10428-7_39. More...

#include <TotalizerEncoder.h>

Inheritance diagram for smtrat::TotalizerEncoder:

Collaboration diagram for smtrat::TotalizerEncoder:

Public Member Functions
	TotalizerEncoder ()
	~TotalizerEncoder ()
bool	canEncode (const ConstraintT &constraint)
Rational	encodingSize (const ConstraintT &constraint)
std::string	name ()
std::optional< FormulaT >	encode (const ConstraintT &constraint)
	Encodes an arbitrary constraint. More...

Data Fields
std::size_t	problem_size

Protected Member Functions
std::optional< FormulaT >	doEncode (const ConstraintT &constraint)
FormulaT	generateVarChain (const std::set< carl::Variable > &vars, carl::FormulaType type)

Private Member Functions
TotalizerTree	buildTree (const std::set< carl::Variable > &variables)
FormulaT	encodeSumPropagation (TotalizerTree &tree)
FormulaT	encodeCardinalityRestriction (TotalizerTree &tree, Rational constantPart)
ConstraintT	normalizeLessConstraint (const ConstraintT &constraint)

Private Attributes
std::map< carl::Variables, TotalizerTree * >	mTreeCache
std::map< carl::Variables, FormulaT >	mSumPropagationFormulaCache

Detailed Description

TotalizerEncoder implements the Totalizer encoding as described in "Incremental Cardinality Constraints for MaxSAT" by Martins et al https://doi.org/10.1007/978-3-319-10428-7_39.

Definition at line 14 of file TotalizerEncoder.h.

Constructor & Destructor Documentation

TotalizerEncoder()

smtrat::TotalizerEncoder::TotalizerEncoder ( )

inline

Definition at line 16 of file TotalizerEncoder.h.

~TotalizerEncoder()

smtrat::TotalizerEncoder::~TotalizerEncoder

(

)

Definition at line 155 of file TotalizerEncoder.cpp.

Member Function Documentation

buildTree()

TotalizerTree smtrat::TotalizerEncoder::buildTree ( const std::set< carl::Variable > &  variables )

private

canEncode()

bool smtrat::TotalizerEncoder::canEncode ( const ConstraintT &  constraint )

virtual

Implements smtrat::PseudoBoolEncoder.

Definition at line 85 of file TotalizerEncoder.cpp.

Here is the caller graph for this function:

doEncode()

std::optional< FormulaT > smtrat::TotalizerEncoder::doEncode ( const ConstraintT &  constraint )

protectedvirtual

Implements smtrat::PseudoBoolEncoder.

Definition at line 4 of file TotalizerEncoder.cpp.

Here is the call graph for this function:

encode()

std::optional< FormulaT > smtrat::PseudoBoolEncoder::encode ( const ConstraintT &  constraint )

inherited

Encodes an arbitrary constraint.

Returns

encoded formula

Definition at line 5 of file PseudoBoolEncoder.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

encodeCardinalityRestriction()

FormulaT smtrat::TotalizerEncoder::encodeCardinalityRestriction ( TotalizerTree &  tree, Rational  constantPart  )

private

Definition at line 67 of file TotalizerEncoder.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

encodeSumPropagation()

FormulaT smtrat::TotalizerEncoder::encodeSumPropagation ( TotalizerTree &  tree )

private

Definition at line 23 of file TotalizerEncoder.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

encodingSize()

Rational smtrat::TotalizerEncoder::encodingSize ( const ConstraintT &  constraint )

virtual

Reimplemented from smtrat::PseudoBoolEncoder.

Definition at line 104 of file TotalizerEncoder.cpp.

Here is the call graph for this function:

generateVarChain()

FormulaT smtrat::PseudoBoolEncoder::generateVarChain ( const std::set< carl::Variable > &  vars, carl::FormulaType  type  )

protectedinherited

Definition at line 38 of file PseudoBoolEncoder.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

name()

std::string smtrat::TotalizerEncoder::name ( )

inlinevirtual

Reimplemented from smtrat::PseudoBoolEncoder.

Definition at line 23 of file TotalizerEncoder.h.

normalizeLessConstraint()

ConstraintT smtrat::PseudoBoolEncoder::normalizeLessConstraint ( const ConstraintT &  constraint )

privateinherited

Definition at line 25 of file PseudoBoolEncoder.cpp.

Here is the caller graph for this function:

Field Documentation

mSumPropagationFormulaCache

std::map<carl::Variables, FormulaT> smtrat::TotalizerEncoder::mSumPropagationFormulaCache

private

Definition at line 33 of file TotalizerEncoder.h.

mTreeCache

std::map<carl::Variables, TotalizerTree*> smtrat::TotalizerEncoder::mTreeCache

private

Definition at line 32 of file TotalizerEncoder.h.

problem_size

std::size_t smtrat::PseudoBoolEncoder::problem_size

inherited

Definition at line 20 of file PseudoBoolEncoder.h.

---

The documentation for this class was generated from the following files:

• smtrat-modules/PBPPModule/Encoders/TotalizerEncoder.h
• smtrat-modules/PBPPModule/Encoders/TotalizerEncoder.cpp