feat: certified card/PB constraint encodings

data/single-card-eq.opb

@@ -0,0 +1 @@
+1 x1 1 x2 1 x3 1 x4 = 2

data/single-ub.opb

@@ -0,0 +1 @@
+-3 x1 -2 x2 +4 x3 -7 x4 >= -2 ;

src/encodings/card/cert.rs

@@ -2,7 +2,20 @@
 
 use std::ops::RangeBounds;
 
-use crate::{encodings::CollectCertClauses, instances::ManageVars};
+use pigeons::AbsConstraintId;
+
+use crate::{
+    clause,
+    encodings::CollectCertClauses,
+    instances::ManageVars,
+    types::{
+        constraints::{CardConstraint, CardEqConstr, CardLbConstr, CardUbConstr},
+        Lit,
+    },
+    utils::unreachable_err,
+};
+
+use super::DbTotalizer;
 
 /// Trait for certified cardinality encodings that allow upper bounding of the form `sum of lits <=
 /// ub`
@@ -27,6 +40,23 @@ pub trait BoundUpper: super::Encode + super::BoundUpper {
         Col: CollectCertClauses,
         R: RangeBounds<usize>,
         W: std::io::Write;
+
+    /// Encodes an upper bound cardinality constraint to CNF with proof logging
+    ///
+    /// # Errors
+    ///
+    /// - Either an [`super::Error`] or [`crate::OutOfMemory`]
+    /// - [`std::io::Error`] if writing the proof fails
+    fn encode_ub_constr_cert<Col, W>(
+        constr: (CardUbConstr, AbsConstraintId),
+        collector: &mut Col,
+        var_manager: &mut dyn ManageVars,
+        proof: &mut pigeons::Proof<W>,
+    ) -> anyhow::Result<()>
+    where
+        Col: CollectCertClauses,
+        W: std::io::Write,
+        Self: FromIterator<Lit> + Sized;
 }
 
 /// Trait for certified cardinality encodings that allow lower bounding of the form `sum of lits >=
@@ -52,6 +82,23 @@ pub trait BoundLower: super::Encode + super::BoundLower {
         Col: CollectCertClauses,
         R: RangeBounds<usize>,
         W: std::io::Write;
+
+    /// Encodes a lower bound cardinality constraint to CNF with proof logging
+    ///
+    /// # Errors
+    ///
+    /// - Either an [`super::Error`] or [`crate::OutOfMemory`]
+    /// - [`std::io::Error`] if writing the proof fails
+    fn encode_lb_constr_cert<Col, W>(
+        constr: (CardLbConstr, AbsConstraintId),
+        collector: &mut Col,
+        var_manager: &mut dyn ManageVars,
+        proof: &mut pigeons::Proof<W>,
+    ) -> anyhow::Result<()>
+    where
+        Col: CollectCertClauses,
+        W: std::io::Write,
+        Self: FromIterator<Lit> + Sized;
 }
 
 /// Trait for certified cardinality encodings that allow upper and lower bounding
@@ -81,6 +128,62 @@ pub trait BoundBoth: BoundUpper + BoundLower {
         self.encode_lb_cert(range, collector, var_manager, proof)?;
         Ok(())
     }
+
+    /// Encodes an equality carinality constraint to CNF with proof logging
+    ///
+    /// # Errors
+    ///
+    /// - Either an [`super::Error`] or [`crate::OutOfMemory`]
+    /// - [`std::io::Error`] if writing the proof fails
+    fn encode_eq_constr_cert<Col, W>(
+        constr: (CardEqConstr, AbsConstraintId),
+        collector: &mut Col,
+        var_manager: &mut dyn ManageVars,
+        proof: &mut pigeons::Proof<W>,
+    ) -> anyhow::Result<()>
+    where
+        Col: CollectCertClauses,
+        W: std::io::Write,
+        Self: FromIterator<Lit> + Sized,
+    {
+        // Assume the two constraints have ID as given and +1
+        let (constr, id) = constr;
+        let (lb_c, ub_c) = constr.split();
+        Self::encode_lb_constr_cert((lb_c, id), collector, var_manager, proof)?;
+        Self::encode_ub_constr_cert((ub_c, id + 1), collector, var_manager, proof)?;
+        Ok(())
+    }
+
+    /// Encodes any carinality constraint to CNF with proof logging
+    ///
+    /// # Errors
+    ///
+    /// - Either an [`super::Error`] or [`crate::OutOfMemory`]
+    /// - [`std::io::Error`] if writing the proof fails
+    fn encode_constr_cert<Col, W>(
+        constr: (CardConstraint, AbsConstraintId),
+        collector: &mut Col,
+        var_manager: &mut dyn ManageVars,
+        proof: &mut pigeons::Proof<W>,
+    ) -> anyhow::Result<()>
+    where
+        Col: CollectCertClauses,
+        W: std::io::Write,
+        Self: FromIterator<Lit> + Sized,
+    {
+        let (constr, id) = constr;
+        match constr {
+            CardConstraint::Ub(constr) => {
+                Self::encode_ub_constr_cert((constr, id), collector, var_manager, proof)
+            }
+            CardConstraint::Lb(constr) => {
+                Self::encode_lb_constr_cert((constr, id), collector, var_manager, proof)
+            }
+            CardConstraint::Eq(constr) => {
+                Self::encode_eq_constr_cert((constr, id), collector, var_manager, proof)
+            }
+        }
+    }
 }
 
 /// Default implementation of [`BoundBoth`] for every encoding that does upper
@@ -171,3 +274,117 @@ pub trait BoundBothIncremental: BoundUpperIncremental + BoundLowerIncremental {
 /// Default implementation of [`BoundBothIncremental`] for every encoding that
 /// does incremental upper and lower bounding
 impl<CE> BoundBothIncremental for CE where CE: BoundUpperIncremental + BoundLowerIncremental {}
+
+/// The default upper bound encoding. For now this is a [`DbTotalizer`].
+pub type DefUpperBounding = DbTotalizer;
+/// The default lower bound encoding. For now this is a [`DbTotalizer`].
+pub type DefLowerBounding = DbTotalizer;
+/// The default encoding for both bounds. For now this is a [`DbTotalizer`].
+pub type DefBothBounding = DbTotalizer;
+/// The default incremental upper bound encoding. For now this is a [`DbTotalizer`].
+pub type DefIncUpperBounding = DbTotalizer;
+/// The default incremental lower bound encoding. For now this is a [`DbTotalizer`].
+pub type DefIncLowerBounding = DbTotalizer;
+/// The default incremental encoding for both bounds. For now this is a [`DbTotalizer`].
+pub type DefIncBothBounding = DbTotalizer;
+
+/// Constructs a default upper bounding cardinality encoding.
+#[must_use]
+pub fn new_default_ub() -> impl BoundUpper {
+    DefUpperBounding::default()
+}
+
+/// Constructs a default lower bounding cardinality encoding.
+#[must_use]
+pub fn new_default_lb() -> impl BoundLower {
+    DefLowerBounding::default()
+}
+
+/// Constructs a default double bounding cardinality encoding.
+#[must_use]
+pub fn new_default_both() -> impl BoundBoth {
+    DefBothBounding::default()
+}
+
+/// Constructs a default incremental upper bounding cardinality encoding.
+#[must_use]
+pub fn new_default_inc_ub() -> impl BoundUpperIncremental {
+    DefIncUpperBounding::default()
+}
+
+/// Constructs a default incremental lower bounding cardinality encoding.
+#[must_use]
+pub fn new_default_inc_lb() -> impl BoundLower {
+    DefIncLowerBounding::default()
+}
+
+/// Constructs a default incremental double bounding cardinality encoding.
+#[must_use]
+pub fn new_default_inc_both() -> impl BoundBoth {
+    DefIncBothBounding::default()
+}
+
+/// A default encoder for any cardinality constraint. This uses a
+/// [`DefBothBounding`] to encode non-trivial constraints.
+///
+/// # Errors
+///
+/// If the clause collector runs out of memory, returns [`crate::OutOfMemory`].
+pub fn default_encode_cardinality_constraint<Col: CollectCertClauses, W: std::io::Write>(
+    constr: (CardConstraint, AbsConstraintId),
+    collector: &mut Col,
+    var_manager: &mut dyn ManageVars,
+    proof: &mut pigeons::Proof<W>,
+) -> anyhow::Result<()> {
+    encode_cardinality_constraint::<DefBothBounding, Col, W>(constr, collector, var_manager, proof)
+}
+
+/// An encoder for any cardinality constraint with an encoding of choice
+///
+/// # Errors
+///
+/// If the clause collector runs out of memory, returns [`crate::OutOfMemory`].
+pub fn encode_cardinality_constraint<
+    CE: BoundBoth + FromIterator<Lit>,
+    Col: CollectCertClauses,
+    W: std::io::Write,
+>(
+    constr: (CardConstraint, AbsConstraintId),
+    collector: &mut Col,
+    var_manager: &mut dyn ManageVars,
+    proof: &mut pigeons::Proof<W>,
+) -> anyhow::Result<()> {
+    let (constr, id) = constr;
+    if constr.is_tautology() {
+        return Ok(());
+    }
+    if constr.is_unsat() {
+        let empty = clause![];
+        let unsat_id = proof.reverse_unit_prop(&empty, [id.into()])?;
+        collector.add_cert_clause(empty, unsat_id)?;
+        return Ok(());
+    }
+    if constr.is_positive_assignment() {
+        for lit in constr.into_lits() {
+            let unit = clause![lit];
+            let unit_id = proof.reverse_unit_prop(&unit, [id.into()])?;
+            collector.add_cert_clause(unit, unit_id)?;
+        }
+        return Ok(());
+    }
+    if constr.is_negative_assignment() {
+        for lit in constr.into_lits() {
+            let unit = clause![!lit];
+            let unit_id = proof.reverse_unit_prop(&unit, [id.into()])?;
+            collector.add_cert_clause(unit, unit_id)?;
+        }
+        return Ok(());
+    }
+    if constr.is_clause() {
+        let clause = unreachable_err!(constr.into_clause());
+        let cl_id = proof.reverse_unit_prop(&clause, [id.into()])?;
+        collector.add_cert_clause(clause, cl_id)?;
+        return Ok(());
+    }
+    CE::encode_constr_cert((constr, id), collector, var_manager, proof)
+}