Implementing a CnfToPbDecoder¶

Class Paramita::CnfToPbDecoder¶

A decoder from CNF to Pseudo-Boolean (PB) constraints.

A decoder analyzes a CNF formula and reconstructs one or more PB constraints that are semantically equivalent to a subset of the clauses.

The decoder operates on a ClauseContainer and uses a set of target literals from where constraints will be detected.

Note:

Use CNF_TO_PB_DECODER_C_INTERFACE to register any subclass of this interface.

#include <CnfToPbDecoder.hpp>

Inherits the following classes: Paramita::Plugin

function decode¶

Decode PB constraints from a CNF formula.

virtual std::vector< PbConstraint > Paramita::CnfToPbDecoder::decode (
    ClauseContainer & container,
    std::vector< Literal > target_lits
) = 0

An implementation analyzes the clauses stored in the given ClauseContainer and reconstructs any PB constraints it recognizes. The target_lits parameter is used to restrict the search to constraints involving specific literals.

Parameters:

container The ClauseContainer containing the CNF formula to analyze.
target_lits The literals of interest for the decoding process.

Returns:

A vector containing the decoded PB constraints.

Struct Paramita::PbConstraint¶

A Pseudo-Boolean (PB) constraint.

A PB constraint represents a linear constraint over Boolean literals. It consists of a set of literals, an optional weight associated with each literal, a comparison operator, and a bound.

If no weights are provided, every literal is assumed to have weight 1, resulting in an unweighted cardinality constraint.

A PB constraint has the general form:

[[ \sum_i w_i \cdot l_i \;\mathrm{op}\; b ]]

where:

\(l_i\) are Boolean literals,
\(w_i\) are integer weights (defaulting to 1 when omitted),
\(\mathrm{op}\) is one of the comparison operators defined by OP,
\(b\) is the bound.
#include <definitions.hpp>

Public Types¶

Type	Name
enum	OP Comparison operators for PB constraints.

Public Attributes¶

Type	Name
int	bound
std::vector< Literal >	lits
OP	op
std::optional< std::vector< int64_t > >	weights

Public Functions¶

Type	Name
	PbConstraint (const std::vector< Literal > & lits, OP op, int bound) Constructs an unweighted PB constraint.
	PbConstraint (const std::vector< Literal > & lits, const std::vector< int64_t > & weights, OP op, int bound) Constructs a weighted PB constraint.

Public Types Documentation¶

enum OP¶

Comparison operators for PB constraints.

enum Paramita::PbConstraint::OP {
    LT,
    LTE,
    GT,
    GTE,
    EQ
};

Defines the relation between the weighted sum of literals and the bound.

LT: Less than.
LTE: Less than or equal to.
GT: Greater than.
GTE: Greater than or equal to.
EQ: Equal to.

Public Attributes Documentation¶

variable bound¶

int Paramita::PbConstraint::bound;

The right-hand side bound of the constraint.

variable lits¶

std::vector<Literal> Paramita::PbConstraint::lits;

The literals appearing in the constraint.

variable op¶

OP Paramita::PbConstraint::op;

The comparison operator relating the weighted sum to the bound.

variable weights¶

std::optional<std::vector<int64_t> > Paramita::PbConstraint::weights;

The weight of each literal. If not provided, all literals are assumed to have weight 1.

Public Functions Documentation¶

function PbConstraint [1/2]¶

Constructs an unweighted PB constraint.

inline Paramita::PbConstraint::PbConstraint (
    const std::vector< Literal > & lits,
    OP op,
    int bound
)

All literals are assigned an implicit weight of 1.

Parameters:

lits The literals in the constraint.
op The comparison operator.
bound The bound of the constraint.

function PbConstraint [2/2]¶

Constructs a weighted PB constraint.

inline Paramita::PbConstraint::PbConstraint (
    const std::vector< Literal > & lits,
    const std::vector< int64_t > & weights,
    OP op,
    int bound
)

Parameters:

lits The literals in the constraint.
weights The weight associated with each literal. The size must match the number of literals.
op The comparison operator.
bound The bound of the constraint.