Struct pblib_rs::PB2CNF

#[repr(C)]
pub struct PB2CNF(/* private fields */);

The entry point for the Rust bindings.

This structure is a wrapper around the underlying C structure that provides a safe interface to the pblib functions. It gives access to the functions dedicated to the encoding of cardinality and Pseudo-Boolean constraints.

Encoding cardinality constraints

Cardinality constraints are encoded thanks to the encode_at_least_k and encode_at_most_k functions. They take as input the list of literals (in the DIMACS format) the constraints relies on, the bound, and the minimal variable index that can be used as an auxiliary variables must be given to the function. Auxiliary variables are often used in such encodings since they allow to use less clauses to encode the constraint. The preferred value for this parameter is in most cases the highest variable index in use plus 1.

The result of this function is an EncodingResult which gives both the clauses encoding the constraint (as a vector of DIMACS-encoded literals) and the new lowest variable index that is not in use.

use pblib_rs::PB2CNF;

// we encode x1 + x2 + x3 >= 2
let literals = vec![1, 2, 3];
let pb2cnf = PB2CNF::new();
// the threshold is 2 and the first variable not in use is 4
let encoding = pb2cnf.encode_at_least_k(literals, 2, 4);
println!("the encoding uses {} variables", encoding.next_free_var_id() - 4);
println!("the encoding uses {} clauses", encoding.clauses().len());
encoding.clauses().iter().enumerate().for_each(|(i,c)| println!("clause {i} is {:?}", c));

Encoding Pseudo-Boolean constraints

The difference between cardinality and Pseudo-Boolean constraints is than weights are applied to literals. Thus, the functions dedicated to this kind of constraints (encode_geq, encode_leq and encode_both) takes a vector of weights as a supplementary parameter. The vectors of weights and literals must be of same lengths, since variable at index i has the weight at index i.

use pblib_rs::PB2CNF;

// we encode 8*x1 + 4*x2 + 2*x3 + 1*x4 >= 6
let weights = vec![8, 4, 2, 1];
let literals = vec![1, 2, 3, 4];
let pb2cnf = PB2CNF::new();
// the threshold is 6 and the first variable not in use is 5
let encoding = pb2cnf.encode_geq(weights.clone(), literals, 6, 5);
println!("the encoding uses {} variables", encoding.next_free_var_id() - 4);
println!("the encoding uses {} clauses", encoding.clauses().len());
encoding.clauses().iter().enumerate().for_each(|(i,c)| println!("clause {i} is {:?}", c));

Note about the encodings

Contrary to pblib, pblib-rs does not allow the user to choose the encoding use for the constraint. The encoding used for the constraints are the default ones of the pblib. In particular, the encodings provided by this library are not intended to match the expected model count of the formula.

Implementations

impl PB2CNF

pub fn new() -> Self

Builds a new structure dedicated to the encoding of constraints.

pub fn encode_leq( &self, weights: Vec<i64>, literals: Vec<i32>, leq: i64, first_aux_var: i32 ) -> EncodingResult

Encodes an At-Most-k Pseudo-Boolean constraint.

An At-Most-k constraint imposes that a weighted sum of literals is less than or equal to an integer value. The vectors of weights and literals must be of same lengths, since variable at index i has the weight at index i.

In addition to this vectors and the threshold, the minimal variable index that can be used as an auxiliary variables must be given to the function. The preferred value for this parameter is in most cases the highest variable index in use plus 1.

The result of this function is an EncodingResult which gives both the clauses encoding the constraint and the new lowest variable index that is not in use.

Panics

In case the weights and literal vectors have not the same length, this function panics.

pub fn encode_geq( &self, weights: Vec<i64>, literals: Vec<i32>, geq: i64, first_aux_var: i32 ) -> EncodingResult

Encodes an At-Least-k Pseudo-Boolean constraint.

An At-Least-k constraint imposes that a weighted sum of literals is greater than or equal to an integer value. The vectors of weights and literals must be of same lengths, since variable at index i has the weight at index i.

In addition to this vectors and the threshold, the minimal variable index that can be used as an auxiliary variables must be given to the function. The preferred value for this parameter is in most cases the highest variable index in use plus 1.

The result of this function is an EncodingResult which gives both the clauses encoding the constraint and the new lowest variable index that is not in use.

Panics

In case the weights and literal vectors have not the same length, this function panics.

pub fn encode_both( &self, weights: Vec<i64>, literals: Vec<i32>, less_or_eq: i64, greater_or_eq: i64, first_aux_var: i32 ) -> EncodingResult

Encodes both an At-Most-k and an At-Least-p Pseudo-Boolean constraints that refers to the same variables and weights.

See encode_leq and encode_geq for more information on At-Most-k and At-Least-p constraints, the first_aux_var parameter and the return type. A call to this function is intended to be more efficient in terms of encoding comparing to a call to encode_leq and a call to encode_geq.

Panics

In case the weights and literal vectors have not the same length, this function panics.

pub fn encode_at_most_k( &self, literals: Vec<i32>, k: i64, first_aux_var: i32 ) -> EncodingResult

Encodes an At-Most-k cardinality constraint.

An At-Most-k cardinality constraint imposes that at most k literals in a vector are set to true.

In addition to this vector and the threshold, the minimal variable index that can be used as an auxiliary variables must be given to the function. The preferred value for this parameter is in most cases the highest variable index in use plus 1.

The result of this function is an EncodingResult which gives both the clauses encoding the constraint and the new lowest variable index that is not in use.

pub fn encode_at_least_k( &self, literals: Vec<i32>, k: i64, first_aux_var: i32 ) -> EncodingResult

Encodes an At-Least-k cardinality constraint.

An At-Least-k cardinality constraint imposes that at least k literals in a vector are set to true.

In addition to this vector and the threshold, the minimal variable index that can be used as an auxiliary variables must be given to the function. The preferred value for this parameter is in most cases the highest variable index in use plus 1.

The result of this function is an EncodingResult which gives both the clauses encoding the constraint and the new lowest variable index that is not in use.

Trait Implementations

impl Default for PB2CNF

fn default() -> Self

Returns the “default value” for a type.

impl Drop for PB2CNF

fn drop(&mut self)

Executes the destructor for this type.