rustsat/encodings/am1/
bimander.rs

1//! # Bimander At-Most-1 Encoding
2//!
3//! ## References
4//!
5//! - Van-Hau Nguyen and Son Thay Mai: _A New Method to Encode the At-Most-One Constraint into SAT,
6//!   SOICT 2015.
7
8use std::marker::PhantomData;
9
10use super::Encode;
11use crate::{
12    encodings::{atomics, CollectClauses, EncodeStats, IterInputs},
13    instances::ManageVars,
14    types::Lit,
15    utils,
16};
17
18/// Implementation of the bimander at-most-1 encoding.
19///
20/// # Generics
21///
22/// - `Sub`: the sub encoding to use for each split
23/// - `N`: the size of the splits
24///
25/// # References
26///
27/// - Van-Hau Nguyen and Son Thay Mai: _A New Method to Encode the At-Most-One Constraint into SAT,
28///   SOICT 2015.
29#[derive(Default, Debug)]
30#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
31pub struct Bimander<const N: usize = 4, Sub = super::Pairwise> {
32    /// Input literals
33    in_lits: Vec<Lit>,
34    /// The number of clauses in the encoding
35    n_clauses: usize,
36    /// The number of new variables in the encoding
37    n_vars: u32,
38    _phantom: PhantomData<Sub>,
39}
40
41impl<const N: usize, Sub> Encode for Bimander<N, Sub>
42where
43    Sub: Encode + FromIterator<Lit> + From<Vec<Lit>>,
44{
45    fn n_lits(&self) -> usize {
46        self.in_lits.len()
47    }
48
49    fn encode<Col>(
50        &mut self,
51        collector: &mut Col,
52        var_manager: &mut dyn ManageVars,
53    ) -> Result<(), crate::OutOfMemory>
54    where
55        Col: CollectClauses,
56    {
57        if self.in_lits.len() <= 1 {
58            return Ok(());
59        }
60        let prev_clauses = collector.n_clauses();
61        let prev_vars = var_manager.n_used();
62
63        let n_splits = self.in_lits.len().div_ceil(N);
64        let p = utils::digits(n_splits - 1, 2);
65
66        let aux_vars: Vec<_> = (0..p).map(|_| var_manager.new_var()).collect();
67
68        for split in 0..n_splits {
69            let lits = &self.in_lits[split * N..std::cmp::min(self.in_lits.len(), (split + 1) * N)];
70            for (k, aux) in aux_vars.iter().enumerate().take(p as usize) {
71                let aux = aux.lit(split & (1 << k) == 0);
72                collector.extend_clauses(atomics::clause_impl_lit(lits, aux))?;
73            }
74            let mut sub = lits.iter().copied().collect::<Sub>();
75            sub.encode(collector, var_manager)?;
76        }
77
78        self.n_clauses = collector.n_clauses() - prev_clauses;
79        self.n_vars += var_manager.n_used() - prev_vars;
80        Ok(())
81    }
82}
83
84impl<const N: usize, Sub> IterInputs for Bimander<N, Sub> {
85    type Iter<'a>
86        = std::iter::Copied<std::slice::Iter<'a, Lit>>
87    where
88        Sub: 'a;
89
90    fn iter(&self) -> Self::Iter<'_> {
91        self.in_lits.iter().copied()
92    }
93}
94
95impl<const N: usize, Sub> EncodeStats for Bimander<N, Sub> {
96    fn n_clauses(&self) -> usize {
97        self.n_clauses
98    }
99
100    fn n_vars(&self) -> u32 {
101        self.n_vars
102    }
103}
104
105impl<const N: usize, Sub> From<Vec<Lit>> for Bimander<N, Sub> {
106    fn from(lits: Vec<Lit>) -> Self {
107        Self {
108            in_lits: lits,
109            n_clauses: 0,
110            n_vars: 0,
111            _phantom: PhantomData,
112        }
113    }
114}
115
116impl<const N: usize, Sub> FromIterator<Lit> for Bimander<N, Sub> {
117    fn from_iter<T: IntoIterator<Item = Lit>>(iter: T) -> Self {
118        Self {
119            in_lits: Vec::from_iter(iter),
120            n_clauses: 0,
121            n_vars: 0,
122            _phantom: PhantomData,
123        }
124    }
125}
126
127impl<const N: usize, Sub> Extend<Lit> for Bimander<N, Sub> {
128    fn extend<T: IntoIterator<Item = Lit>>(&mut self, iter: T) {
129        self.in_lits.extend(iter);
130    }
131}
132
133#[cfg(test)]
134mod tests {
135    use crate::{
136        encodings::am1::Encode,
137        instances::{BasicVarManager, Cnf, ManageVars},
138        lit, var,
139    };
140
141    #[test]
142    fn basic() {
143        let mut enc: super::Bimander = [lit![0], lit![1], lit![2], lit![3]].into_iter().collect();
144        let mut cnf = Cnf::new();
145        let mut vm = BasicVarManager::from_next_free(var![4]);
146        enc.encode(&mut cnf, &mut vm).unwrap();
147        assert_eq!(vm.n_used(), 5);
148        assert_eq!(cnf.len(), 10);
149    }
150}
rustsat/encodings/am1/bimander.rs

rustsat/encodings/am1/
bimander.rs
