Struct PbConstraint 

pub struct PbConstraint { /* private fields */ }

A normalized pseudo-Boolean constraint Σ coeff·lit ≥ degree: every coeff > 0, every variable appears at most once, and the literal sign rides the entry — (coeff, positive) with positive == false meaning the literal ¬x. degree may be ≤ 0 (then the constraint is trivially true) or exceed the coefficient sum (then it is a contradiction).

Implementations

impl PbConstraint

pub fn at_least(lits: &[(usize, bool)], k: i64) -> PbConstraint

Σ ℓ ≥ k over the given literals (each coefficient 1). Literals must be over distinct variables (the caller’s responsibility — true for clause/cardinality inputs).

pub fn clause(lits: &[(usize, bool)]) -> PbConstraint

A CNF clause ℓ₁ ∨ … ∨ ℓₖ as the PB constraint Σ ℓ ≥ 1 — the bridge that lets the cutting plane engine consume ordinary SAT clauses (and p-simulate resolution on them).

pub fn at_most(lits: &[(usize, bool)], k: i64) -> PbConstraint

Σ ℓ ≤ k, normalized to ≥ form by flipping every literal: Σ ¬ℓ ≥ n − k.

pub fn degree(&self) -> i64

The degree (right-hand side).

pub fn len(&self) -> usize

Number of (non-cancelled) terms.

pub fn is_empty(&self) -> bool

pub fn add(&self, other: &PbConstraint) -> PbConstraint

Addition — LHS₁ + LHS₂ ≥ d₁ + d₂, then re-normalized. A variable that is x in one and ¬x in the other partially cancels (a·x + b·¬x = (a−b)·x + b), so the shared minimum min(a,b) leaves the literal and is moved to the right, dropping the degree by min(a,b). Sound: the sum of two valid ≥ constraints is valid, and x + ¬x = 1 is exact for 0/1.

pub fn multiply(&self, c: i64) -> PbConstraint

Multiplication by a positive integer — c·LHS ≥ c·degree. Trivially sound (scaling a valid ≥ constraint by c > 0).

pub fn divide_round(&self, d: i64) -> PbConstraint

Division with rounding-up (the Gomory–Chvátal cut) — Σ ⌈aᵢ/d⌉·ℓᵢ ≥ ⌈degree/d⌉. Sound ONLY because variables are integral: ⌈aᵢ/d⌉ ≥ aᵢ/d so the LHS only grows (≥ degree/d), and being an integer it is ≥ ⌈degree/d⌉. This rounding of the fractional slack is exactly what makes cutting planes stronger than resolution.

pub fn saturate(&self) -> PbConstraint

Saturation — clamp every coefficient to the degree (min(aᵢ, degree)). A single 0/1 variable can contribute at most degree toward the bound, so the excess is redundant. Sound, and it keeps coefficients from blowing up across many additions.

pub fn is_contradiction(&self) -> bool

A constraint NO 0/1 assignment can satisfy: the maximum possible LHS (every coefficient counted) is still below the degree. The terminal of a refutation — e.g. 0 ≥ 1.

pub fn is_satisfied(&self, assign: &dyn Fn(usize) -> bool) -> bool

Evaluate under assign (a variable → bool map; unmentioned variables are false): does Σ coeff·[literal true] ≥ degree hold? The oracle the rule soundness tests check against.

pub fn new_weighted(terms: &[(usize, i64, bool)], degree: i64) -> PbConstraint

Σ coeffᵢ·litᵢ ≥ degree directly from weighted terms (var, coeff, positive) — for constraints whose coefficients are not all 1.

pub fn term(&self, v: usize) -> Option<(i64, bool)>

The (coeff, positive) term on variable v, or None if v does not occur.

pub fn terms(&self) -> impl Iterator<Item = (usize, i64, bool)> + '_

Iterate the constraint’s terms as (variable, coeff, positive) — the public view of the otherwise-private normalized map, so a live theory can read a constraint without owning it.

Trait Implementations

impl Clone for PbConstraint

fn clone(&self) -> PbConstraint

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for PbConstraint

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Eq for PbConstraint

impl PartialEq for PbConstraint

fn eq(&self, other: &PbConstraint) -> bool

Equality operator ==.

fn ne(&self, other: &Rhs) -> bool

Inequality operator !=.

impl StructuralPartialEq for PbConstraint