rustsat/encodings/am1/
bitwise.rs

1//! # Bitwise At-Most-1 Encoding
2//!
3//! ## References
4//!
5//! - Steven D. Prestwich: _Finding large Cliques using SAT Local Search_, in Trends in Constraint
6//!   Programming 2007.
7//! - Steven D. Prestwich: _CNF Encodings_, in Handbook of Satisfiability 2021.
8
9use super::Encode;
10use crate::{
11    encodings::{atomics, CollectClauses, EncodeStats, IterInputs},
12    instances::ManageVars,
13    types::Lit,
14    utils,
15};
16
17/// Implementations of the bitwise at-most-1 encoding.
18///
19/// # References
20///
21/// - Steven D. Prestwich: _Finding large Cliques using SAT Local Search_, in Trends in Constraint
22///   Programming 2007.
23/// - Steven D. Prestwich: _CNF Encodings_, in Handbook of Satisfiability 2021.
24#[derive(Default, Debug)]
25#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
26pub struct Bitwise {
27    /// Input literals
28    in_lits: Vec<Lit>,
29    /// The number of clauses in the encoding
30    n_clauses: usize,
31    /// The number of new variables in the encoding
32    n_vars: u32,
33}
34
35impl Encode for Bitwise {
36    fn n_lits(&self) -> usize {
37        self.in_lits.len()
38    }
39
40    fn encode<Col>(
41        &mut self,
42        collector: &mut Col,
43        var_manager: &mut dyn ManageVars,
44    ) -> Result<(), crate::OutOfMemory>
45    where
46        Col: CollectClauses,
47    {
48        if self.in_lits.len() <= 1 {
49            return Ok(());
50        }
51        let prev_clauses = collector.n_clauses();
52
53        let p = utils::digits(self.in_lits.len() - 1, 2);
54        let aux_vars: Vec<_> = (0..p).map(|_| var_manager.new_var()).collect();
55
56        let clause = |idx: usize, k: usize| {
57            let aux = aux_vars[k].lit(idx & (1 << k) == 0);
58            atomics::lit_impl_lit(self.in_lits[idx], aux)
59        };
60        collector.extend_clauses(
61            (0..self.in_lits.len()).flat_map(|idx| (0..p as usize).map(move |k| clause(idx, k))),
62        )?;
63
64        self.n_clauses = collector.n_clauses() - prev_clauses;
65        self.n_vars += p;
66        Ok(())
67    }
68}
69
70impl IterInputs for Bitwise {
71    type Iter<'a> = std::iter::Copied<std::slice::Iter<'a, Lit>>;
72
73    fn iter(&self) -> Self::Iter<'_> {
74        self.in_lits.iter().copied()
75    }
76}
77
78impl EncodeStats for Bitwise {
79    fn n_clauses(&self) -> usize {
80        self.n_clauses
81    }
82
83    fn n_vars(&self) -> u32 {
84        self.n_vars
85    }
86}
87
88impl From<Vec<Lit>> for Bitwise {
89    fn from(lits: Vec<Lit>) -> Self {
90        Self {
91            in_lits: lits,
92            n_clauses: 0,
93            n_vars: 0,
94        }
95    }
96}
97
98impl FromIterator<Lit> for Bitwise {
99    fn from_iter<T: IntoIterator<Item = Lit>>(iter: T) -> Self {
100        Self {
101            in_lits: Vec::from_iter(iter),
102            n_clauses: 0,
103            n_vars: 0,
104        }
105    }
106}
107
108impl Extend<Lit> for Bitwise {
109    fn extend<T: IntoIterator<Item = Lit>>(&mut self, iter: T) {
110        self.in_lits.extend(iter);
111    }
112}
113
114#[cfg(test)]
115mod tests {
116    use crate::{
117        encodings::am1::Encode,
118        instances::{BasicVarManager, Cnf, ManageVars},
119        lit, var,
120    };
121
122    #[test]
123    fn basic() {
124        let mut enc: super::Bitwise = [lit![0], lit![1], lit![2], lit![3]].into_iter().collect();
125        let mut cnf = Cnf::new();
126        let mut vm = BasicVarManager::from_next_free(var![4]);
127        enc.encode(&mut cnf, &mut vm).unwrap();
128        assert_eq!(vm.n_used(), 6);
129        assert_eq!(cnf.len(), 8);
130    }
131}
rustsat/encodings/am1/bitwise.rs

rustsat/encodings/am1/
bitwise.rs
