rustsat/encodings/
pb.rs

1//! # CNF Encodings for Pseudo-Boolean Constraints
2//!
3//! The module contains implementations of CNF encodings for pseudo-boolean
4//! constraints. It defines traits for (non-)incremental PB constraints and
5//! encodings implementing these traits.
6//!
7//! ## Example Usage
8//!
9//! ```
10//! # use rustsat::{
11//! #     clause,
12//! #     encodings::pb::{BoundBoth, DefIncBothBounding, Encode},
13//! #     instances::{BasicVarManager, Cnf, ManageVars},
14//! #     lit, solvers, var,
15//! #     types::RsHashMap,
16//! # };
17//! #
18//! let mut var_manager = BasicVarManager::default();
19//! var_manager.increase_next_free(var![4]);
20//!
21//! let mut lits = RsHashMap::default();
22//! lits.insert(lit![0], 4);
23//! lits.insert(lit![1], 2);
24//! lits.insert(lit![2], 2);
25//! lits.insert(lit![3], 6);
26//! let mut enc = DefIncBothBounding::from(lits);
27//! let mut encoding = Cnf::new();
28//! enc.encode_both(4..=4, &mut encoding, &mut var_manager);
29//! ```
30//!
31//! When using cardinality and pseudo-boolean encodings at the same time, it is
32//! recommended to import only the modules or rename the traits, e.g., `use
33//! card::Encode as EncodePB`.
34
35use std::{
36    cmp,
37    ops::{Bound, Range, RangeBounds},
38};
39
40use super::{card, CollectClauses, ConstraintEncodingError, EnforceError};
41use crate::{
42    clause,
43    instances::ManageVars,
44    types::{
45        constraints::{PbConstraint, PbEqConstr, PbLbConstr, PbUbConstr},
46        Clause, Lit,
47    },
48    utils::unreachable_err,
49};
50
51pub mod gte;
52pub use gte::GeneralizedTotalizer;
53
54pub mod simulators;
55/// Inverted generalized totalizer that can be used for lower bounding PB expressions
56pub type InvertedGeneralizedTotalizer = simulators::Inverted<GeneralizedTotalizer>;
57/// Double generalized totalizer that can be used for upper and lower bounding PB expressions
58pub type DoubleGeneralizedTotalizer =
59    simulators::Double<GeneralizedTotalizer, InvertedGeneralizedTotalizer>;
60
61pub mod dpw;
62pub use dpw::DynamicPolyWatchdog;
63
64pub mod adder;
65pub use adder::BinaryAdder;
66
67#[cfg(feature = "proof-logging")]
68pub mod cert;
69
70/// Trait for all pseudo-boolean encodings of form `weighted sum of lits <> rhs`
71pub trait Encode {
72    /// Get the sum of weights in the encoding
73    fn weight_sum(&self) -> usize;
74    /// Gets the next higher value possible to be achieved by the weighted sum.
75    /// Might simply return `val + 1` if no stronger value can be inferred.
76    fn next_higher(&self, val: usize) -> usize {
77        val + 1
78    }
79    /// Gets the next lower value possible to be achieved by the weighted sum.
80    /// Might simply return `val - 1` if no stronger value can be inferred.
81    fn next_lower(&self, val: usize) -> usize {
82        val - 1
83    }
84}
85
86/// Trait for pseudo-boolean encodings that allow upper bounding of the form `sum
87/// of lits <= ub`
88pub trait BoundUpper: Encode {
89    /// Lazily builds the pseudo-boolean encoding to enable upper bounds within
90    /// a given range. `var_manager` is the variable manager to use for tracking
91    /// new variables. A specific encoding might ignore the upper or lower end
92    /// of the range.
93    ///
94    /// # Errors
95    ///
96    /// If the clause collector runs out of memory.
97    fn encode_ub<Col, R>(
98        &mut self,
99        range: R,
100        collector: &mut Col,
101        var_manager: &mut dyn ManageVars,
102    ) -> Result<(), crate::OutOfMemory>
103    where
104        Col: CollectClauses,
105        R: RangeBounds<usize>;
106    /// Returns assumptions/units for enforcing an upper bound (`weighted sum of
107    /// lits <= ub`). Make sure that [`BoundUpper::encode_ub`] has been called
108    /// adequately and nothing has been called afterwards.
109    ///
110    /// # Errors
111    ///
112    /// If [`BoundUpper::encode_ub`] has not been called adequately, or `lb` is larger than the
113    /// sum of weights in the encoding.
114    fn enforce_ub(&self, ub: usize) -> Result<Vec<Lit>, EnforceError>;
115    /// Encodes an upper bound pseudo-boolean constraint to CNF
116    ///
117    /// # Errors
118    ///
119    /// If the constraint is unsatisfiable or the collector runs out of memory.
120    fn encode_ub_constr<Col>(
121        constr: PbUbConstr,
122        collector: &mut Col,
123        var_manager: &mut dyn ManageVars,
124    ) -> Result<(), ConstraintEncodingError>
125    where
126        Col: CollectClauses,
127        Self: FromIterator<(Lit, usize)> + Sized,
128    {
129        let (lits, ub) = constr.decompose();
130        if ub < 0 {
131            return Err(ConstraintEncodingError::Unsat);
132        }
133        let ub = ub.unsigned_abs();
134        let mut enc = Self::from_iter(lits);
135        enc.encode_ub(ub..=ub, collector, var_manager)?;
136        collector.extend_clauses(
137            enc.enforce_ub(ub)
138                .unwrap()
139                .into_iter()
140                .map(|unit| clause![unit]),
141        )?;
142        Ok(())
143    }
144    /// Gets the next smaller upper bound value that can be _easily_ encoded. This
145    /// is used for coarse convergence, e.g., with the [`DynamicPolyWatchdog`]
146    /// encoding.
147    fn coarse_ub(&self, ub: usize) -> usize {
148        ub
149    }
150}
151
152/// Trait for pseudo-boolean encodings that allow lower bounding of the form `sum
153/// of lits >= lb`
154pub trait BoundLower: Encode {
155    /// Lazily builds the pseudo-boolean encoding to enable lower bounds in a
156    /// given range. `var_manager` is the variable manager to use for tracking
157    /// new variables. A specific encoding might ignore the upper or lower end
158    /// of the range.
159    ///
160    /// # Errors
161    ///
162    /// If the collector runs out of memory.
163    fn encode_lb<Col, R>(
164        &mut self,
165        range: R,
166        collector: &mut Col,
167        var_manager: &mut dyn ManageVars,
168    ) -> Result<(), crate::OutOfMemory>
169    where
170        Col: CollectClauses,
171        R: RangeBounds<usize>;
172    /// Returns assumptions/units for enforcing a lower bound (`sum of lits >=
173    /// lb`). Make sure that [`BoundLower::encode_lb`] has been called
174    /// adequately and nothing has been added afterwards.
175    ///
176    /// # Errors
177    ///
178    /// If [`BoundLower::encode_lb`] has not been called adequately, or `lb` is larger than the
179    /// sum of weights in the encoding.
180    fn enforce_lb(&self, lb: usize) -> Result<Vec<Lit>, EnforceError>;
181    /// Encodes a lower bound pseudo-boolean constraint to CNF
182    ///
183    /// # Errors
184    ///
185    /// If the constraint is unsatisfiable or the collector runs out of memory.
186    fn encode_lb_constr<Col>(
187        constr: PbLbConstr,
188        collector: &mut Col,
189        var_manager: &mut dyn ManageVars,
190    ) -> Result<(), ConstraintEncodingError>
191    where
192        Col: CollectClauses,
193        Self: FromIterator<(Lit, usize)> + Sized,
194    {
195        let (lits, lb) = constr.decompose();
196        let lb = if lb < 0 {
197            return Ok(()); // tautology
198        } else {
199            lb.unsigned_abs()
200        };
201        if lb > lits.iter().fold(0, |sum, (_, w)| sum + *w) {
202            return Err(ConstraintEncodingError::Unsat);
203        }
204        let mut enc = Self::from_iter(lits);
205        enc.encode_lb(lb..=lb, collector, var_manager)?;
206        collector.extend_clauses(
207            enc.enforce_lb(lb)
208                .unwrap()
209                .into_iter()
210                .map(|unit| clause![unit]),
211        )?;
212        Ok(())
213    }
214    /// Gets the next greater lower bound value that can be _easily_ encoded. This
215    /// is used for coarse convergence.
216    fn coarse_lb(&self, lb: usize) -> usize {
217        lb
218    }
219}
220
221/// Trait for pseudo-boolean encodings that allow upper and lower bounding
222pub trait BoundBoth: BoundUpper + BoundLower {
223    /// Lazily builds the pseudo-boolean encoding to enable both bounds in a
224    /// given range. `var_manager` is the variable manager to use for tracking
225    /// new variables. A specific encoding might ignore the upper or lower end
226    /// of the range.
227    ///
228    /// # Errors
229    ///
230    /// If the collector runs out of memory.
231    fn encode_both<Col, R>(
232        &mut self,
233        range: R,
234        collector: &mut Col,
235        var_manager: &mut dyn ManageVars,
236    ) -> Result<(), crate::OutOfMemory>
237    where
238        Col: CollectClauses,
239        R: RangeBounds<usize> + Clone,
240    {
241        self.encode_ub(range.clone(), collector, var_manager)?;
242        self.encode_lb(range, collector, var_manager)?;
243        Ok(())
244    }
245    /// Returns assumptions for enforcing an equality (`sum of lits = b`) or an
246    /// error if the encoding does not support one of the two required bound
247    /// types. Make sure the adequate `encode_x` methods have been called before
248    /// this method and nothing has been added afterwards.
249    ///
250    /// # Errors
251    ///
252    /// If not adequately encoded, or `b` is larger than the sum of weights in the encoding.
253    fn enforce_eq(&self, b: usize) -> Result<Vec<Lit>, EnforceError> {
254        let mut assumps = self.enforce_ub(b)?;
255        assumps.extend(self.enforce_lb(b)?);
256        Ok(assumps)
257    }
258    /// Encodes an equality pseudo-boolean constraint to CNF
259    ///
260    /// # Errors
261    ///
262    /// If the constraint is unsatisfiable or the collector runs out of memory.
263    fn encode_eq_constr<Col>(
264        constr: PbEqConstr,
265        collector: &mut Col,
266        var_manager: &mut dyn ManageVars,
267    ) -> Result<(), ConstraintEncodingError>
268    where
269        Col: CollectClauses,
270        Self: FromIterator<(Lit, usize)> + Sized,
271    {
272        let (lits, b) = constr.decompose();
273        if b < 0 {
274            return Err(ConstraintEncodingError::Unsat);
275        }
276        let b = b.unsigned_abs();
277        if b > lits.iter().fold(0, |sum, (_, w)| sum + *w) {
278            return Err(ConstraintEncodingError::Unsat);
279        }
280        let mut enc = Self::from_iter(lits);
281        enc.encode_both(b..=b, collector, var_manager)?;
282        collector.extend_clauses(
283            enc.enforce_eq(b)
284                .unwrap()
285                .into_iter()
286                .map(|unit| clause![unit]),
287        )?;
288        Ok(())
289    }
290    /// Encodes any pseudo-boolean constraint to CNF
291    ///
292    /// # Errors
293    ///
294    /// If the constraint is unsatisfiable or the collector runs out of memory.
295    fn encode_constr<Col>(
296        constr: PbConstraint,
297        collector: &mut Col,
298        var_manager: &mut dyn ManageVars,
299    ) -> Result<(), ConstraintEncodingError>
300    where
301        Col: CollectClauses,
302        Self: FromIterator<(Lit, usize)> + Sized,
303    {
304        match constr {
305            PbConstraint::Ub(constr) => Self::encode_ub_constr(constr, collector, var_manager),
306            PbConstraint::Lb(constr) => Self::encode_lb_constr(constr, collector, var_manager),
307            PbConstraint::Eq(constr) => Self::encode_eq_constr(constr, collector, var_manager),
308        }
309    }
310}
311
312/// Trait for all pseudo-boolean encodings of form `sum of lits <> rhs`
313pub trait EncodeIncremental: Encode {
314    /// Reserves all variables this encoding might need
315    fn reserve(&mut self, var_manager: &mut dyn ManageVars);
316}
317
318/// Trait for incremental pseudo-boolean encodings that allow upper bounding of the
319/// form `sum of lits <= ub`
320pub trait BoundUpperIncremental: BoundUpper + EncodeIncremental {
321    /// Lazily builds the _change in_ pseudo-boolean encoding to enable upper
322    /// bounds from within the range. A change might be added literals or
323    /// changed bounds. `var_manager` is the variable manager to use for
324    /// tracking new variables. A specific encoding might ignore the lower or
325    /// upper end of the range.
326    ///
327    /// # Errors
328    ///
329    /// If the clause collector runs out of memory.
330    fn encode_ub_change<Col, R>(
331        &mut self,
332        range: R,
333        collector: &mut Col,
334        var_manager: &mut dyn ManageVars,
335    ) -> Result<(), crate::OutOfMemory>
336    where
337        Col: CollectClauses,
338        R: RangeBounds<usize>;
339}
340
341/// Trait for incremental pseudo-boolean encodings that allow lower bounding of the
342/// form `sum of lits >= lb`
343pub trait BoundLowerIncremental: BoundLower + EncodeIncremental {
344    /// Lazily builds the _change in_ pseudo-boolean encoding to enable lower
345    /// bounds within the range. `var_manager` is the variable manager to use
346    /// for tracking new variables. A specific encoding might ignore the lower
347    /// or upper end of the range.
348    ///
349    /// # Errors
350    ///
351    /// If the clause collector runs out of memory.
352    fn encode_lb_change<Col, R>(
353        &mut self,
354        range: R,
355        collector: &mut Col,
356        var_manager: &mut dyn ManageVars,
357    ) -> Result<(), crate::OutOfMemory>
358    where
359        Col: CollectClauses,
360        R: RangeBounds<usize>;
361}
362
363/// Trait for incremental pseudo-boolean encodings that allow upper and lower bounding
364pub trait BoundBothIncremental: BoundUpperIncremental + BoundLowerIncremental + BoundBoth {
365    /// Lazily builds the _change in_ pseudo-boolean encoding to enable both
366    /// bounds from `min_b` to `max_b`. `var_manager` is the variable manager to
367    /// use for tracking new variables. A specific encoding might ignore the
368    /// lower or upper end of the range.
369    ///
370    /// # Errors
371    ///
372    /// If the clause collector runs out of memory.
373    fn encode_both_change<Col, R>(
374        &mut self,
375        range: R,
376        collector: &mut Col,
377        var_manager: &mut dyn ManageVars,
378    ) -> Result<(), crate::OutOfMemory>
379    where
380        Col: CollectClauses,
381        R: RangeBounds<usize> + Clone,
382    {
383        self.encode_ub_change(range.clone(), collector, var_manager)?;
384        self.encode_lb_change(range, collector, var_manager)?;
385        Ok(())
386    }
387}
388
389/// The default upper bound encoding. For now this is a [`GeneralizedTotalizer`].
390pub type DefUpperBounding = GeneralizedTotalizer;
391/// The default lower bound encoding. For now this is a [`InvertedGeneralizedTotalizer`].
392pub type DefLowerBounding = InvertedGeneralizedTotalizer;
393/// The default encoding for both bounds. For now this is a [`DoubleGeneralizedTotalizer`].
394pub type DefBothBounding = DoubleGeneralizedTotalizer;
395/// The default incremental upper bound encoding. For now this is a [`GeneralizedTotalizer`].
396pub type DefIncUpperBounding = GeneralizedTotalizer;
397/// The default incremental lower bound encoding. For now this is a [`InvertedGeneralizedTotalizer`].
398pub type DefIncLowerBounding = InvertedGeneralizedTotalizer;
399/// The default incremental encoding for both bounds. For now this is a [`DoubleGeneralizedTotalizer`].
400pub type DefIncBothBounding = DoubleGeneralizedTotalizer;
401
402/// Constructs a default upper bounding pseudo-boolean encoding.
403#[must_use]
404pub fn new_default_ub() -> impl BoundUpper + Extend<(Lit, usize)> {
405    DefUpperBounding::default()
406}
407
408/// Constructs a default lower bounding pseudo-boolean encoding.
409#[must_use]
410pub fn new_default_lb() -> impl BoundLower + Extend<(Lit, usize)> {
411    DefLowerBounding::default()
412}
413
414/// Constructs a default double bounding pseudo-boolean encoding.
415#[must_use]
416pub fn new_default_both() -> impl BoundBoth + Extend<(Lit, usize)> {
417    DefBothBounding::default()
418}
419
420/// Constructs a default incremental upper bounding pseudo-boolean encoding.
421#[must_use]
422pub fn new_default_inc_ub() -> impl BoundUpperIncremental + Extend<(Lit, usize)> {
423    DefIncUpperBounding::default()
424}
425
426/// Constructs a default incremental lower bounding pseudo-boolean encoding.
427#[must_use]
428pub fn new_default_inc_lb() -> impl BoundLower + Extend<(Lit, usize)> {
429    DefIncLowerBounding::default()
430}
431
432/// Constructs a default incremental double bounding pseudo-boolean encoding.
433#[must_use]
434pub fn new_default_inc_both() -> impl BoundBoth + Extend<(Lit, usize)> {
435    DefIncBothBounding::default()
436}
437
438/// A default encoder for any pseudo-boolean constraint. This uses a
439/// [`DefBothBounding`] to encode true pseudo-boolean constraints and
440/// [`card::default_encode_cardinality_constraint`] for cardinality constraints.
441///
442/// # Errors
443///
444/// If the clause collector runs out of memory.
445pub fn default_encode_pb_constraint<Col: CollectClauses>(
446    constr: PbConstraint,
447    collector: &mut Col,
448    var_manager: &mut dyn ManageVars,
449) -> Result<(), crate::OutOfMemory> {
450    encode_pb_constraint::<DefBothBounding, Col>(constr, collector, var_manager)
451}
452
453/// An encoder for any pseudo-boolean constraint with an encoding of choice
454///
455/// # Errors
456///
457/// If the clause collector runs out of memory.
458pub fn encode_pb_constraint<PBE: BoundBoth + FromIterator<(Lit, usize)>, Col: CollectClauses>(
459    constr: PbConstraint,
460    collector: &mut Col,
461    var_manager: &mut dyn ManageVars,
462) -> Result<(), crate::OutOfMemory> {
463    if constr.is_tautology() {
464        return Ok(());
465    }
466    if constr.is_unsat() {
467        return collector.add_clause(Clause::new());
468    }
469    if constr.is_positive_assignment() {
470        return collector
471            .extend_clauses(constr.into_lits().into_iter().map(|(lit, _)| clause![lit]));
472    }
473    if constr.is_negative_assignment() {
474        return collector
475            .extend_clauses(constr.into_lits().into_iter().map(|(lit, _)| clause![!lit]));
476    }
477    if constr.is_clause() {
478        return collector.add_clause(unreachable_err!(constr.into_clause()));
479    }
480    if constr.is_card() {
481        let card = unreachable_err!(constr.into_card_constr());
482        return card::default_encode_cardinality_constraint(card, collector, var_manager);
483    }
484    match PBE::encode_constr(constr, collector, var_manager) {
485        Ok(()) => Ok(()),
486        Err(ConstraintEncodingError::OutOfMemory(err)) => Err(err),
487        Err(ConstraintEncodingError::Unsat) => unreachable!(),
488    }
489}
490
491fn prepare_ub_range<Enc: Encode, R: RangeBounds<usize>>(enc: &Enc, range: R) -> Range<usize> {
492    (match range.start_bound() {
493        Bound::Included(b) => *b,
494        Bound::Excluded(b) => b + 1,
495        Bound::Unbounded => 0,
496    })..match range.end_bound() {
497        Bound::Included(b) => cmp::min(b + 1, enc.weight_sum()),
498        Bound::Excluded(b) => cmp::min(*b, enc.weight_sum()),
499        Bound::Unbounded => enc.weight_sum(),
500    }
501}
502
503fn prepare_lb_range<Enc: Encode, R: RangeBounds<usize>>(enc: &Enc, range: R) -> Range<usize> {
504    (match range.start_bound() {
505        Bound::Included(b) => cmp::max(*b, 1),
506        Bound::Excluded(b) => cmp::max(b + 1, 1),
507        Bound::Unbounded => 1,
508    })..match range.end_bound() {
509        Bound::Included(b) => cmp::min(b + 1, enc.weight_sum() + 1),
510        Bound::Excluded(b) => cmp::min(*b, enc.weight_sum() + 1),
511        Bound::Unbounded => enc.weight_sum() + 1,
512    }
513}
514
515fn prepare_both_range<Enc: Encode, R: RangeBounds<usize>>(enc: &Enc, range: R) -> Range<usize> {
516    (match range.start_bound() {
517        Bound::Included(b) => *b,
518        Bound::Excluded(b) => b + 1,
519        Bound::Unbounded => 1,
520    })..match range.end_bound() {
521        Bound::Included(b) => cmp::min(b + 1, enc.weight_sum() + 1),
522        Bound::Excluded(b) => cmp::min(*b, enc.weight_sum() + 1),
523        Bound::Unbounded => enc.weight_sum() + 1,
524    }
525}
rustsat/encodings/pb.rs

rustsat/encodings/
pb.rs
