Skip to content

Commit

Permalink
feat(pyapi): include bimander encoding
Browse files Browse the repository at this point in the history
  • Loading branch information
chrjabs committed Mar 9, 2025
1 parent 3489c1e commit baf235a
Show file tree
Hide file tree
Showing 2 changed files with 25 additions and 3 deletions.
10 changes: 9 additions & 1 deletion pyapi/python/rustsat/encodings/am1/__init__.pyi
Original file line number Diff line number Diff line change
@@ -1,7 +1,15 @@
from rustsat import Lit, Cnf, VarManager
from typing import List, final

__all__ = ["Bitwise", "Commander", "Ladder", "Pairwise"]
__all__ = ["Bimander", "Bitwise", "Commander", "Ladder", "Pairwise"]

@final
class Bimander:
def __new__(cls, lits: List[Lit]) -> "Bimander": ...
def n_lits(self) -> int: ...
def n_clauses(self) -> int: ...
def n_vars(self) -> int: ...
def encode(self, var_manager: VarManager) -> Cnf: ...

@final
class Bitwise:
Expand Down
18 changes: 16 additions & 2 deletions pyapi/src/encodings/am1.rs
Original file line number Diff line number Diff line change
Expand Up @@ -5,8 +5,8 @@ use pyo3::prelude::*;
use rustsat::{
encodings::{
am1::{
Bitwise as RsBitwise, Commander as RsCommander, Encode, Ladder as RsLadder,
Pairwise as RsPairwise,
Bimander as RsBimander, Bitwise as RsBitwise, Commander as RsCommander, Encode,
Ladder as RsLadder, Pairwise as RsPairwise,
},
EncodeStats,
},
Expand Down Expand Up @@ -68,6 +68,20 @@ macro_rules! implement_pyapi {
};
}

/// Implementation of the bimander at-most-1 encoding.
///
/// The sub encoding is fixed to [`Pairwise`] and the size of the splits to 4.
///
/// # References
///
/// - Van-Hau Nguyen and Son Thay Mai: _A New Method to Encode the At-Most-One Constraint into SAT,
/// SOICT 2015.
#[pyclass]
#[repr(transparent)]
pub struct Bimander(RsBimander);

implement_pyapi!(Bimander, RsBimander);

/// Implementations of the bitwise at-most-1 encoding.
///
/// # References
Expand Down

0 comments on commit baf235a

Please sign in to comment.