From a3a0526a61333ad750e6b9909d01b94ced0bc469 Mon Sep 17 00:00:00 2001 From: Christoph Jabs Date: Tue, 4 Mar 2025 14:25:10 +0200 Subject: [PATCH] feat: certified card/PB constraint encodings --- data/single-card-eq.opb | 1 + data/single-ub.opb | 1 + src/encodings/card/cert.rs | 219 ++++++++++++++++- src/encodings/card/dbtotalizer.rs | 151 ++++++++++++ src/encodings/card/simulators.rs | 266 ++++++++++++++++++++ src/encodings/pb/cert.rs | 254 ++++++++++++++++++- src/encodings/pb/dbgte.rs | 141 +++++++++++ src/encodings/pb/simulators.rs | 392 ++++++++++++++++++++++++++++++ src/encodings/totdb/cert.rs | 23 ++ 9 files changed, 1434 insertions(+), 14 deletions(-) create mode 100644 data/single-card-eq.opb create mode 100644 data/single-ub.opb diff --git a/data/single-card-eq.opb b/data/single-card-eq.opb new file mode 100644 index 00000000..61d48641 --- /dev/null +++ b/data/single-card-eq.opb @@ -0,0 +1 @@ +1 x1 1 x2 1 x3 1 x4 = 2 diff --git a/data/single-ub.opb b/data/single-ub.opb new file mode 100644 index 00000000..f33cb834 --- /dev/null +++ b/data/single-ub.opb @@ -0,0 +1 @@ +-3 x1 -2 x2 +4 x3 -7 x4 >= -2 ; diff --git a/src/encodings/card/cert.rs b/src/encodings/card/cert.rs index 8990b1ef..a09ce988 100644 --- a/src/encodings/card/cert.rs +++ b/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, 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( + constr: (CardUbConstr, AbsConstraintId), + collector: &mut Col, + var_manager: &mut dyn ManageVars, + proof: &mut pigeons::Proof, + ) -> anyhow::Result<()> + where + Col: CollectCertClauses, + W: std::io::Write, + Self: FromIterator + 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, 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( + constr: (CardLbConstr, AbsConstraintId), + collector: &mut Col, + var_manager: &mut dyn ManageVars, + proof: &mut pigeons::Proof, + ) -> anyhow::Result<()> + where + Col: CollectCertClauses, + W: std::io::Write, + Self: FromIterator + 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( + constr: (CardEqConstr, AbsConstraintId), + collector: &mut Col, + var_manager: &mut dyn ManageVars, + proof: &mut pigeons::Proof, + ) -> anyhow::Result<()> + where + Col: CollectCertClauses, + W: std::io::Write, + Self: FromIterator + 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( + constr: (CardConstraint, AbsConstraintId), + collector: &mut Col, + var_manager: &mut dyn ManageVars, + proof: &mut pigeons::Proof, + ) -> anyhow::Result<()> + where + Col: CollectCertClauses, + W: std::io::Write, + Self: FromIterator + 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 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( + constr: (CardConstraint, AbsConstraintId), + collector: &mut Col, + var_manager: &mut dyn ManageVars, + proof: &mut pigeons::Proof, +) -> anyhow::Result<()> { + encode_cardinality_constraint::(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, + Col: CollectCertClauses, + W: std::io::Write, +>( + constr: (CardConstraint, AbsConstraintId), + collector: &mut Col, + var_manager: &mut dyn ManageVars, + proof: &mut pigeons::Proof, +) -> 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) +} diff --git a/src/encodings/card/dbtotalizer.rs b/src/encodings/card/dbtotalizer.rs index 765449eb..199be99a 100644 --- a/src/encodings/card/dbtotalizer.rs +++ b/src/encodings/card/dbtotalizer.rs @@ -371,6 +371,42 @@ impl super::cert::BoundUpper for DbTotalizer { self.db.reset_encoded(totdb::Semantics::If); self.encode_ub_change_cert(range, collector, var_manager, proof) } + + fn encode_ub_constr_cert( + constr: ( + crate::types::constraints::CardUbConstr, + pigeons::AbsConstraintId, + ), + collector: &mut Col, + var_manager: &mut dyn ManageVars, + proof: &mut pigeons::Proof, + ) -> anyhow::Result<()> + where + Col: crate::encodings::CollectCertClauses, + W: std::io::Write, + Self: FromIterator + Sized, + { + use pigeons::OperationSequence; + + use crate::types::Var; + + // TODO: properly take care of constraints where no structure is built + + let (constr, id) = constr; + let (lits, ub) = constr.decompose(); + let mut enc = Self::from_iter(lits); + enc.encode_ub_cert(ub..=ub, collector, var_manager, proof)?; + let (olit, sem_defs) = enc.output_proof_details(ub + 1)?; + let unit_id = proof.operations( + &((OperationSequence::::from(id) + sem_defs.only_if_def.unwrap()) / (ub + 1)), + )?; + let unit_cl = crate::clause![!olit]; + #[cfg(feature = "verbose-proofs")] + proof.equals(&unit_cl, Some(unit_id.into()))?; + collector.add_cert_clause(unit_cl, unit_id)?; + enc.db.delete_semantics(proof)?; + Ok(()) + } } #[cfg(feature = "proof-logging")] @@ -434,6 +470,42 @@ impl super::cert::BoundLower for DbTotalizer { self.db.reset_encoded(totdb::Semantics::OnlyIf); self.encode_lb_change_cert(range, collector, var_manager, proof) } + + fn encode_lb_constr_cert( + constr: ( + crate::types::constraints::CardLBConstr, + pigeons::AbsConstraintId, + ), + collector: &mut Col, + var_manager: &mut dyn ManageVars, + proof: &mut pigeons::Proof, + ) -> anyhow::Result<()> + where + Col: crate::encodings::CollectCertClauses, + W: std::io::Write, + Self: FromIterator + Sized, + { + use pigeons::OperationSequence; + + use crate::types::Var; + + // TODO: properly take care of constraints where no structure is built + + let (constr, id) = constr; + let (lits, ub) = constr.decompose(); + let mut enc = Self::from_iter(lits); + enc.encode_lb_cert(ub..=ub, collector, var_manager, proof)?; + let (olit, sem_defs) = enc.output_proof_details(ub)?; + let unit_id = proof.operations( + &((OperationSequence::::from(id) + sem_defs.if_def.unwrap()) / (ub + 1)), + )?; + let unit_cl = crate::clause![olit]; + #[cfg(feature = "verbose-proofs")] + proof.equals(&unit_cl, Some(unit_id.into()))?; + collector.add_cert_clause(unit_cl, unit_id)?; + enc.db.delete_semantics(proof)?; + Ok(()) + } } #[cfg(feature = "proof-logging")] @@ -787,4 +859,83 @@ mod tests { tot.encode_ub(0..3, &mut cnf, &mut var_manager).unwrap(); assert_eq!(var_manager.n_used(), 12); } + + #[cfg(feature = "proof-logging")] + mod proofs { + use std::{ + fs::File, + io::{BufRead, BufReader}, + path::Path, + process::Command, + }; + + use crate::{ + encodings::card::cert::BoundBoth, + instances::{Cnf, SatInstance}, + types::{constraints::CardConstraint, Var}, + }; + + fn print_file>(path: P) { + println!(); + for line in BufReader::new(File::open(path).expect("could not open file")).lines() { + println!("{}", line.unwrap()); + } + println!(); + } + + fn verify_proof, P2: AsRef>(instance: P1, proof: P2) { + if let Ok(veripb) = std::env::var("VERIPB_CHECKER") { + println!("start checking proof"); + let out = Command::new(veripb) + .arg(instance.as_ref()) + .arg(proof.as_ref()) + .output() + .expect("failed to run veripb"); + print_file(proof); + if out.status.success() { + return; + } + panic!("verification failed: {out:?}") + } else { + println!("`$VERIPB_CHECKER` not set, omitting proof checking"); + } + } + + fn new_proof( + num_constraints: usize, + optimization: bool, + ) -> pigeons::Proof { + let file = + tempfile::NamedTempFile::new().expect("failed to create temporary proof file"); + pigeons::Proof::new(file, num_constraints, optimization).expect("failed to start proof") + } + + #[test] + fn constraint() { + let manifest = std::env::var("CARGO_MANIFEST_DIR").unwrap(); + let inst_path = format!("{manifest}/data/single-card-eq.opb"); + let constr: SatInstance = + SatInstance::from_opb_path(&inst_path, Default::default()).unwrap(); + let (constr, mut vm) = constr.into_pbs(); + assert_eq!(constr.len(), 1); + let constr = constr.into_iter().next().unwrap(); + let constr = constr.into_card_constr().unwrap(); + let CardConstraint::Eq(constr) = constr else { + panic!() + }; + let mut cnf = Cnf::new(); + let mut proof = new_proof(2, false); + super::DbTotalizer::encode_eq_constr_cert( + (constr, pigeons::AbsConstraintId::new(1)), + &mut cnf, + &mut vm, + &mut proof, + ) + .unwrap(); + let proof_file = proof + .conclude::(pigeons::OutputGuarantee::None, &pigeons::Conclusion::None) + .unwrap(); + verify_proof(&inst_path, proof_file.path()); + } + } } diff --git a/src/encodings/card/simulators.rs b/src/encodings/card/simulators.rs index fea7cf6c..229de11d 100644 --- a/src/encodings/card/simulators.rs +++ b/src/encodings/card/simulators.rs @@ -148,6 +148,50 @@ where } } +#[cfg(feature = "proof-logging")] +impl super::cert::BoundUpper for Inverted +where + CE: super::cert::BoundLower + FromIterator, +{ + fn encode_ub_cert( + &mut self, + range: R, + collector: &mut Col, + var_manager: &mut dyn ManageVars, + proof: &mut pigeons::Proof, + ) -> anyhow::Result<()> + where + Col: crate::encodings::CollectCertClauses, + R: RangeBounds, + W: std::io::Write, + { + self.card_enc.encode_lb_cert( + self.convert_encoding_range(super::prepare_ub_range(self, range)), + collector, + var_manager, + proof, + ) + } + + fn encode_ub_constr_cert( + constr: ( + crate::types::constraints::CardUbConstr, + pigeons::AbsConstraintId, + ), + collector: &mut Col, + var_manager: &mut dyn ManageVars, + proof: &mut pigeons::Proof, + ) -> anyhow::Result<()> + where + Col: crate::encodings::CollectCertClauses, + W: std::io::Write, + Self: FromIterator + Sized, + { + let constr = (constr.0.invert(), constr.1); + CE::encode_lb_constr_cert(constr, collector, var_manager, proof) + } +} + impl BoundLower for Inverted where CE: BoundUpper, @@ -179,6 +223,50 @@ where } } +#[cfg(feature = "proof-logging")] +impl super::cert::BoundLower for Inverted +where + CE: super::cert::BoundUpper + FromIterator, +{ + fn encode_lb_cert( + &mut self, + range: R, + collector: &mut Col, + var_manager: &mut dyn ManageVars, + proof: &mut pigeons::Proof, + ) -> anyhow::Result<()> + where + Col: crate::encodings::CollectCertClauses, + R: RangeBounds, + W: std::io::Write, + { + self.card_enc.encode_ub_cert( + self.convert_encoding_range(super::prepare_ub_range(self, range)), + collector, + var_manager, + proof, + ) + } + + fn encode_lb_constr_cert( + constr: ( + crate::types::constraints::CardLBConstr, + pigeons::AbsConstraintId, + ), + collector: &mut Col, + var_manager: &mut dyn ManageVars, + proof: &mut pigeons::Proof, + ) -> anyhow::Result<()> + where + Col: crate::encodings::CollectCertClauses, + W: std::io::Write, + Self: FromIterator + Sized, + { + let constr = (constr.0.invert(), constr.1); + CE::encode_ub_constr_cert(constr, collector, var_manager, proof) + } +} + impl BoundUpperIncremental for Inverted where CE: BoundLowerIncremental, @@ -201,6 +289,32 @@ where } } +#[cfg(feature = "proof-logging")] +impl super::cert::BoundUpperIncremental for Inverted +where + CE: super::cert::BoundLowerIncremental + FromIterator, +{ + fn encode_ub_change_cert( + &mut self, + range: R, + collector: &mut Col, + var_manager: &mut dyn ManageVars, + proof: &mut pigeons::Proof, + ) -> anyhow::Result<()> + where + Col: crate::encodings::CollectCertClauses, + R: RangeBounds, + W: std::io::Write, + { + self.card_enc.encode_lb_change_cert( + self.convert_encoding_range(super::prepare_ub_range(self, range)), + collector, + var_manager, + proof, + ) + } +} + impl BoundLowerIncremental for Inverted where CE: BoundUpperIncremental, @@ -223,6 +337,32 @@ where } } +#[cfg(feature = "proof-logging")] +impl super::cert::BoundLowerIncremental for Inverted +where + CE: super::cert::BoundUpperIncremental + FromIterator, +{ + fn encode_lb_change_cert( + &mut self, + range: R, + collector: &mut Col, + var_manager: &mut dyn ManageVars, + proof: &mut pigeons::Proof, + ) -> anyhow::Result<()> + where + Col: crate::encodings::CollectCertClauses, + R: RangeBounds, + W: std::io::Write, + { + self.card_enc.encode_ub_change_cert( + self.convert_encoding_range(super::prepare_ub_range(self, range)), + collector, + var_manager, + proof, + ) + } +} + impl EncodeStats for Inverted where CE: Encode + EncodeStats, @@ -355,6 +495,46 @@ where } } +#[cfg(feature = "proof-logging")] +impl super::cert::BoundUpper for Double +where + UBE: super::cert::BoundUpper + FromIterator, + LBE: super::cert::BoundLower + FromIterator, +{ + fn encode_ub_cert( + &mut self, + range: R, + collector: &mut Col, + var_manager: &mut dyn ManageVars, + proof: &mut pigeons::Proof, + ) -> anyhow::Result<()> + where + Col: crate::encodings::CollectCertClauses, + R: RangeBounds, + W: std::io::Write, + { + self.ub_enc + .encode_ub_cert(range, collector, var_manager, proof) + } + + fn encode_ub_constr_cert( + constr: ( + crate::types::constraints::CardUbConstr, + pigeons::AbsConstraintId, + ), + collector: &mut Col, + var_manager: &mut dyn ManageVars, + proof: &mut pigeons::Proof, + ) -> anyhow::Result<()> + where + Col: crate::encodings::CollectCertClauses, + W: std::io::Write, + Self: FromIterator + Sized, + { + UBE::encode_ub_constr_cert(constr, collector, var_manager, proof) + } +} + impl BoundLower for Double where UBE: BoundUpper, @@ -378,6 +558,46 @@ where } } +#[cfg(feature = "proof-logging")] +impl super::cert::BoundLower for Double +where + UBE: super::cert::BoundUpper + FromIterator, + LBE: super::cert::BoundLower + FromIterator, +{ + fn encode_lb_cert( + &mut self, + range: R, + collector: &mut Col, + var_manager: &mut dyn ManageVars, + proof: &mut pigeons::Proof, + ) -> anyhow::Result<()> + where + Col: crate::encodings::CollectCertClauses, + R: RangeBounds, + W: std::io::Write, + { + self.lb_enc + .encode_lb_cert(range, collector, var_manager, proof) + } + + fn encode_lb_constr_cert( + constr: ( + crate::types::constraints::CardLBConstr, + pigeons::AbsConstraintId, + ), + collector: &mut Col, + var_manager: &mut dyn ManageVars, + proof: &mut pigeons::Proof, + ) -> anyhow::Result<()> + where + Col: crate::encodings::CollectCertClauses, + W: std::io::Write, + Self: FromIterator + Sized, + { + LBE::encode_lb_constr_cert(constr, collector, var_manager, proof) + } +} + impl BoundUpperIncremental for Double where UBE: BoundUpperIncremental, @@ -397,6 +617,29 @@ where } } +#[cfg(feature = "proof-logging")] +impl super::cert::BoundUpperIncremental for Double +where + UBE: super::cert::BoundUpperIncremental + BoundUpperIncremental + FromIterator, + LBE: super::cert::BoundLowerIncremental + BoundLowerIncremental + FromIterator, +{ + fn encode_ub_change_cert( + &mut self, + range: R, + collector: &mut Col, + var_manager: &mut dyn ManageVars, + proof: &mut pigeons::Proof, + ) -> anyhow::Result<()> + where + Col: crate::encodings::CollectCertClauses, + R: RangeBounds, + W: std::io::Write, + { + self.ub_enc + .encode_ub_change_cert(range, collector, var_manager, proof) + } +} + impl BoundLowerIncremental for Double where UBE: BoundUpperIncremental, @@ -416,6 +659,29 @@ where } } +#[cfg(feature = "proof-logging")] +impl super::cert::BoundLowerIncremental for Double +where + UBE: super::cert::BoundUpperIncremental + BoundUpperIncremental + FromIterator, + LBE: super::cert::BoundLowerIncremental + BoundLowerIncremental + FromIterator, +{ + fn encode_lb_change_cert( + &mut self, + range: R, + collector: &mut Col, + var_manager: &mut dyn ManageVars, + proof: &mut pigeons::Proof, + ) -> anyhow::Result<()> + where + Col: crate::encodings::CollectCertClauses, + R: RangeBounds, + W: std::io::Write, + { + self.lb_enc + .encode_lb_change_cert(range, collector, var_manager, proof) + } +} + impl EncodeStats for Double where UBE: EncodeStats + BoundUpper, diff --git a/src/encodings/pb/cert.rs b/src/encodings/pb/cert.rs index cd55f6ce..d36240b0 100644 --- a/src/encodings/pb/cert.rs +++ b/src/encodings/pb/cert.rs @@ -2,12 +2,25 @@ use std::ops::RangeBounds; -use crate::{encodings::CollectCertClauses, instances::ManageVars}; +use pigeons::AbsConstraintId; -/// Trait for certified cardinality encodings that allow upper bounding of the form `sum of lits <= +use crate::{ + clause, + encodings::{card, CollectCertClauses}, + instances::ManageVars, + types::{ + constraints::{PbConstraint, PbEqConstr, PbLbConstr, PbUbConstr}, + Lit, + }, + utils::unreachable_err, +}; + +use super::{simulators, DbGte}; + +/// Trait for certified PB encodings that allow upper bounding of the form `sum of lits <= /// ub` pub trait BoundUpper: super::Encode + super::BoundUpper { - /// Lazily builds the certified cardinality encoding to enable upper bounds in a given range. + /// Lazily builds the certified PB encoding to enable upper bounds in a given range. /// `var_manager` is the variable manager to use for tracking new variables. A specific /// encoding might ignore the lower or upper end of the range. The derivation of the encoding /// is written to the given `proof`. @@ -27,12 +40,29 @@ pub trait BoundUpper: super::Encode + super::BoundUpper { Col: CollectCertClauses, R: RangeBounds, W: std::io::Write; + + /// Encodes an upper bound pseudo-boolean 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( + constr: (PbUbConstr, AbsConstraintId), + collector: &mut Col, + var_manager: &mut dyn ManageVars, + proof: &mut pigeons::Proof, + ) -> anyhow::Result<()> + where + Col: CollectCertClauses, + W: std::io::Write, + Self: FromIterator<(Lit, usize)> + Sized; } -/// Trait for certified cardinality encodings that allow lower bounding of the form `sum of lits >= +/// Trait for certified PB encodings that allow lower bounding of the form `sum of lits >= /// lb` pub trait BoundLower: super::Encode + super::BoundLower { - /// Lazily builds the certified cardinality encoding to enable lower bounds in a given range. + /// Lazily builds the certified PB encoding to enable lower bounds in a given range. /// `var_manager` is the variable manager to use for tracking new variables. A specific /// encoding might ignore the lower or upper end of the range. The derivation of the encoding /// is written to the given `proof`. @@ -52,11 +82,28 @@ pub trait BoundLower: super::Encode + super::BoundLower { Col: CollectCertClauses, R: RangeBounds, W: std::io::Write; + + /// Encodes a lower bound pseudo-boolean 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( + constr: (PbLbConstr, AbsConstraintId), + collector: &mut Col, + var_manager: &mut dyn ManageVars, + proof: &mut pigeons::Proof, + ) -> anyhow::Result<()> + where + Col: CollectCertClauses, + W: std::io::Write, + Self: FromIterator<(Lit, usize)> + Sized; } -/// Trait for certified cardinality encodings that allow upper and lower bounding +/// Trait for certified PB encodings that allow upper and lower bounding pub trait BoundBoth: BoundUpper + BoundLower { - /// Lazily builds the certified cardinality encoding to enable both bounds in a given range. + /// Lazily builds the certified PB encoding to enable both bounds in a given range. /// `var_manager` is the variable manager to use for tracking new variables. A specific /// encoding might ignore the lower or upper end of the range. The derivation of the encoding /// is written to the given `proof`. @@ -81,16 +128,72 @@ pub trait BoundBoth: BoundUpper + BoundLower { self.encode_lb_cert(range, collector, var_manager, proof)?; Ok(()) } + + /// Encodes an equality pseudo-boolean 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( + constr: (PbEqConstr, AbsConstraintId), + collector: &mut Col, + var_manager: &mut dyn ManageVars, + proof: &mut pigeons::Proof, + ) -> anyhow::Result<()> + where + Col: CollectCertClauses, + W: std::io::Write, + Self: FromIterator<(Lit, usize)> + 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 pseudo-boolean 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( + constr: (PbConstraint, AbsConstraintId), + collector: &mut Col, + var_manager: &mut dyn ManageVars, + proof: &mut pigeons::Proof, + ) -> anyhow::Result<()> + where + Col: CollectCertClauses, + W: std::io::Write, + Self: FromIterator<(Lit, usize)> + Sized, + { + let (constr, id) = constr; + match constr { + PbConstraint::Ub(constr) => { + Self::encode_ub_constr_cert((constr, id), collector, var_manager, proof) + } + PbConstraint::Lb(constr) => { + Self::encode_lb_constr_cert((constr, id), collector, var_manager, proof) + } + PbConstraint::Eq(constr) => { + Self::encode_eq_constr_cert((constr, id), collector, var_manager, proof) + } + } + } } /// Default implementation of [`BoundBoth`] for every encoding that does upper /// and lower bounding impl BoundBoth for CE where CE: BoundUpper + BoundLower {} -/// Trait for incremental certified cardinality encodings that allow upper bounding of the form +/// Trait for incremental certified PB encodings that allow upper bounding of the form /// `sum of lits <= ub` pub trait BoundUpperIncremental: BoundUpper + super::EncodeIncremental { - /// Lazily builds the _change in_ the certified cardinality encoding to enable upper bounds in + /// Lazily builds the _change in_ the certified PB encoding to enable upper bounds in /// a given range. A change might be added literals or changed bounds. `var_manager` is the /// variable manager to use for tracking new variables. A specific encoding might ignore the /// lower or upper end of the range. The derivation of the encoding is written to the given @@ -113,10 +216,10 @@ pub trait BoundUpperIncremental: BoundUpper + super::EncodeIncremental { W: std::io::Write; } -/// Trait for incremental certified cardinality encodings that allow lower bounding of the form +/// Trait for incremental certified PB encodings that allow lower bounding of the form /// `sum of lits >= lb` pub trait BoundLowerIncremental: BoundLower + super::EncodeIncremental { - /// Lazily builds the _change in_ the certified cardinality encoding to enable upper bounds in + /// Lazily builds the _change in_ the certified PB encoding to enable upper bounds in /// a given range. A change might be added literals or changed bounds. `var_manager` is the /// variable manager to use for tracking new variables. A specific encoding might ignore the /// lower or upper end of the range. The derivation of the encoding is written to the given @@ -139,9 +242,9 @@ pub trait BoundLowerIncremental: BoundLower + super::EncodeIncremental { W: std::io::Write; } -/// Trait for incremental cardinality encodings that allow upper and lower bounding +/// Trait for incremental PB encodings that allow upper and lower bounding pub trait BoundBothIncremental: BoundUpperIncremental + BoundLowerIncremental { - /// Lazily builds the _change in_ the certified cardinality encoding to enable both bounds in a + /// Lazily builds the _change in_ the certified PB encoding to enable both bounds in a /// given range. `var_manager` is the variable manager to use for tracking new variables. A /// specific encoding might ignore the lower or upper end of the range. The derivation of the /// encoding is written to the given `proof`. @@ -171,3 +274,128 @@ pub trait BoundBothIncremental: BoundUpperIncremental + BoundLowerIncremental { /// Default implementation of [`BoundBothIncremental`] for every encoding that /// does incremental upper and lower bounding impl BoundBothIncremental for CE where CE: BoundUpperIncremental + BoundLowerIncremental {} + +/// The default upper bound encoding. For now this is a [`DbGte`]. +pub type DefUpperBounding = DbGte; +/// The default lower bound encoding. For now this is an inverted [`DbGte`]. +pub type DefLowerBounding = simulators::Inverted; +/// The default encoding for both bounds. For now this is a doubled [`DbGte`]. +pub type DefBothBounding = simulators::Double>; +/// The default incremental upper bound encoding. For now this is a [`DbGte`]. +pub type DefIncUpperBounding = DbGte; +/// The default incremental lower bound encoding. For now this is an inverted [`DbGte`]. +pub type DefIncLowerBounding = simulators::Inverted; +/// The default incremental encoding for both bounds. For now this is a doubled [`DbGte`]. +pub type DefIncBothBounding = simulators::Double>; + +/// Constructs a default upper bounding pseudo-boolean encoding. +#[must_use] +pub fn new_default_ub() -> impl BoundUpper + Extend<(Lit, usize)> { + DefUpperBounding::default() +} + +/// Constructs a default lower bounding pseudo-boolean encoding. +#[must_use] +pub fn new_default_lb() -> impl BoundLower + Extend<(Lit, usize)> { + DefLowerBounding::default() +} + +/// Constructs a default double bounding pseudo-boolean encoding. +#[must_use] +pub fn new_default_both() -> impl BoundBoth + Extend<(Lit, usize)> { + DefBothBounding::default() +} + +/// Constructs a default incremental upper bounding pseudo-boolean encoding. +#[must_use] +pub fn new_default_inc_ub() -> impl BoundUpperIncremental + Extend<(Lit, usize)> { + DefIncUpperBounding::default() +} + +/// Constructs a default incremental lower bounding pseudo-boolean encoding. +#[must_use] +pub fn new_default_inc_lb() -> impl BoundLower + Extend<(Lit, usize)> { + DefIncLowerBounding::default() +} + +/// Constructs a default incremental double bounding pseudo-boolean encoding. +#[must_use] +pub fn new_default_inc_both() -> impl BoundBoth + Extend<(Lit, usize)> { + DefIncBothBounding::default() +} + +/// A default encoder for any pseudo-boolean constraint. This uses a +/// [`DefBothBounding`] to encode true pseudo-boolean constraints and +/// [`card::cert::default_encode_cardinality_constraint`] for cardinality constraints. +/// +/// # Errors +/// +/// - If the clause collector runs out of memory, returns [`crate::OutOfMemory`]. +/// - If writing the proof fails, returns [`std::io::Error`] +pub fn default_encode_pb_constraint( + constr: (PbConstraint, AbsConstraintId), + collector: &mut Col, + var_manager: &mut dyn ManageVars, + proof: &mut pigeons::Proof, +) -> anyhow::Result<()> { + encode_pb_constraint::(constr, collector, var_manager, proof) +} + +/// An encoder for any pseudo-boolean constraint with an encoding of choice +/// +/// # Errors +/// +/// If the clause collector runs out of memory, returns [`crate::OutOfMemory`]. +pub fn encode_pb_constraint< + PBE: BoundBoth + FromIterator<(Lit, usize)>, + Col: CollectCertClauses, + W: std::io::Write, +>( + constr: (PbConstraint, AbsConstraintId), + collector: &mut Col, + var_manager: &mut dyn ManageVars, + proof: &mut pigeons::Proof, +) -> 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(()); + } + if constr.is_card() { + let card = unreachable_err!(constr.into_card_constr()); + return card::cert::default_encode_cardinality_constraint( + (card, id), + collector, + var_manager, + proof, + ); + } + PBE::encode_constr_cert((constr, id), collector, var_manager, proof) +} diff --git a/src/encodings/pb/dbgte.rs b/src/encodings/pb/dbgte.rs index 567578a7..2f7d7210 100644 --- a/src/encodings/pb/dbgte.rs +++ b/src/encodings/pb/dbgte.rs @@ -380,6 +380,69 @@ impl super::cert::BoundUpper for DbGte { self.db.reset_encoded(totdb::Semantics::If); self.encode_ub_change_cert(range, collector, var_manager, proof) } + + fn encode_ub_constr_cert( + constr: ( + crate::types::constraints::PbUbConstr, + pigeons::AbsConstraintId, + ), + collector: &mut Col, + var_manager: &mut dyn ManageVars, + proof: &mut pigeons::Proof, + ) -> anyhow::Result<()> + where + Col: crate::encodings::CollectCertClauses, + W: std::io::Write, + Self: FromIterator<(Lit, usize)> + Sized, + { + use pigeons::{OperationSequence, VarLike}; + + use crate::types::Var; + + // TODO: properly take care of constraints where no structure is built + + let (constr, mut id) = constr; + let (lits, ub) = constr.decompose(); + anyhow::ensure!(ub >= 0, Error::Unsat); + let ub = ub.unsigned_abs(); + let mut enc = Self::from_iter(lits); + enc.encode_ub_cert(ub..=ub, collector, var_manager, proof)?; + let mut val = enc.next_higher(ub); + for unit in enc + .enforce_ub(ub) + .expect("should have caught special case before here") + { + let (olit, sem_defs) = enc.output_proof_details(val)?; + let unit_cl = crate::clause![unit]; + let unit_id = if unit.var() < olit.var() { + // input literal with weight larger than bound + let weight = *enc.lit_buffer.get(&!unit).unwrap(); + let unit_id = proof.reverse_unit_prop(&unit_cl, [id.into()])?; + // simplify main constraint + #[cfg(feature = "verbose-proofs")] + proof.comment(&"rewritten main constraint")?; + id = proof.operations( + &(OperationSequence::::from(unit.var().axiom(!unit.is_neg())) * weight + + id), + )?; + unit_id + } else { + // output literal + // NOTE: by the time we're here, all buffered literals have been removed from `id` + debug_assert_eq!(!unit, olit); + let unit_id = proof.operations( + &((OperationSequence::::from(id) + sem_defs.only_if_def.unwrap()) / val), + )?; + #[cfg(feature = "verbose-proofs")] + proof.equals(&unit_cl, Some(unit_id.into()))?; + val = enc.next_higher(val); + unit_id + }; + collector.add_cert_clause(unit_cl, unit_id)?; + } + enc.db.delete_semantics(proof)?; + Ok(()) + } } #[cfg(feature = "proof-logging")] @@ -910,4 +973,82 @@ mod tests { gte.encode_ub(0..3, &mut cnf, &mut var_manager).unwrap(); assert_eq!(var_manager.n_used(), 24); } + + #[cfg(feature = "proof-logging")] + mod proofs { + use std::{ + fs::File, + io::{BufRead, BufReader}, + path::Path, + process::Command, + }; + + use crate::{ + encodings::pb::cert::BoundUpper, + instances::{Cnf, SatInstance}, + types::{constraints::PbConstraint, Var}, + }; + + fn print_file>(path: P) { + println!(); + for line in BufReader::new(File::open(path).expect("could not open file")).lines() { + println!("{}", line.unwrap()); + } + println!(); + } + + fn verify_proof, P2: AsRef>(instance: P1, proof: P2) { + if let Ok(veripb) = std::env::var("VERIPB_CHECKER") { + println!("start checking proof"); + let out = Command::new(veripb) + .arg(instance.as_ref()) + .arg(proof.as_ref()) + .output() + .expect("failed to run veripb"); + print_file(proof); + if out.status.success() { + return; + } + panic!("verification failed: {out:?}") + } else { + println!("`$VERIPB_CHECKER` not set, omitting proof checking"); + } + } + + fn new_proof( + num_constraints: usize, + optimization: bool, + ) -> pigeons::Proof { + let file = + tempfile::NamedTempFile::new().expect("failed to create temporary proof file"); + pigeons::Proof::new(file, num_constraints, optimization).expect("failed to start proof") + } + + #[test] + fn constraint() { + let manifest = std::env::var("CARGO_MANIFEST_DIR").unwrap(); + let inst_path = format!("{manifest}/data/single-ub.opb"); + let constr: SatInstance = + SatInstance::from_opb_path(&inst_path, Default::default()).unwrap(); + let (constr, mut vm) = constr.into_pbs(); + assert_eq!(constr.len(), 1); + let Some(PbConstraint::Lb(constr)) = constr.into_iter().next() else { + panic!() + }; + let constr = constr.invert(); + let mut cnf = Cnf::new(); + let mut proof = new_proof(1, false); + super::DbGte::encode_ub_constr_cert( + (constr, pigeons::AbsConstraintId::new(1)), + &mut cnf, + &mut vm, + &mut proof, + ) + .unwrap(); + let proof_file = proof + .conclude::(pigeons::OutputGuarantee::None, &pigeons::Conclusion::None) + .unwrap(); + verify_proof(&inst_path, proof_file.path()); + } + } } diff --git a/src/encodings/pb/simulators.rs b/src/encodings/pb/simulators.rs index 139d2550..5749e762 100644 --- a/src/encodings/pb/simulators.rs +++ b/src/encodings/pb/simulators.rs @@ -159,6 +159,50 @@ where } } +#[cfg(feature = "proof-logging")] +impl super::cert::BoundUpper for Inverted +where + PBE: super::cert::BoundLower + FromIterator<(Lit, usize)>, +{ + fn encode_ub_cert( + &mut self, + range: R, + collector: &mut Col, + var_manager: &mut dyn ManageVars, + proof: &mut pigeons::Proof, + ) -> anyhow::Result<()> + where + Col: crate::encodings::CollectCertClauses, + R: RangeBounds, + W: std::io::Write, + { + self.pb_enc.encode_lb_cert( + self.convert_encoding_range(super::prepare_ub_range(self, range)), + collector, + var_manager, + proof, + ) + } + + fn encode_ub_constr_cert( + constr: ( + crate::types::constraints::PbUbConstr, + pigeons::AbsConstraintId, + ), + collector: &mut Col, + var_manager: &mut dyn ManageVars, + proof: &mut pigeons::Proof, + ) -> anyhow::Result<()> + where + Col: crate::encodings::CollectCertClauses, + W: std::io::Write, + Self: FromIterator<(Lit, usize)> + Sized, + { + let constr = (constr.0.invert(), constr.1); + PBE::encode_lb_constr_cert(constr, collector, var_manager, proof) + } +} + impl BoundLower for Inverted where PBE: BoundUpper, @@ -190,6 +234,50 @@ where } } +#[cfg(feature = "proof-logging")] +impl super::cert::BoundLower for Inverted +where + PBE: super::cert::BoundUpper + FromIterator<(Lit, usize)>, +{ + fn encode_lb_cert( + &mut self, + range: R, + collector: &mut Col, + var_manager: &mut dyn ManageVars, + proof: &mut pigeons::Proof, + ) -> anyhow::Result<()> + where + Col: crate::encodings::CollectCertClauses, + R: RangeBounds, + W: std::io::Write, + { + self.pb_enc.encode_ub_cert( + self.convert_encoding_range(super::prepare_ub_range(self, range)), + collector, + var_manager, + proof, + ) + } + + fn encode_lb_constr_cert( + constr: ( + crate::types::constraints::PbLbConstr, + pigeons::AbsConstraintId, + ), + collector: &mut Col, + var_manager: &mut dyn ManageVars, + proof: &mut pigeons::Proof, + ) -> anyhow::Result<()> + where + Col: crate::encodings::CollectCertClauses, + W: std::io::Write, + Self: FromIterator<(Lit, usize)> + Sized, + { + let constr = (constr.0.invert(), constr.1); + PBE::encode_ub_constr_cert(constr, collector, var_manager, proof) + } +} + impl BoundUpperIncremental for Inverted where PBE: BoundLowerIncremental, @@ -212,6 +300,32 @@ where } } +#[cfg(feature = "proof-logging")] +impl super::cert::BoundUpperIncremental for Inverted +where + PBE: super::cert::BoundLowerIncremental + FromIterator<(Lit, usize)>, +{ + fn encode_ub_change_cert( + &mut self, + range: R, + collector: &mut Col, + var_manager: &mut dyn ManageVars, + proof: &mut pigeons::Proof, + ) -> anyhow::Result<()> + where + Col: crate::encodings::CollectCertClauses, + R: RangeBounds, + W: std::io::Write, + { + self.pb_enc.encode_lb_change_cert( + self.convert_encoding_range(super::prepare_ub_range(self, range)), + collector, + var_manager, + proof, + ) + } +} + impl BoundLowerIncremental for Inverted where PBE: BoundUpperIncremental, @@ -234,6 +348,32 @@ where } } +#[cfg(feature = "proof-logging")] +impl super::cert::BoundLowerIncremental for Inverted +where + PBE: super::cert::BoundUpperIncremental + FromIterator<(Lit, usize)>, +{ + fn encode_lb_change_cert( + &mut self, + range: R, + collector: &mut Col, + var_manager: &mut dyn ManageVars, + proof: &mut pigeons::Proof, + ) -> anyhow::Result<()> + where + Col: crate::encodings::CollectCertClauses, + R: RangeBounds, + W: std::io::Write, + { + self.pb_enc.encode_ub_change_cert( + self.convert_encoding_range(super::prepare_ub_range(self, range)), + collector, + var_manager, + proof, + ) + } +} + impl EncodeStats for Inverted where PBE: Encode + EncodeStats, @@ -377,6 +517,46 @@ where } } +#[cfg(feature = "proof-logging")] +impl super::cert::BoundUpper for Double +where + UBE: super::cert::BoundUpper + FromIterator<(Lit, usize)>, + LBE: super::cert::BoundLower + FromIterator<(Lit, usize)>, +{ + fn encode_ub_cert( + &mut self, + range: R, + collector: &mut Col, + var_manager: &mut dyn ManageVars, + proof: &mut pigeons::Proof, + ) -> anyhow::Result<()> + where + Col: crate::encodings::CollectCertClauses, + R: RangeBounds, + W: std::io::Write, + { + self.ub_enc + .encode_ub_cert(range, collector, var_manager, proof) + } + + fn encode_ub_constr_cert( + constr: ( + crate::types::constraints::PbUbConstr, + pigeons::AbsConstraintId, + ), + collector: &mut Col, + var_manager: &mut dyn ManageVars, + proof: &mut pigeons::Proof, + ) -> anyhow::Result<()> + where + Col: crate::encodings::CollectCertClauses, + W: std::io::Write, + Self: FromIterator<(Lit, usize)> + Sized, + { + UBE::encode_ub_constr_cert(constr, collector, var_manager, proof) + } +} + impl BoundLower for Double where UBE: BoundUpper, @@ -400,6 +580,46 @@ where } } +#[cfg(feature = "proof-logging")] +impl super::cert::BoundLower for Double +where + UBE: super::cert::BoundUpper + FromIterator<(Lit, usize)>, + LBE: super::cert::BoundLower + FromIterator<(Lit, usize)>, +{ + fn encode_lb_cert( + &mut self, + range: R, + collector: &mut Col, + var_manager: &mut dyn ManageVars, + proof: &mut pigeons::Proof, + ) -> anyhow::Result<()> + where + Col: crate::encodings::CollectCertClauses, + R: RangeBounds, + W: std::io::Write, + { + self.lb_enc + .encode_lb_cert(range, collector, var_manager, proof) + } + + fn encode_lb_constr_cert( + constr: ( + crate::types::constraints::PbLbConstr, + pigeons::AbsConstraintId, + ), + collector: &mut Col, + var_manager: &mut dyn ManageVars, + proof: &mut pigeons::Proof, + ) -> anyhow::Result<()> + where + Col: crate::encodings::CollectCertClauses, + W: std::io::Write, + Self: FromIterator<(Lit, usize)> + Sized, + { + LBE::encode_lb_constr_cert(constr, collector, var_manager, proof) + } +} + impl BoundUpperIncremental for Double where UBE: BoundUpperIncremental, @@ -419,6 +639,29 @@ where } } +#[cfg(feature = "proof-logging")] +impl super::cert::BoundUpperIncremental for Double +where + UBE: super::cert::BoundUpperIncremental + BoundUpperIncremental + FromIterator<(Lit, usize)>, + LBE: super::cert::BoundLowerIncremental + BoundLowerIncremental + FromIterator<(Lit, usize)>, +{ + fn encode_ub_change_cert( + &mut self, + range: R, + collector: &mut Col, + var_manager: &mut dyn ManageVars, + proof: &mut pigeons::Proof, + ) -> anyhow::Result<()> + where + Col: crate::encodings::CollectCertClauses, + R: RangeBounds, + W: std::io::Write, + { + self.ub_enc + .encode_ub_change_cert(range, collector, var_manager, proof) + } +} + impl BoundLowerIncremental for Double where UBE: BoundUpperIncremental, @@ -438,6 +681,29 @@ where } } +#[cfg(feature = "proof-logging")] +impl super::cert::BoundLowerIncremental for Double +where + UBE: super::cert::BoundUpperIncremental + BoundUpperIncremental + FromIterator<(Lit, usize)>, + LBE: super::cert::BoundLowerIncremental + BoundLowerIncremental + FromIterator<(Lit, usize)>, +{ + fn encode_lb_change_cert( + &mut self, + range: R, + collector: &mut Col, + var_manager: &mut dyn ManageVars, + proof: &mut pigeons::Proof, + ) -> anyhow::Result<()> + where + Col: crate::encodings::CollectCertClauses, + R: RangeBounds, + W: std::io::Write, + { + self.lb_enc + .encode_lb_change_cert(range, collector, var_manager, proof) + } +} + impl EncodeStats for Double where UBE: EncodeStats + BoundUpper, @@ -571,6 +837,47 @@ where } } +#[cfg(feature = "proof-logging")] +impl super::cert::BoundUpper for Card +where + CE: card::cert::BoundUpper + FromIterator, +{ + fn encode_ub_cert( + &mut self, + range: R, + collector: &mut Col, + var_manager: &mut dyn ManageVars, + proof: &mut pigeons::Proof, + ) -> anyhow::Result<()> + where + Col: crate::encodings::CollectCertClauses, + R: RangeBounds, + W: std::io::Write, + { + self.card_enc + .encode_ub_cert(range, collector, var_manager, proof) + } + + fn encode_ub_constr_cert( + constr: ( + crate::types::constraints::PbUbConstr, + pigeons::AbsConstraintId, + ), + collector: &mut Col, + var_manager: &mut dyn ManageVars, + proof: &mut pigeons::Proof, + ) -> anyhow::Result<()> + where + Col: crate::encodings::CollectCertClauses, + W: std::io::Write, + Self: FromIterator<(Lit, usize)> + Sized, + { + let (constr, id) = constr; + let constr = constr.extend_to_card_constr(); + CE::encode_ub_constr_cert((constr, id), collector, var_manager, proof) + } +} + impl BoundLower for Card where CE: card::BoundLower, @@ -593,6 +900,47 @@ where } } +#[cfg(feature = "proof-logging")] +impl super::cert::BoundLower for Card +where + CE: card::cert::BoundLower + FromIterator, +{ + fn encode_lb_cert( + &mut self, + range: R, + collector: &mut Col, + var_manager: &mut dyn ManageVars, + proof: &mut pigeons::Proof, + ) -> anyhow::Result<()> + where + Col: crate::encodings::CollectCertClauses, + R: RangeBounds, + W: std::io::Write, + { + self.card_enc + .encode_lb_cert(range, collector, var_manager, proof) + } + + fn encode_lb_constr_cert( + constr: ( + crate::types::constraints::PbLbConstr, + pigeons::AbsConstraintId, + ), + collector: &mut Col, + var_manager: &mut dyn ManageVars, + proof: &mut pigeons::Proof, + ) -> anyhow::Result<()> + where + Col: crate::encodings::CollectCertClauses, + W: std::io::Write, + Self: FromIterator<(Lit, usize)> + Sized, + { + let (constr, id) = constr; + let constr = constr.extend_to_card_constr(); + CE::encode_lb_constr_cert((constr, id), collector, var_manager, proof) + } +} + impl BoundUpperIncremental for Card where CE: card::BoundUpperIncremental, @@ -612,6 +960,28 @@ where } } +#[cfg(feature = "proof-logging")] +impl super::cert::BoundUpperIncremental for Card +where + CE: card::cert::BoundUpperIncremental + FromIterator, +{ + fn encode_ub_change_cert( + &mut self, + range: R, + collector: &mut Col, + var_manager: &mut dyn ManageVars, + proof: &mut pigeons::Proof, + ) -> anyhow::Result<()> + where + Col: crate::encodings::CollectCertClauses, + R: RangeBounds, + W: std::io::Write, + { + self.card_enc + .encode_ub_change_cert(range, collector, var_manager, proof) + } +} + impl BoundLowerIncremental for Card where CE: card::BoundLowerIncremental, @@ -631,6 +1001,28 @@ where } } +#[cfg(feature = "proof-logging")] +impl super::cert::BoundLowerIncremental for Card +where + CE: card::cert::BoundLowerIncremental + FromIterator, +{ + fn encode_lb_change_cert( + &mut self, + range: R, + collector: &mut Col, + var_manager: &mut dyn ManageVars, + proof: &mut pigeons::Proof, + ) -> anyhow::Result<()> + where + Col: crate::encodings::CollectCertClauses, + R: RangeBounds, + W: std::io::Write, + { + self.card_enc + .encode_lb_change_cert(range, collector, var_manager, proof) + } +} + fn add_unit_weight(lit: Lit) -> (Lit, usize) { (lit, 1) } diff --git a/src/encodings/totdb/cert.rs b/src/encodings/totdb/cert.rs index 4041b915..5d070400 100644 --- a/src/encodings/totdb/cert.rs +++ b/src/encodings/totdb/cert.rs @@ -374,6 +374,25 @@ impl super::Db { Ok(unreachable_none!(self.semantic_defs.get(&def_id).copied())) } + /// Deletes all semantic definitions from the proof + /// + /// # Errors + /// + /// If writing the proof fails, returns [`std::io::Error`] + pub fn delete_semantics(&mut self, proof: &mut pigeons::Proof) -> std::io::Result<()> + where + W: std::io::Write, + { + let iter = self + .semantic_defs + .iter() + .flat_map(|(_, def)| def.iter()) + .map(Into::into); + proof.delete_ids::(iter, None)?; + self.semantic_defs.clear(); + Ok(()) + } + /// Generates the encoding to define the positive output literal with value `val`, if it is not /// already defined. The derivation of the generated clauses is certified in the provided /// proof. Recurses down the tree. The returned literal is the output literal and the encoding @@ -1186,6 +1205,10 @@ impl SemDefs { SemDefTyp::OnlyIf => self.only_if_def.unwrap(), } } + + fn iter(&self) -> impl Iterator { + self.if_def.into_iter().chain(self.only_if_def) + } } /// The data needed to identify a semantic definition