Binary adder PB encoding

.config/abbreviations.dic

@@ -1,4 +1,4 @@
-26
+27
 AIJ
 API
 APIs
@@ -17,6 +17,7 @@ GCD
 IJCAI
 IPASIR
 IPASIR's
+JSAT
 MCNF
 MOPB
 OPB

.config/lingo.dic

@@ -1,4 +1,4 @@
-37
+38
 accessor
 al
 AllDifferent
@@ -11,6 +11,7 @@ boolean
 cardinality
 changelog
 children's
+comparator
 decrementing
 encoding/S
 et

.config/names.dic

@@ -1,4 +1,4 @@
-55
+58
 Argelich
 Armin
 Audemard
@@ -12,7 +12,7 @@ Boufkhad
 bzip2
 CaDiCaL
 CaDiCaL's
-Een
+Eén
 Fazekas
 Fleury
 Gihwon
@@ -24,11 +24,13 @@ Jeremias
 Joao
 Josep
 Joshi
+Joose
 Katalin
 Kissat
 Kissat's
 Klieber
 Kwon
+Lett
 Lynce
 Manquinho
 Matti
@@ -52,5 +54,6 @@ Tobias
 Treengeling
 Vasco
 vOptLib
+Warners
 WebAssembly
 Yacine

.github/workflows/capi.yml

@@ -14,7 +14,7 @@ jobs:
     name: Build and test
     strategy:
       matrix:
-        os: [ubuntu-latest, macos-latest, windows-latest]
+        os: [ubuntu-latest, macos-latest]
     runs-on: ${{ matrix.os }}
     steps:
       - name: Checkout sources

.github/workflows/pyapi.yml

@@ -19,7 +19,7 @@ permissions:
 
 jobs:
   build-test:
-    name: Build and test
+    name: Build
     strategy:
       matrix:
         os: [ubuntu-latest, macos-latest, windows-latest]
@@ -32,16 +32,16 @@ jobs:
       - uses: Swatinem/rust-cache@v2
         with:
           shared-key: "build-test"
-      - name: Install latest nextest release
-        uses: taiki-e/install-action@nextest
+      # - name: Install latest nextest release
+      #   uses: taiki-e/install-action@nextest
       - name: Cargo build
         run: cargo build -p rustsat-pyapi --verbose
         env:
           CMAKE_BUILD_PARALLEL_LEVEL: ${{ fromJSON('["", "4"]')[matrix.os == 'macos-latest'] }}
-      - name: Run tests
-        run: cargo nextest run --profile ci -p rustsat-pyapi --verbose
-        env:
-          CMAKE_BUILD_PARALLEL_LEVEL: ${{ fromJSON('["", "4"]')[matrix.os == 'macos-latest'] }}
+      # - name: Run tests
+      #   run: cargo nextest run --profile ci -p rustsat-pyapi --verbose
+      #   env:
+      #     CMAKE_BUILD_PARALLEL_LEVEL: ${{ fromJSON('["", "4"]')[matrix.os == 'macos-latest'] }}
       - name: Build Python package
         uses: PyO3/maturin-action@v1
         with:

capi/cbindgen.toml

@@ -50,7 +50,7 @@ cpp_compat = true
 
 
 [export]
-include = ["DbTotalizer", "DynamicPolyWatchdog", "DbGte"]
+include = ["DbTotalizer", "DynamicPolyWatchdog", "DbGte", "BinaryAdder"]
 exclude = []
 # prefix = "CAPI_"
 item_types = []

capi/rustsat.h

@@ -43,6 +43,19 @@ typedef enum MaybeError {
   PrecisionDecreased,
 } MaybeError;
 
+/**
+ * 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.
+ */
+typedef struct BinaryAdder BinaryAdder;
+
 /**
  * Implementation of the binary adder tree generalized totalizer encoding
  * \[1\]. The implementation is incremental. The implementation is recursive.
@@ -97,6 +110,132 @@ typedef void (*CAssumpCollector)(int lit, void *data);
 extern "C" {
 #endif // __cplusplus
 
+/**
+ * Adds a new input literal to a [`BinaryAdder`].
+ *
+ * # Errors
+ *
+ * - If `lit` is not a valid IPASIR-style literal (e.g., `lit = 0`),
+ *     [`MaybeError::InvalidLiteral`] is returned
+ *
+ * # Safety
+ *
+ * `adder` must be a return value of [`bin_adder_new`] that [`bin_adder_drop`] has not yet been
+ * called on.
+ */
+enum MaybeError bin_adder_add(struct BinaryAdder *adder, int lit, size_t weight);
+
+/**
+ * Frees the memory associated with a [`BinaryAdder`]
+ *
+ * # Safety
+ *
+ * `adder` must be a return value of [`bin_adder_new`] and cannot be used
+ * afterwards again.
+ */
+void bin_adder_drop(struct BinaryAdder *adder);
+
+/**
+ * Lazily builds the _change in_ pseudo-boolean encoding to enable lower bounds from within the
+ * range.
+ *
+ * The min and max bounds are inclusive. After a call to [`bin_adder_encode_lb`] with
+ * `min_bound=2` and `max_bound=4`, bounds satisfying `2 <= bound <= 4` can be enforced.
+ *
+ * Clauses are returned via the `collector`. The `collector` function should expect clauses to be
+ * passed similarly to `ipasir_add`, as a 0-terminated sequence of literals where the literals are
+ * passed as the first argument and the `collector_data` as a second.
+ *
+ * `n_vars_used` must be the number of variables already used and will be incremented by the
+ * number of variables used up in the encoding.
+ *
+ * # Safety
+ *
+ * `adder` must be a return value of [`bin_adder_new`] that [`bin_adder_drop`] has not yet been
+ * called on.
+ *
+ * # Panics
+ *
+ * If `min_bound > max_bound`.
+ */
+void bin_adder_encode_lb(struct BinaryAdder *adder,
+                         size_t min_bound,
+                         size_t max_bound,
+                         uint32_t *n_vars_used,
+                         CClauseCollector collector,
+                         void *collector_data);
+
+/**
+ * Lazily builds the _change in_ pseudo-boolean encoding to enable upper bounds from within the
+ * range.
+ *
+ * The min and max bounds are inclusive. After a call to [`bin_adder_encode_ub`] with
+ * `min_bound=2` and `max_bound=4`, bounds satisfying `2 <= bound <= 4` can be enforced.
+ *
+ * Clauses are returned via the `collector`. The `collector` function should expect clauses to be
+ * passed similarly to `ipasir_add`, as a 0-terminated sequence of literals where the literals are
+ * passed as the first argument and the `collector_data` as a second.
+ *
+ * `n_vars_used` must be the number of variables already used and will be incremented by the
+ * number of variables used up in the encoding.
+ *
+ * # Safety
+ *
+ * `adder` must be a return value of [`bin_adder_new`] that [`bin_adder_drop`] has not yet been
+ * called on.
+ *
+ * # Panics
+ *
+ * If `min_bound > max_bound`.
+ */
+void bin_adder_encode_ub(struct BinaryAdder *adder,
+                         size_t min_bound,
+                         size_t max_bound,
+                         uint32_t *n_vars_used,
+                         CClauseCollector collector,
+                         void *collector_data);
+
+/**
+ * Returns assumptions/units for enforcing an upper bound (`sum of lits >= lb`). Make sure that
+ * [`bin_adder_encode_lb`] has been called adequately and nothing has been called afterwards,
+ * otherwise [`MaybeError::NotEncoded`] will be returned.
+ *
+ * Assumptions are returned via the collector callback. There is _no_ terminating zero, all
+ * assumptions are passed when [`bin_adder_enforce_lb`] returns.
+ *
+ * # Safety
+ *
+ * `adder` must be a return value of [`bin_adder_new`] that [`bin_adder_drop`] has not yet been
+ * called on.
+ */
+enum MaybeError bin_adder_enforce_lb(struct BinaryAdder *adder,
+                                     size_t ub,
+                                     CAssumpCollector collector,
+                                     void *collector_data);
+
+/**
+ * Returns assumptions/units for enforcing an upper bound (`sum of lits <= ub`). Make sure that
+ * [`bin_adder_encode_ub`] has been called adequately and nothing has been called afterwards,
+ * otherwise [`MaybeError::NotEncoded`] will be returned.
+ *
+ * Assumptions are returned via the collector callback. There is _no_ terminating zero, all
+ * assumptions are passed when [`bin_adder_enforce_ub`] returns.
+ *
+ * # Safety
+ *
+ * `adder` must be a return value of [`bin_adder_new`] that [`bin_adder_drop`] has not yet been
+ * called on.
+ */
+enum MaybeError bin_adder_enforce_ub(struct BinaryAdder *adder,
+                                     size_t ub,
+                                     CAssumpCollector collector,
+                                     void *collector_data);
+
+/**
+ * Creates a new [`BinaryAdder`] cardinality encoding
+ */
+struct BinaryAdder *bin_adder_new(void);
+
 /**
  * Adds a new input literal to a [`DynamicPolyWatchdog`].
  *
@@ -291,6 +430,10 @@ void gte_drop(struct DbGte *gte);
  * # Safety
  *
  * `gte` must be a return value of [`gte_new`] that [`gte_drop`] has not yet been called on.
+ *
+ * # Panics
+ *
+ * If `min_bound > max_bound`.
  */
 void gte_encode_ub(struct DbGte *gte,
                    size_t min_bound,
@@ -364,7 +507,7 @@ void tot_drop(struct DbTotalizer *tot);
  *
  * # Panics
  *
- * If `min_bound <= max_bound`.
+ * If `min_bound > max_bound`.
  */
 void tot_encode_ub(struct DbTotalizer *tot,
                    size_t min_bound,

capi/src/encodings.rs

@@ -153,6 +153,7 @@ impl<'a> ManageVars for VarManager<'a> {
     }
 }
 
+pub mod adder;
 pub mod dpw;
 pub mod gte;
 pub mod totalizer;