Skip to content

Commit

Permalink
feat: extending PB constraints to cardinalities
Browse files Browse the repository at this point in the history
this can also be used if the constraint is not a cardinality yet, it
will repeat input literals then
  • Loading branch information
chrjabs committed Mar 4, 2025
1 parent d8254bb commit 45cca3c
Showing 1 changed file with 71 additions and 1 deletion.
72 changes: 71 additions & 1 deletion src/types/constraints.rs
Original file line number Diff line number Diff line change
Expand Up @@ -1439,7 +1439,8 @@ impl PbConstraint {
self.into_card_constr()
}

/// Converts the pseudo-boolean constraint into a cardinality constraint, if possible
/// Converts the pseudo-boolean constraint into a cardinality constraint, only if the
/// constraint is already a cardinality
///
/// # Errors
///
Expand Down Expand Up @@ -1498,6 +1499,21 @@ impl PbConstraint {
})
}

/// Extends the constraint into a cardinality constraint by repeating literals as often as
/// their coefficient requires
///
/// # Panics
///
/// If the constraint is UNSAT or a tautology
#[must_use]
pub fn extend_to_card_constr(self) -> CardConstraint {
match self {
PbConstraint::Ub(constr) => CardConstraint::Ub(constr.extend_to_card_constr()),
PbConstraint::Lb(constr) => CardConstraint::Lb(constr.extend_to_card_constr()),
PbConstraint::Eq(constr) => CardConstraint::Eq(constr.extend_to_card_constr()),
}
}

/// Converts the constraint into a clause, if possible
#[deprecated(
since = "0.5.0",
Expand Down Expand Up @@ -1758,6 +1774,24 @@ impl PbUbConstr {
}
}

/// Extends the constraint into a cardinality constraint by repeating literals as often as
/// their coefficient requires
///
/// # Panics
///
/// If the constraint is UNSAT
#[must_use]
pub fn extend_to_card_constr(self) -> CardUbConstr {
CardUbConstr {
lits: self
.lits
.into_iter()
.flat_map(|(l, w)| std::iter::repeat(l).take(w))
.collect(),
b: self.b.unsigned_abs(),
}
}

/// Checks if the constraint is always satisfied
#[must_use]
pub fn is_tautology(&self) -> bool {
Expand Down Expand Up @@ -1874,6 +1908,24 @@ impl PbLbConstr {
}
}

/// Extends the constraint into a cardinality constraint by repeating literals as often as
/// their coefficient requires
///
/// # Panics
///
/// If the constraint is a tautology
#[must_use]
pub fn extend_to_card_constr(self) -> CardLbConstr {
CardLbConstr {
lits: self
.lits
.into_iter()
.flat_map(|(l, w)| std::iter::repeat(l).take(w))
.collect(),
b: self.b.unsigned_abs(),
}
}

/// Checks if the constraint is always satisfied
#[must_use]
pub fn is_tautology(&self) -> bool {
Expand Down Expand Up @@ -1987,6 +2039,24 @@ impl PbEqConstr {
)
}

/// Extends the constraint into a cardinality constraint by repeating literals as often as
/// their coefficient requires
///
/// # Panics
///
/// If the constraint is UNSAT
#[must_use]
pub fn extend_to_card_constr(self) -> CardEqConstr {
CardEqConstr {
lits: self
.lits
.into_iter()
.flat_map(|(l, w)| std::iter::repeat(l).take(w))
.collect(),
b: self.b.unsigned_abs(),
}
}

/// Checks if the constraint is unsatisfiable
///
/// This only checks whether the bound is smaller than the sum of weights, not if a subset sum
Expand Down

0 comments on commit 45cca3c

Please sign in to comment.