feat(encodings): Bimander at-most-one encoding

src/encodings/am1.rs

@@ -35,6 +35,9 @@ pub use bitwise::Bitwise;
 mod commander;
 pub use commander::Commander;
 
+mod bimander;
+pub use bimander::Bimander;
+
 /// Trait for all at-most-1 encodings
 pub trait Encode {
     /// Gets the number of literals in the encoding

src/encodings/am1/bimander.rs

@@ -0,0 +1,127 @@
+//! # Bimander At-Most-1 Encoding
+//!
+//! ## References
+//!
+//! - Van-Hau Nguyen and Son Thay Mai: _A New Method to Encode the At-Most-One Constraint into SAT,
+//!   SOICT 2015.
+
+use std::marker::PhantomData;
+
+use super::Encode;
+use crate::{
+    encodings::{atomics, CollectClauses, EncodeStats, IterInputs},
+    instances::ManageVars,
+    types::Lit,
+    utils,
+};
+
+/// Implementation of the bimander at-most-1 encoding.
+///
+/// # Generics
+///
+/// - `Sub`: the sub encoding to use for each split
+/// - `N`: the size of the splits
+///
+/// # References
+///
+/// - Van-Hau Nguyen and Son Thay Mai: _A New Method to Encode the At-Most-One Constraint into SAT,
+///   SOICT 2015.
+#[derive(Default)]
+pub struct Bimander<const N: usize = 4, Sub = super::Pairwise> {
+    /// Input literals
+    in_lits: Vec<Lit>,
+    /// The number of clauses in the encoding
+    n_clauses: usize,
+    /// The number of new variables in the encoding
+    n_vars: u32,
+    _phantom: PhantomData<Sub>,
+}
+
+impl<const N: usize, Sub> Encode for Bimander<N, Sub>
+where
+    Sub: Encode + FromIterator<Lit> + From<Vec<Lit>>,
+{
+    fn n_lits(&self) -> usize {
+        self.in_lits.len()
+    }
+
+    fn encode<Col>(
+        &mut self,
+        collector: &mut Col,
+        var_manager: &mut dyn ManageVars,
+    ) -> Result<(), crate::OutOfMemory>
+    where
+        Col: CollectClauses,
+    {
+        if self.in_lits.len() <= 1 {
+            return Ok(());
+        }
+        let prev_clauses = collector.n_clauses();
+        let prev_vars = var_manager.n_used();
+
+        let n_splits = (self.in_lits.len() + N - 1) / N;
+        let p = utils::digits(n_splits - 1, 2);
+
+        let aux_vars: Vec<_> = (0..p).map(|_| var_manager.new_var()).collect();
+
+        for split in 0..n_splits {
+            let lits = &self.in_lits[split * N..std::cmp::min(self.in_lits.len(), (split + 1) * N)];
+            for k in 0..p as usize {
+                let aux = aux_vars[k].lit(split & (1 << k) == 0);
+                collector.extend_clauses(atomics::clause_impl_lit(lits, aux))?;
+            }
+            let mut sub = lits.iter().copied().collect::<Sub>();
+            sub.encode(collector, var_manager)?;
+        }
+
+        self.n_clauses = collector.n_clauses() - prev_clauses;
+        self.n_vars += var_manager.n_used() - prev_vars;
+        Ok(())
+    }
+}
+
+impl<const N: usize, Sub> IterInputs for Bimander<N, Sub> {
+    type Iter<'a> = std::iter::Copied<std::slice::Iter<'a, Lit>> where Sub: 'a;
+
+    fn iter(&self) -> Self::Iter<'_> {
+        self.in_lits.iter().copied()
+    }
+}
+
+impl<const N: usize, Sub> EncodeStats for Bimander<N, Sub> {
+    fn n_clauses(&self) -> usize {
+        self.n_clauses
+    }
+
+    fn n_vars(&self) -> u32 {
+        self.n_vars
+    }
+}
+
+impl<const N: usize, Sub> From<Vec<Lit>> for Bimander<N, Sub> {
+    fn from(lits: Vec<Lit>) -> Self {
+        Self {
+            in_lits: lits,
+            n_clauses: 0,
+            n_vars: 0,
+            _phantom: PhantomData,
+        }
+    }
+}
+
+impl<const N: usize, Sub> FromIterator<Lit> for Bimander<N, Sub> {
+    fn from_iter<T: IntoIterator<Item = Lit>>(iter: T) -> Self {
+        Self {
+            in_lits: Vec::from_iter(iter),
+            n_clauses: 0,
+            n_vars: 0,
+            _phantom: PhantomData,
+        }
+    }
+}
+
+impl<const N: usize, Sub> Extend<Lit> for Bimander<N, Sub> {
+    fn extend<T: IntoIterator<Item = Lit>>(&mut self, iter: T) {
+        self.in_lits.extend(iter);
+    }
+}

src/encodings/am1/bitwise.rs

@@ -47,7 +47,7 @@ impl Encode for Bitwise {
         }
         let prev_clauses = collector.n_clauses();
 
-        let p = utils::digits(self.in_lits.len(), 2);
+        let p = utils::digits(self.in_lits.len() - 1, 2);
         let aux_vars: Vec<_> = (0..p).map(|_| var_manager.new_var()).collect();
 
         let clause = |idx: usize, k: usize| {

tests/am1_encodings.rs

@@ -87,3 +87,8 @@ fn bitwise() {
 fn commander() {
     test_am1::<am1::Commander<2>>();
 }
+
+#[test]
+fn bimander() {
+    test_am1::<am1::Bimander<2>>();
+}