Implementing a PbToCnfEncoder¶

Pseudo-Boolean encoders allow to translate Cardinality Constraints and Pseudo-Boolean Constraints to SAT clauses.

Class Paramita::PbToCnfEncoder¶

An encoder from PB constraints to Satisfiability CNF.

Note:

Use PB_TO_CNF_ENCODER_C_INTERFACE to register any subclass of this interface.

#include <PbToCnfEncoder.hpp>

Inherits the following classes: Paramita::Plugin

function encode¶

Encode the PB constraint to the specified container.

virtual Context Paramita::PbToCnfEncoder::encode (
    const PbConstraint & constraint,
    ClauseContainer & container,
    Context context
) = 0

This method receives an optional Context that the encoder can use to encode constraints incrementally.

In this sense, it can also return another Context to be used by the same encoder later.

Non-incremental encoders can fully ignore the Context, both as parameter and return value.

Parameters:

constraint The PbConstraint to be encoded to CNF.
container A ClauseContainer where clauses will be added.
context An (possibly empty) Context for incremental encoders.

Returns:

A (possibly empty) Context to be used by the same encoder to incrementally encode constraints in subsequent calls.

Class Paramita::PbToCnfEncoder::ContextState¶

Opaque type for storing arbitrary context for incremental encoders.

#include <PbToCnfEncoder.hpp>

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.