diff --git a/.github/workflows/pages.yml b/.github/workflows/pages.yml index 38696b11..2eaafe9c 100644 --- a/.github/workflows/pages.yml +++ b/.github/workflows/pages.yml @@ -33,7 +33,7 @@ jobs: - name: Install Python package run: pip install --no-index --find-links target/wheels/ rustsat - name: Build Python API docs - run: pip install pdoc && pdoc -o _site/pyapi/ rustsat + run: pip install pdoc && pdoc -o _site/pyapi/ --no-show-source rustsat - name: Upload artifact # Automatically uploads an artifact from the './_site' directory by default uses: actions/upload-pages-artifact@v3 diff --git a/Cargo.lock b/Cargo.lock index aa1465e6..c8a82059 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -740,6 +740,15 @@ dependencies = [ "rustc_version", ] +[[package]] +name = "inventory" +version = "0.3.16" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e5d80fade88dd420ce0d9ab6f7c58ef2272dde38db874657950f827d4982c817" +dependencies = [ + "rustversion", +] + [[package]] name = "is-terminal" version = "0.4.13" @@ -1075,6 +1084,7 @@ checksum = "e484fd2c8b4cb67ab05a318f1fd6fa8f199fcc30819f08f07d200809dba26c15" dependencies = [ "cfg-if", "indoc", + "inventory", "libc", "memoffset", "once_cell", @@ -1385,6 +1395,12 @@ dependencies = [ "termcolor", ] +[[package]] +name = "rustversion" +version = "1.0.18" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0e819f2bc632f285be6d7cd36e25940d45b2391dd6d9b939e79de557f7014248" + [[package]] name = "ryu" version = "1.0.18" diff --git a/pyapi/Cargo.toml b/pyapi/Cargo.toml index 3c26cf5c..cf6f43e1 100644 --- a/pyapi/Cargo.toml +++ b/pyapi/Cargo.toml @@ -19,6 +19,7 @@ pyo3 = { version = "0.23.3", features = [ "extension-module", "abi3", "abi3-py37", + "multiple-pymethods", ] } [build-dependencies] diff --git a/pyapi/examples/pyapi-dpw.py b/pyapi/examples/pyapi-dpw.py index cd1e02d1..58619798 100644 --- a/pyapi/examples/pyapi-dpw.py +++ b/pyapi/examples/pyapi-dpw.py @@ -1,19 +1,19 @@ from rustsat import Lit, VarManager -from rustsat.encodings import DynamicPolyWatchdog as Dpw +from rustsat.encodings.pb import DynamicPolyWatchdog as Dpw # Lit creates a literal object from an ipasir integer representation. The # encoding takes a list of (lit, weight) pairs as input. input_lits = [ - (Lit(1), 5), - (Lit(-2), 4), - (Lit(3), 3), - (Lit(-4), 2), - (Lit(5), 1), + (Lit(1), 5), + (Lit(-2), 4), + (Lit(3), 3), + (Lit(-4), 2), + (Lit(5), 1), ] # Getting unused variables is handled by a VarManager. Create one that has 5 # variables already used. -vm = VarManager(n_used = 5) +vm = VarManager(n_used=5) dpw = Dpw(input_lits) @@ -26,8 +26,8 @@ # DIMACS format. for cl in cnf: for l in cl: - print(l.to_ipasir(), end=' ') - print('0') + print(l.to_ipasir(), end=" ") + print("0") # Get assumptions to enforce an upper bound of 4 on the input literals. The # assumptions are a list of literals. diff --git a/pyapi/pyproject.toml b/pyapi/pyproject.toml index 9a983bf4..fd84c5e9 100644 --- a/pyapi/pyproject.toml +++ b/pyapi/pyproject.toml @@ -5,3 +5,6 @@ requires-python = ">=3.7" [build-system] requires = ["maturin>=1.0,<2.0"] build-backend = "maturin" + +[tool.maturin] +python-source = "python" diff --git a/pyapi/rustsat/__init__.py b/pyapi/python/rustsat/__init__.py similarity index 100% rename from pyapi/rustsat/__init__.py rename to pyapi/python/rustsat/__init__.py diff --git a/pyapi/rustsat/__init__.pyi b/pyapi/python/rustsat/__init__.pyi similarity index 84% rename from pyapi/rustsat/__init__.pyi rename to pyapi/python/rustsat/__init__.pyi index dc9cf6b2..dc992dbb 100644 --- a/pyapi/rustsat/__init__.pyi +++ b/pyapi/python/rustsat/__init__.pyi @@ -1,13 +1,15 @@ from typing import List, final +from rustsat import encodings + @final class Lit: - def __new__(cls, ipasir: int) -> Lit: ... + def __new__(cls, ipasir: int) -> "Lit": ... def to_ipasir(self) -> int: ... @final class Clause: - def __new__(cls, lits: List[Lit]) -> Clause: ... + def __new__(cls, lits: List[Lit]) -> "Clause": ... def is_unit(self) -> bool: ... def is_binary(self) -> bool: ... def add(self, lit: Lit) -> None: ... @@ -17,7 +19,7 @@ class Clause: @final class Cnf: - def __new__(cls, clauses: List[Clause]) -> Cnf: ... + def __new__(cls, clauses: List[Clause]) -> "Cnf": ... def add_clause(self, clause: Clause) -> None: ... def add_unit(self, unit: Lit) -> None: ... def add_binary(self, lit1: Lit, lit2: Lit) -> None: ... @@ -34,7 +36,7 @@ class Cnf: @final class VarManager: - def __new__(cls, n_used: int = 0) -> VarManager: ... + def __new__(cls, n_used: int = 0) -> "VarManager": ... def increase_used(self, n_used: int) -> None: ... def new_var(self) -> int: ... def n_used(self) -> int: ... diff --git a/pyapi/rustsat/encodings/__init__.py b/pyapi/python/rustsat/encodings/__init__.py similarity index 100% rename from pyapi/rustsat/encodings/__init__.py rename to pyapi/python/rustsat/encodings/__init__.py diff --git a/pyapi/python/rustsat/encodings/__init__.pyi b/pyapi/python/rustsat/encodings/__init__.pyi new file mode 100644 index 00000000..fc1ea710 --- /dev/null +++ b/pyapi/python/rustsat/encodings/__init__.pyi @@ -0,0 +1 @@ +from rustsat.encodings import card, pb, am1 diff --git a/pyapi/python/rustsat/encodings/am1/__init__.py b/pyapi/python/rustsat/encodings/am1/__init__.py new file mode 100644 index 00000000..e9d86d41 --- /dev/null +++ b/pyapi/python/rustsat/encodings/am1/__init__.py @@ -0,0 +1,5 @@ +from .rustsat.encodings.am1 import * + +__doc__ = rustsat.encodings.am1.__doc__ +if hasattr(rustsat.encodings.am1, "__all__"): + __all__ = rustsat.encodings.am1.__all__ diff --git a/pyapi/python/rustsat/encodings/am1/__init__.pyi b/pyapi/python/rustsat/encodings/am1/__init__.pyi new file mode 100644 index 00000000..8ed37316 --- /dev/null +++ b/pyapi/python/rustsat/encodings/am1/__init__.pyi @@ -0,0 +1,34 @@ +from rustsat import Lit, Cnf, VarManager +from typing import List, final + +@final +class Bitwise: + def __new__(cls, lits: List[Lit]) -> "Bitwise": ... + def n_lits(self) -> int: ... + def n_clauses(self) -> int: ... + def n_vars(self) -> int: ... + def encode(self, var_manager: VarManager) -> Cnf: ... + +@final +class Commander: + def __new__(cls, lits: List[Lit]) -> "Commander": ... + def n_lits(self) -> int: ... + def n_clauses(self) -> int: ... + def n_vars(self) -> int: ... + def encode(self, var_manager: VarManager) -> Cnf: ... + +@final +class Ladder: + def __new__(cls, lits: List[Lit]) -> "Ladder": ... + def n_lits(self) -> int: ... + def n_clauses(self) -> int: ... + def n_vars(self) -> int: ... + def encode(self, var_manager: VarManager) -> Cnf: ... + +@final +class Pairwise: + def __new__(cls, lits: List[Lit]) -> "Pairwise": ... + def n_lits(self) -> int: ... + def n_clauses(self) -> int: ... + def n_vars(self) -> int: ... + def encode(self, var_manager: VarManager) -> Cnf: ... diff --git a/pyapi/python/rustsat/encodings/card/__init__.py b/pyapi/python/rustsat/encodings/card/__init__.py new file mode 100644 index 00000000..fd26067f --- /dev/null +++ b/pyapi/python/rustsat/encodings/card/__init__.py @@ -0,0 +1,5 @@ +from .rustsat.encodings.card import * + +__doc__ = rustsat.encodings.card.__doc__ +if hasattr(rustsat.encodings.card, "__all__"): + __all__ = rustsat.encodings.card.__all__ diff --git a/pyapi/python/rustsat/encodings/card/__init__.pyi b/pyapi/python/rustsat/encodings/card/__init__.pyi new file mode 100644 index 00000000..625f45c1 --- /dev/null +++ b/pyapi/python/rustsat/encodings/card/__init__.pyi @@ -0,0 +1,12 @@ +from rustsat import Lit, Cnf, VarManager +from typing import List, final + +@final +class Totalizer: + def __new__(cls, lits: List[Lit]) -> "Totalizer": ... + def extend(self, lits: List[Lit]) -> None: ... + def n_lits(self) -> int: ... + def n_clauses(self) -> int: ... + def n_vars(self) -> int: ... + def encode_ub(self, min_ub: int, max_ub: int, var_manager: VarManager) -> Cnf: ... + def enforce_ub(self, ub) -> List[Lit]: ... diff --git a/pyapi/python/rustsat/encodings/pb/__init__.py b/pyapi/python/rustsat/encodings/pb/__init__.py new file mode 100644 index 00000000..fb339209 --- /dev/null +++ b/pyapi/python/rustsat/encodings/pb/__init__.py @@ -0,0 +1,5 @@ +from .rustsat.encodings.pb import * + +__doc__ = rustsat.encodings.pb.__doc__ +if hasattr(rustsat.encodings.pb, "__all__"): + __all__ = rustsat.encodings.pb.__all__ diff --git a/pyapi/python/rustsat/encodings/pb/__init__.pyi b/pyapi/python/rustsat/encodings/pb/__init__.pyi new file mode 100644 index 00000000..9fc56e2a --- /dev/null +++ b/pyapi/python/rustsat/encodings/pb/__init__.pyi @@ -0,0 +1,37 @@ +from rustsat import Lit, Cnf, VarManager +from typing import List, final + +@final +class GeneralizedTotalizer: + def __new__(cls, wlits: List[tuple[int, Lit]]) -> "GeneralizedTotalizer": ... + def extend(self, lits: List[Lit]) -> None: ... + def weight_sum(self) -> int: ... + def n_clauses(self) -> int: ... + def n_vars(self) -> int: ... + def encode_ub(self, min_ub: int, max_ub: int, var_manager: VarManager) -> Cnf: ... + def enforce_ub(self, ub) -> List[Lit]: ... + +@final +class DynamicPolyWatchdog: + def __new__(cls, wlits: List[tuple[int, Lit]]) -> "DynamicPolyWatchdog": ... + def weight_sum(self) -> int: ... + def n_clauses(self) -> int: ... + def n_vars(self) -> int: ... + def encode_ub(self, min_ub: int, max_ub: int, var_manager: VarManager) -> Cnf: ... + def enforce_ub(self, ub) -> List[Lit]: ... + +@final +class BinaryAdder: + def __new__(cls, wlits: List[tuple[int, Lit]]) -> "BinaryAdder": ... + def extend(self, lits: List[Lit]) -> None: ... + def weight_sum(self) -> int: ... + def n_clauses(self) -> int: ... + def n_vars(self) -> int: ... + def encode_ub(self, min_ub: int, max_ub: int, var_manager: VarManager) -> Cnf: ... + def enforce_ub(self, ub) -> List[Lit]: ... + def encode_lb(self, min_lb: int, max_lb: int, var_manager: VarManager) -> Cnf: ... + def enforce_lb(self, lb) -> List[Lit]: ... + def encode_both( + self, min_bound: int, max_bound: int, var_manager: VarManager + ) -> Cnf: ... + def enforce_eq(self, val) -> List[Lit]: ... diff --git a/pyapi/rustsat/py.typed b/pyapi/python/rustsat/py.typed similarity index 100% rename from pyapi/rustsat/py.typed rename to pyapi/python/rustsat/py.typed diff --git a/pyapi/rustsat/encodings/__init__.pyi b/pyapi/rustsat/encodings/__init__.pyi deleted file mode 100644 index 91aa0c9b..00000000 --- a/pyapi/rustsat/encodings/__init__.pyi +++ /dev/null @@ -1,31 +0,0 @@ -from rustsat import Lit, Cnf, VarManager -from typing import List, final - -@final -class Totalizer: - def __new__(cls, lits: List[Lit]) -> Totalizer: ... - def extend(self, lits: List[Lit]) -> None: ... - def n_lits(self) -> int: ... - def n_clauses(self) -> int: ... - def n_vars(self) -> int: ... - def encode_ub(self, max_ub: int, min_ub: int, var_manager: VarManager) -> Cnf: ... - def enforce_ub(self, ub) -> List[Lit]: ... - -@final -class GeneralizedTotalizer: - def __new__(cls, wlits: List[tuple[int, Lit]]) -> GeneralizedTotalizer: ... - def extend(self, lits: List[Lit]) -> None: ... - def weight_sum(self) -> int: ... - def n_clauses(self) -> int: ... - def n_vars(self) -> int: ... - def encode_ub(self, max_ub: int, min_ub: int, var_manager: VarManager) -> Cnf: ... - def enforce_ub(self, ub) -> List[Lit]: ... - -@final -class DynamicPolyWatchdog: - def __new__(cls, wlits: List[tuple[int, Lit]]) -> DynamicPolyWatchdog: ... - def weight_sum(self) -> int: ... - def n_clauses(self) -> int: ... - def n_vars(self) -> int: ... - def encode_ub(self, max_ub: int, min_ub: int, var_manager: VarManager) -> Cnf: ... - def enforce_ub(self, ub) -> List[Lit]: ... diff --git a/pyapi/src/encodings.rs b/pyapi/src/encodings.rs index 6dfbb959..17134a2e 100644 --- a/pyapi/src/encodings.rs +++ b/pyapi/src/encodings.rs @@ -1,273 +1,5 @@ //! # Python API for RustSAT Encodings -use pyo3::prelude::*; - -use rustsat::{ - encodings::{ - card::{ - BoundUpper as CardBU, BoundUpperIncremental as CardBUI, DbTotalizer, - Encode as CardEncode, - }, - pb::{ - BoundUpper as PbBU, BoundUpperIncremental as PbBUI, DbGte, - DynamicPolyWatchdog as RsDpw, Encode as PbEncode, - }, - EncodeStats, Error, - }, - instances::{BasicVarManager, Cnf as RsCnf}, - types::Lit as RsLit, -}; - -use crate::{ - handle_oom, - instances::{Cnf, VarManager}, - types::Lit, -}; - -#[allow(clippy::needless_pass_by_value)] -fn convert_error(err: Error) -> PyErr { - match err { - Error::NotEncoded => { - pyo3::exceptions::PyRuntimeError::new_err("not encoded to enforce bound") - } - Error::Unsat => pyo3::exceptions::PyValueError::new_err("encoding is unsat"), - } -} - -/// Implementation of the binary adder tree totalizer encoding \[1\]. -/// The implementation is incremental as extended in \[2\]. -/// The implementation is based on a node database. -/// For now, this implementation only supports upper bounding. -/// -/// # References -/// -/// - \[1\] Olivier Bailleux and Yacine Boufkhad: _Efficient CNF Encoding of Boolean Cardinality Constraints_, CP 2003. -/// - \[2\] Ruben Martins and Saurabh Joshi and Vasco Manquinho and Ines Lynce: _Incremental Cardinality Constraints for MaxSAT_, CP 2014. -#[pyclass] -#[repr(transparent)] -pub struct Totalizer(DbTotalizer); - -impl From for Totalizer { - fn from(value: DbTotalizer) -> Self { - Self(value) - } -} - -impl From for DbTotalizer { - fn from(value: Totalizer) -> Self { - value.0 - } -} - -#[pymethods] -impl Totalizer { - #[new] - fn new(lits: Vec) -> Self { - let lits: Vec = unsafe { std::mem::transmute(lits) }; - DbTotalizer::from_iter(lits).into() - } - - /// Adds additional input literals to the totalizer - fn extend(&mut self, lits: Vec) { - let lits: Vec = unsafe { std::mem::transmute(lits) }; - self.0.extend(lits); - } - - /// Gets the number of input literals in the encoding - fn n_lits(&self) -> usize { - self.0.n_lits() - } - - /// Gets the number of clauses in the encoding - fn n_clauses(&self) -> usize { - self.0.n_clauses() - } - - /// Gets the number of variables in the encoding - fn n_vars(&self) -> u32 { - self.0.n_vars() - } - - /// Incrementally builds the totalizer encoding to that upper bounds - /// in the range `max_ub..=min_ub` can be enforced. New variables will - /// be taken from `var_manager`. - fn encode_ub( - &mut self, - max_ub: usize, - min_ub: usize, - var_manager: &mut VarManager, - ) -> PyResult { - let mut cnf = RsCnf::new(); - let var_manager: &mut BasicVarManager = var_manager.into(); - handle_oom!(self - .0 - .encode_ub_change(max_ub..=min_ub, &mut cnf, var_manager)); - Ok(cnf.into()) - } - - /// Gets assumptions to enforce the given upper bound. Make sure that - /// the required encoding is built first. - fn enforce_ub(&self, ub: usize) -> PyResult> { - let assumps: Vec = - unsafe { std::mem::transmute(self.0.enforce_ub(ub).map_err(convert_error)?) }; - Ok(assumps) - } -} - -/// Implementation of the binary adder tree generalized totalizer encoding -/// \[1\]. The implementation is incremental. The implementation is recursive. -/// This encoding only support upper bounding. Lower bounding can be achieved by -/// negating the input literals. This is implemented in -/// [`super::simulators::Inverted`]. -/// The implementation is based on a node database. -/// -/// # References -/// -/// - \[1\] Saurabh Joshi and Ruben Martins and Vasco Manquinho: _Generalized -/// Totalizer Encoding for Pseudo-Boolean Constraints_, CP 2015. -#[pyclass] -#[repr(transparent)] -pub struct GeneralizedTotalizer(DbGte); - -impl From for GeneralizedTotalizer { - fn from(value: DbGte) -> Self { - Self(value) - } -} - -impl From for DbGte { - fn from(value: GeneralizedTotalizer) -> Self { - value.0 - } -} - -#[pymethods] -impl GeneralizedTotalizer { - #[new] - fn new(lits: Vec<(Lit, usize)>) -> Self { - let lits: Vec<(RsLit, usize)> = unsafe { std::mem::transmute(lits) }; - DbGte::from_iter(lits).into() - } - - /// Adds additional input literals to the generalized totalizer - fn extend(&mut self, lits: Vec<(Lit, usize)>) { - let lits: Vec<(RsLit, usize)> = unsafe { std::mem::transmute(lits) }; - self.0.extend(lits); - } - - /// Gets the sum of weights in the encoding - fn weight_sum(&self) -> usize { - self.0.weight_sum() - } - - /// Gets the number of clauses in the encoding - fn n_clauses(&self) -> usize { - self.0.n_clauses() - } - - /// Gets the number of variables in the encoding - fn n_vars(&self) -> u32 { - self.0.n_vars() - } - - /// Incrementally builds the GTE encoding to that upper bounds - /// in the range `max_ub..=min_ub` can be enforced. New variables will - /// be taken from `var_manager`. - fn encode_ub( - &mut self, - max_ub: usize, - min_ub: usize, - var_manager: &mut VarManager, - ) -> PyResult { - let mut cnf = RsCnf::new(); - let var_manager: &mut BasicVarManager = var_manager.into(); - handle_oom!(self - .0 - .encode_ub_change(max_ub..=min_ub, &mut cnf, var_manager)); - Ok(cnf.into()) - } - - /// Gets assumptions to enforce the given upper bound. Make sure that - /// the required encoding is built first. - fn enforce_ub(&self, ub: usize) -> PyResult> { - let assumps: Vec = - unsafe { std::mem::transmute(self.0.enforce_ub(ub).map_err(convert_error)?) }; - Ok(assumps) - } -} - -/// Implementation of the dynamic polynomial watchdog (DPW) encoding \[1\]. -/// -/// **Note**: -/// This implementation of the DPW encoding only supports incrementally -/// changing the bound, but not adding new input literals. Calling extend after -/// encoding resets the entire encoding and with the next encode and entirely -/// new encoding will be returned. -/// -/// ## References -/// -/// - \[1\] Tobias Paxian and Sven Reimer and Bernd Becker: _Dynamic Polynomial -/// Watchdog Encoding for Solving Weighted MaxSAT_, SAT 2018. -#[pyclass] -#[repr(transparent)] -pub struct DynamicPolyWatchdog(RsDpw); - -impl From for DynamicPolyWatchdog { - fn from(value: RsDpw) -> Self { - Self(value) - } -} - -impl From for RsDpw { - fn from(value: DynamicPolyWatchdog) -> Self { - value.0 - } -} - -#[pymethods] -impl DynamicPolyWatchdog { - #[new] - fn new(lits: Vec<(Lit, usize)>) -> Self { - let lits: Vec<(RsLit, usize)> = unsafe { std::mem::transmute(lits) }; - RsDpw::from_iter(lits).into() - } - - /// Gets the sum of weights in the encoding - fn weight_sum(&self) -> usize { - self.0.weight_sum() - } - - /// Gets the number of clauses in the encoding - fn n_clauses(&self) -> usize { - self.0.n_clauses() - } - - /// Gets the number of variables in the encoding - fn n_vars(&self) -> u32 { - self.0.n_vars() - } - - /// Incrementally builds the DPW encoding to that upper bounds - /// in the range `max_ub..=min_ub` can be enforced. New variables will - /// be taken from `var_manager`. - fn encode_ub( - &mut self, - max_ub: usize, - min_ub: usize, - var_manager: &mut VarManager, - ) -> PyResult { - let mut cnf = RsCnf::new(); - let var_manager: &mut BasicVarManager = var_manager.into(); - handle_oom!(self - .0 - .encode_ub_change(max_ub..=min_ub, &mut cnf, var_manager)); - Ok(cnf.into()) - } - - /// Gets assumptions to enforce the given upper bound. Make sure that - /// the required encoding is built first. - fn enforce_ub(&self, ub: usize) -> PyResult> { - let assumps = self.0.enforce_ub(ub).map_err(convert_error)?; - Ok(assumps.into_iter().map(Into::into).collect()) - } -} +pub mod am1; +pub mod card; +pub mod pb; diff --git a/pyapi/src/encodings/am1.rs b/pyapi/src/encodings/am1.rs new file mode 100644 index 00000000..71f3c7e2 --- /dev/null +++ b/pyapi/src/encodings/am1.rs @@ -0,0 +1,117 @@ +//! # Python API for RustSAT At-Most-One Encodings + +use pyo3::prelude::*; + +use rustsat::{ + encodings::{ + am1::{ + Bitwise as RsBitwise, Commander as RsCommander, Encode, Ladder as RsLadder, + Pairwise as RsPairwise, + }, + EncodeStats, + }, + instances::{BasicVarManager, Cnf as RsCnf}, + types::Lit as RsLit, +}; + +use crate::{ + handle_oom, + instances::{Cnf, VarManager}, + types::Lit, +}; + +macro_rules! implement_pyapi { + ($type:ty, $rstype:ty) => { + impl From<$rstype> for $type { + fn from(value: $rstype) -> Self { + Self(value) + } + } + + impl From<$type> for $rstype { + fn from(value: $type) -> Self { + value.0 + } + } + + #[pymethods] + impl $type { + #[new] + fn new(lits: Vec) -> Self { + let lits: Vec = unsafe { std::mem::transmute(lits) }; + <$rstype>::from_iter(lits).into() + } + + /// Gets the number of input literals in the encoding + fn n_lits(&self) -> usize { + self.0.n_lits() + } + + /// Gets the number of clauses in the encoding + fn n_clauses(&self) -> usize { + self.0.n_clauses() + } + + /// Gets the number of variables in the encoding + fn n_vars(&self) -> u32 { + self.0.n_vars() + } + + /// Builds the encoding. New variables will be taken from `var_manager`. + fn encode(&mut self, var_manager: &mut VarManager) -> PyResult { + let mut cnf = RsCnf::new(); + let var_manager: &mut BasicVarManager = var_manager.into(); + handle_oom!(self.0.encode(&mut cnf, var_manager)); + Ok(cnf.into()) + } + } + }; +} + +/// Implementations of the bitwise at-most-1 encoding. +/// +/// # References +/// +/// - Steven D. Prestwich: _Negative Effects of Modeling Techniques on Search Performance_, in +/// Trends in Constraint Programming 2007. +#[pyclass] +#[repr(transparent)] +pub struct Bitwise(RsBitwise); + +implement_pyapi!(Bitwise, RsBitwise); + +/// Implementations of the commander at-most-1 encoding. +/// +/// The encoding uses 4 splits and the pairwise encoding as the sub encoding. +/// +/// # References +/// +/// - Will Klieber and Gihwon Kwon: _Efficient CNF Encoding for Selecting 1 from N Objects, CFV +/// 2007. +#[pyclass] +#[repr(transparent)] +pub struct Commander(RsCommander); + +implement_pyapi!(Commander, RsCommander); + +/// Implementations of the ladder at-most-1 encoding. +/// +/// # References +/// +/// - Ian P. Gent and Peter Nightingale: _A new Encoding of AllDifferent into SAT_, CP 2004. +#[pyclass] +#[repr(transparent)] +pub struct Ladder(RsLadder); + +implement_pyapi!(Ladder, RsLadder); + +/// Implementations of the pairwise at-most-1 encoding. +/// +/// # References +/// +/// - Steven D. Prestwich: _CNF Encodings_, in Handbook of Satisfiability 2021. +#[pyclass] +#[repr(transparent)] +pub struct Pairwise(RsPairwise); + +implement_pyapi!(Pairwise, RsPairwise); diff --git a/pyapi/src/encodings/card.rs b/pyapi/src/encodings/card.rs new file mode 100644 index 00000000..554cdcb9 --- /dev/null +++ b/pyapi/src/encodings/card.rs @@ -0,0 +1,116 @@ +//! # Python API for RustSAT Cardinality Encodings + +use pyo3::prelude::*; + +use rustsat::{ + encodings::{ + card::{ + BoundUpper as CardBU, BoundUpperIncremental as CardBUI, DbTotalizer, + Encode as CardEncode, + }, + EncodeStats, Error, + }, + instances::{BasicVarManager, Cnf as RsCnf}, + types::Lit as RsLit, +}; + +use crate::{ + handle_oom, + instances::{Cnf, VarManager}, + types::Lit, +}; + +#[allow(clippy::needless_pass_by_value)] +fn convert_error(err: Error) -> PyErr { + match err { + Error::NotEncoded => { + pyo3::exceptions::PyRuntimeError::new_err("not encoded to enforce bound") + } + Error::Unsat => pyo3::exceptions::PyValueError::new_err("encoding is unsat"), + } +} + +macro_rules! implement_pyapi { + ($type:ty, $rstype:ty) => { + impl From<$rstype> for $type { + fn from(value: $rstype) -> Self { + Self(value) + } + } + + impl From<$type> for $rstype { + fn from(value: $type) -> Self { + value.0 + } + } + + #[pymethods] + impl $type { + #[new] + fn new(lits: Vec) -> Self { + let lits: Vec = unsafe { std::mem::transmute(lits) }; + <$rstype>::from_iter(lits).into() + } + + /// Adds additional input literals to the encoding + fn extend(&mut self, lits: Vec) { + let lits: Vec = unsafe { std::mem::transmute(lits) }; + self.0.extend(lits); + } + + /// Gets the number of input literals in the encoding + fn n_lits(&self) -> usize { + self.0.n_lits() + } + + /// Gets the number of clauses in the encoding + fn n_clauses(&self) -> usize { + self.0.n_clauses() + } + + /// Gets the number of variables in the encoding + fn n_vars(&self) -> u32 { + self.0.n_vars() + } + + /// Incrementally builds the encoding to that upper bounds in the range + /// `min_ub..=max_ub` can be enforced. New variables will be taken from `var_manager`. + fn encode_ub( + &mut self, + min_ub: usize, + max_ub: usize, + var_manager: &mut VarManager, + ) -> PyResult { + let mut cnf = RsCnf::new(); + let var_manager: &mut BasicVarManager = var_manager.into(); + handle_oom!(self + .0 + .encode_ub_change(min_ub..=max_ub, &mut cnf, var_manager)); + Ok(cnf.into()) + } + + /// Gets assumptions to enforce the given upper bound. Make sure that the required + /// encoding is built first. + fn enforce_ub(&self, ub: usize) -> PyResult> { + let assumps: Vec = + unsafe { std::mem::transmute(self.0.enforce_ub(ub).map_err(convert_error)?) }; + Ok(assumps) + } + } + }; +} + +/// Implementation of the binary adder tree totalizer encoding \[1\]. +/// The implementation is incremental as extended in \[2\]. +/// The implementation is based on a node database. +/// For now, this implementation only supports upper bounding. +/// +/// # References +/// +/// - \[1\] Olivier Bailleux and Yacine Boufkhad: _Efficient CNF Encoding of Boolean Cardinality Constraints_, CP 2003. +/// - \[2\] Ruben Martins and Saurabh Joshi and Vasco Manquinho and Ines Lynce: _Incremental Cardinality Constraints for MaxSAT_, CP 2014. +#[pyclass] +#[repr(transparent)] +pub struct Totalizer(DbTotalizer); + +implement_pyapi!(Totalizer, DbTotalizer); diff --git a/pyapi/src/encodings/pb.rs b/pyapi/src/encodings/pb.rs new file mode 100644 index 00000000..1b808186 --- /dev/null +++ b/pyapi/src/encodings/pb.rs @@ -0,0 +1,240 @@ +//! # Python API for RustSAT PB Encodings + +use pyo3::prelude::*; + +use rustsat::{ + encodings::{ + pb::{ + BinaryAdder as RsAdder, BoundBoth, BoundBothIncremental, BoundLower, + BoundLowerIncremental, BoundUpper as PbBU, BoundUpperIncremental as PbBUI, DbGte, + DynamicPolyWatchdog as RsDpw, Encode as PbEncode, + }, + EncodeStats, Error, + }, + instances::{BasicVarManager, Cnf as RsCnf}, + types::Lit as RsLit, +}; + +use crate::{ + handle_oom, + instances::{Cnf, VarManager}, + types::Lit, +}; + +#[allow(clippy::needless_pass_by_value)] +fn convert_error(err: Error) -> PyErr { + match err { + Error::NotEncoded => { + pyo3::exceptions::PyRuntimeError::new_err("not encoded to enforce bound") + } + Error::Unsat => pyo3::exceptions::PyValueError::new_err("encoding is unsat"), + } +} + +macro_rules! shared_pyapi { + (derive_from, $type:ty, $rstype:ty) => { + impl From<$rstype> for $type { + fn from(value: $rstype) -> Self { + Self(value) + } + } + + impl From<$type> for $rstype { + fn from(value: $type) -> Self { + value.0 + } + } + }; + (extend, $type:ty) => { + #[pymethods] + impl $type { + /// Adds additional input literals to the encoding + fn extend(&mut self, lits: Vec<(Lit, usize)>) { + let lits: Vec<(RsLit, usize)> = unsafe { std::mem::transmute(lits) }; + self.0.extend(lits); + } + } + }; + (base, $type:ty, $rstype:ty) => { + #[pymethods] + impl $type { + #[new] + fn new(lits: Vec<(Lit, usize)>) -> Self { + let lits: Vec<(RsLit, usize)> = unsafe { std::mem::transmute(lits) }; + <$rstype>::from_iter(lits).into() + } + + /// Gets the sum of weights in the encoding + fn weight_sum(&self) -> usize { + self.0.weight_sum() + } + + /// Gets the number of clauses in the encoding + fn n_clauses(&self) -> usize { + self.0.n_clauses() + } + + /// Gets the number of variables in the encoding + fn n_vars(&self) -> u32 { + self.0.n_vars() + } + } + }; + (ub, $type:ty) => { + #[pymethods] + impl $type { + /// Incrementally builds the encoding to that upper bounds in the range + /// `min_ub..=max_ub` can be enforced. New variables will be taken from `var_manager`. + fn encode_ub( + &mut self, + min_ub: usize, + max_ub: usize, + var_manager: &mut VarManager, + ) -> PyResult { + let mut cnf = RsCnf::new(); + let var_manager: &mut BasicVarManager = var_manager.into(); + handle_oom!(self + .0 + .encode_ub_change(min_ub..=max_ub, &mut cnf, var_manager)); + Ok(cnf.into()) + } + + /// Gets assumptions to enforce the given upper bound. Make sure that the required + /// encoding is built first. + fn enforce_ub(&self, ub: usize) -> PyResult> { + let assumps: Vec = + unsafe { std::mem::transmute(self.0.enforce_ub(ub).map_err(convert_error)?) }; + Ok(assumps) + } + } + }; + (lb, $type:ty) => { + #[pymethods] + impl $type { + /// Incrementally builds the encoding to that lower bounds in the range `min_lb..=max_lb` + /// can be enforced. New variables will be taken from `var_manager`. + fn encode_lb( + &mut self, + min_lb: usize, + max_lb: usize, + var_manager: &mut VarManager, + ) -> PyResult { + let mut cnf = RsCnf::new(); + let var_manager: &mut BasicVarManager = var_manager.into(); + handle_oom!(self + .0 + .encode_lb_change(min_lb..=max_lb, &mut cnf, var_manager)); + Ok(cnf.into()) + } + + /// Gets assumptions to enforce the given lower bound. Make sure that the required encoding + /// is built first. + fn enforce_lb(&self, lb: usize) -> PyResult> { + let assumps = self.0.enforce_lb(lb).map_err(convert_error)?; + Ok(assumps.into_iter().map(Into::into).collect()) + } + } + }; + (both, $type:ty) => { + #[pymethods] + impl $type { + /// Incrementally builds the encoding to that both bounds in the range + /// `min_bound..=max_bound` can be enforced. New variables will be taken from + /// `var_manager`. + fn encode_both( + &mut self, + min_bound: usize, + max_bound: usize, + var_manager: &mut VarManager, + ) -> PyResult { + let mut cnf = RsCnf::new(); + let var_manager: &mut BasicVarManager = var_manager.into(); + handle_oom!(self.0.encode_both_change( + min_bound..=max_bound, + &mut cnf, + var_manager + )); + Ok(cnf.into()) + } + + /// Gets assumptions to enforce the given equality bound. Make sure that the required + /// encoding is built first. + fn enforce_eq(&self, val: usize) -> PyResult> { + let assumps = self.0.enforce_eq(val).map_err(convert_error)?; + Ok(assumps.into_iter().map(Into::into).collect()) + } + } + }; +} + +macro_rules! implement_pyapi { + (ub, $type:ty, $rstype:ty) => { + shared_pyapi!(derive_from, $type, $rstype); + shared_pyapi!(base, $type, $rstype); + shared_pyapi!(extend, $type); + shared_pyapi!(ub, $type); + }; + (ub_noextend, $type:ty, $rstype:ty) => { + shared_pyapi!(derive_from, $type, $rstype); + shared_pyapi!(base, $type, $rstype); + shared_pyapi!(ub, $type); + }; + (both, $type:ty, $rstype:ty) => { + shared_pyapi!(derive_from, $type, $rstype); + shared_pyapi!(base, $type, $rstype); + shared_pyapi!(extend, $type); + shared_pyapi!(ub, $type); + shared_pyapi!(lb, $type); + shared_pyapi!(both, $type); + }; +} + +/// Implementation of the binary adder tree generalized totalizer encoding +/// \[1\]. The implementation is incremental. The implementation is recursive. +/// This encoding only support upper bounding. Lower bounding can be achieved by +/// negating the input literals. This is implemented in +/// [`super::simulators::Inverted`]. +/// The implementation is based on a node database. +/// +/// # References +/// +/// - \[1\] Saurabh Joshi and Ruben Martins and Vasco Manquinho: _Generalized +/// Totalizer Encoding for Pseudo-Boolean Constraints_, CP 2015. +#[pyclass] +#[repr(transparent)] +pub struct GeneralizedTotalizer(DbGte); + +implement_pyapi!(ub, GeneralizedTotalizer, DbGte); + +/// Implementation of the dynamic polynomial watchdog (DPW) encoding \[1\]. +/// +/// **Note**: +/// This implementation of the DPW encoding only supports incrementally +/// changing the bound, but not adding new input literals. Calling extend after +/// encoding resets the entire encoding and with the next encode and entirely +/// new encoding will be returned. +/// +/// ## References +/// +/// - \[1\] Tobias Paxian and Sven Reimer and Bernd Becker: _Dynamic Polynomial +/// Watchdog Encoding for Solving Weighted MaxSAT_, SAT 2018. +#[pyclass] +#[repr(transparent)] +pub struct DynamicPolyWatchdog(RsDpw); + +implement_pyapi!(ub_noextend, DynamicPolyWatchdog, RsDpw); + +/// Implementation of the binary adder encoding first described in \[1\]. +/// The implementation follows the description in \[2\]. +/// +/// ## References +/// +/// - \[1\] Joose P. Warners: _A linear-time transformation of linear inequalities into conjunctive +/// normal form_, Inf. Process. Lett. 1998. +/// - \[2\] Niklas Eén and Niklas Sörensson: _Translating Pseudo-Boolean Constraints into SAT_, +/// JSAT 2006. +#[pyclass] +#[repr(transparent)] +pub struct BinaryAdder(RsAdder); + +implement_pyapi!(both, BinaryAdder, RsAdder); diff --git a/pyapi/src/lib.rs b/pyapi/src/lib.rs index c3ede98d..e0fdb044 100644 --- a/pyapi/src/lib.rs +++ b/pyapi/src/lib.rs @@ -23,7 +23,11 @@ mod instances; mod types; use crate::{ - encodings::{DynamicPolyWatchdog, GeneralizedTotalizer, Totalizer}, + encodings::{ + am1::{Bitwise, Commander, Ladder, Pairwise}, + card::Totalizer, + pb::{BinaryAdder, DynamicPolyWatchdog, GeneralizedTotalizer}, + }, instances::{Cnf, VarManager}, types::{Clause, Lit}, }; @@ -43,15 +47,35 @@ fn rustsat(py: Python<'_>, m: &Bound<'_, PyModule>) -> PyResult<()> { m.add_class::()?; let encodings = PyModule::new(py, "rustsat.encodings")?; - encodings.add_class::()?; - encodings.add_class::()?; - encodings.add_class::()?; + let card = PyModule::new(py, "rustsat.encodings.card")?; + card.add_class::()?; + let pb = PyModule::new(py, "rustsat.encodings.pb")?; + pb.add_class::()?; + pb.add_class::()?; + pb.add_class::()?; + let am1 = PyModule::new(py, "rustsat.encodings.am1")?; + am1.add_class::()?; + am1.add_class::()?; + am1.add_class::()?; + am1.add_class::()?; + encodings.add("card", &card)?; + encodings.add("pb", &pb)?; + encodings.add("am1", &am1)?; m.add("encodings", &encodings)?; // To import encodings. Fix from https://github.com/PyO3/pyo3/issues/759 py.import("sys")? .getattr("modules")? .set_item("rustsat.encodings", &encodings)?; + py.import("sys")? + .getattr("modules")? + .set_item("rustsat.encodings.pb", &pb)?; + py.import("sys")? + .getattr("modules")? + .set_item("rustsat.encodings.card", &card)?; + py.import("sys")? + .getattr("modules")? + .set_item("rustsat.encodings.am1", &am1)?; Ok(()) } diff --git a/pyapi/stubtest-allowlist.txt b/pyapi/stubtest-allowlist.txt index 1b5184fc..49c3011a 100644 --- a/pyapi/stubtest-allowlist.txt +++ b/pyapi/stubtest-allowlist.txt @@ -1,2 +1 @@ rustsat.rustsat -rustsat.encodings diff --git a/shell.nix b/shell.nix index 974760b6..eacee064 100644 --- a/shell.nix +++ b/shell.nix @@ -14,6 +14,7 @@ in cargo-nextest release-plz jq + maturin ]; buildInputs = libs; RUSTC_VERSION = overrides.toolchain.channel;