Add pick_cube_symbolic(), pick_cube_symbolic_set()

.project-words.txt

@@ -86,6 +86,7 @@ madvise
 manylinux
 mdbook
 memchr
+minterm
 Miri
 mmap
 MSVC

bindings/cpp/include/oxidd/bcdd.hpp

@@ -653,6 +653,35 @@ class bcdd_function {
     return util::assignment(capi::oxidd_bcdd_pick_cube(_func));
   }
 
+  /// Pick a satisfying assignment, represented as BCDD
+  ///
+  /// Locking behavior: acquires the manager's lock for shared access.
+  ///
+  /// @returns  A satisfying assignment if there exists one. Otherwise (i.e., if
+  ///           `f` is ⊥), ⊥ is returned.
+  [[nodiscard]] bcdd_function pick_cube_symbolic() const noexcept {
+    return capi::oxidd_bcdd_pick_cube_symbolic(_func);
+  }
+
+  /// Pick a satisfying assignment, represented as BCDD, using the literals in
+  /// `literal_set` if there is a choice
+  ///
+  /// `literal_set` is represented as a conjunction of literals. Whenever there
+  /// is a choice for a variable, it will be set to true if the variable has a
+  /// positive occurrence in `literal_set`, and set to false if it occurs
+  /// negated in `literal_set`. If the variable does not occur in `literal_set`,
+  /// then it will be left as don't care if possible, otherwise an arbitrary
+  /// (not necessarily random) choice will be performed.
+  ///
+  /// Locking behavior: acquires the manager's lock for shared access.
+  ///
+  /// @returns  A satisfying assignment if there exists one. Otherwise (i.e., if
+  ///           `f` is ⊥), ⊥ is returned.
+  [[nodiscard]] bcdd_function
+  pick_cube_symbolic_set(const bcdd_function &literal_set) const noexcept {
+    return capi::oxidd_bcdd_pick_cube_symbolic_set(_func, literal_set._func);
+  }
+
   /// Evaluate this Boolean function with arguments `args`
   ///
   /// `args` determines the valuation for all variables. Missing values are

bindings/cpp/include/oxidd/bdd.hpp

@@ -657,6 +657,35 @@ class bdd_function {
     return util::assignment(capi::oxidd_bdd_pick_cube(_func));
   }
 
+  /// Pick a satisfying assignment, represented as BDD
+  ///
+  /// Locking behavior: acquires the manager's lock for shared access.
+  ///
+  /// @returns  A satisfying assignment if there exists one. Otherwise (i.e., if
+  ///           `f` is ⊥), ⊥ is returned.
+  [[nodiscard]] bdd_function pick_cube_symbolic() const noexcept {
+    return capi::oxidd_bdd_pick_cube_symbolic(_func);
+  }
+
+  /// Pick a satisfying assignment, represented as BDD, using the literals in
+  /// `literal_set` if there is a choice
+  ///
+  /// `literal_set` is represented as a conjunction of literals. Whenever there
+  /// is a choice for a variable, it will be set to true if the variable has a
+  /// positive occurrence in `literal_set`, and set to false if it occurs
+  /// negated in `literal_set`. If the variable does not occur in `literal_set`,
+  /// then it will be left as don't care if possible, otherwise an arbitrary
+  /// (not necessarily random) choice will be performed.
+  ///
+  /// Locking behavior: acquires the manager's lock for shared access.
+  ///
+  /// @returns  A satisfying assignment if there exists one. Otherwise (i.e., if
+  ///           `f` is ⊥), ⊥ is returned.
+  [[nodiscard]] bdd_function
+  pick_cube_symbolic_set(const bdd_function &literal_set) const noexcept {
+    return capi::oxidd_bdd_pick_cube_symbolic_set(_func, literal_set._func);
+  }
+
   /// Evaluate this Boolean function with arguments `args`
   ///
   /// `args` determines the valuation for all variables. Missing values are

bindings/cpp/include/oxidd/concepts.hpp

@@ -232,6 +232,12 @@ concept substitution = function_subst<typename S::function> &&
 /// - `f.pick_cube()` returns a satisfying `oxidd::util::assignment` if `f` is
 ///   satisfiable, or an empty `oxidd::util::assignment` otherwise. `f` must be
 ///   valid.
+/// - `f.pick_cube_symbolic()` returns a satisfying assignment as decision
+///   diagram if there is one or ⊥.
+/// - `f.pick_cube_symbolic_set(literal_set)` returns a satisfying assignment as
+///   decision diagram if there is one or ⊥. Whenever there is a choice for a
+///   variable, and the variable is defined in `literal_set`, the respective
+///   polarity is used.
 /// - `f.eval(args)` evaluates the Boolean function `f` with arguments `args`
 ///   and returns the respective result. `args` determines the valuation for all
 ///   variables. Missing values are assumed to be false. The order is
@@ -283,6 +289,8 @@ concept boolean_function =
       { f.sat_count_double(levels) } -> std::same_as<double>;
 
       { f.pick_cube() } -> std::same_as<util::assignment>;
+      { f.pick_cube_symbolic() } -> std::same_as<F>;
+      { f.pick_cube_symbolic_set(f) } -> std::same_as<F>;
 
       { f.eval(args) } -> std::same_as<bool>;
     } &&

bindings/cpp/include/oxidd/zbdd.hpp

@@ -618,6 +618,35 @@ class zbdd_function {
     return util::assignment(capi::oxidd_zbdd_pick_cube(_func));
   }
 
+  /// Pick a satisfying assignment, represented as ZBDD
+  ///
+  /// Locking behavior: acquires the manager's lock for shared access.
+  ///
+  /// @returns  A satisfying assignment if there exists one. Otherwise (i.e., if
+  ///           `f` is ⊥), ⊥ is returned.
+  [[nodiscard]] zbdd_function pick_cube_symbolic() const noexcept {
+    return capi::oxidd_zbdd_pick_cube_symbolic(_func);
+  }
+
+  /// Pick a satisfying assignment, represented as ZBDD, using the literals in
+  /// `literal_set` if there is a choice
+  ///
+  /// `literal_set` is represented as a conjunction of literals. Whenever there
+  /// is a choice for a variable, it will be set to true if the variable has a
+  /// positive occurrence in `literal_set`, and set to false if it occurs
+  /// negated in `literal_set`. If the variable does not occur in `literal_set`,
+  /// then it will be left as don't care if possible, otherwise an arbitrary
+  /// (not necessarily random) choice will be performed.
+  ///
+  /// Locking behavior: acquires the manager's lock for shared access.
+  ///
+  /// @returns  A satisfying assignment if there exists one. Otherwise (i.e., if
+  ///           `f` is ⊥), ⊥ is returned.
+  [[nodiscard]] zbdd_function
+  pick_cube_symbolic_set(const zbdd_function &literal_set) const noexcept {
+    return capi::oxidd_zbdd_pick_cube_symbolic_set(_func, literal_set._func);
+  }
+
   /// Evaluate this Boolean function with arguments `args`
   ///
   /// `args` determines the valuation for all variables. Missing values are

bindings/cpp/tests/boolean-function.cpp

@@ -121,9 +121,15 @@ using my_enumerate::enumerate;
 template <boolean_function_manager M> class test_all_boolean_functions {
   M _mgr;
   slice<typename M::function> _vars, _var_handles;
-  /// Stores all possible Boolean functions with `vars.size()` vars
+  /// Stores all possible Boolean functions over `vars.size()` variables
   std::vector<typename M::function> _boolean_functions;
+  /// Map from Boolean functions as decision diagrams to their explicit (truth
+  /// table) representations
   std::unordered_map<typename M::function, explicit_b_func> _dd_to_boolean_func;
+  /// Map from variables (`0..vars.size()`) to Boolean functions
+  ///
+  /// Example for three variables: `[0b01010101, 0b00110011, 0b00001111]`
+  std::vector<explicit_b_func> _var_functions;
 
 public:
   /// Initialize the test, generating DDs for all Boolean functions for the
@@ -191,8 +197,34 @@ template <boolean_function_manager M> class test_all_boolean_functions {
       assert(inserted &&
              "two different Boolean functions have the same representation");
     }
+
+    _var_functions.reserve(nvars);
+    for (unsigned i = 0; i < nvars; ++i) {
+      explicit_b_func f = 0;
+      for (unsigned assignment = 0; assignment < num_assignments; ++assignment)
+        f |= explicit_b_func{(assignment >> i) & 1} << assignment;
+      _var_functions.push_back(f);
+    }
+  }
+
+private:
+  typename M::function make_cube(unsigned positive, unsigned negative) const {
+    assert((positive & negative) == 0);
+
+    typename M::function cube = _boolean_functions.back(); // ⊤
+    for (const auto &[i, var] : enumerate(_vars)) {
+      if (((positive >> i) & 1) != 0) {
+        cube &= var;
+      } else if (((negative >> i) & 1) != 0) {
+        cube &= ~var;
+      }
+    }
+
+    assert(!cube.is_invalid());
+    return cube;
   }
 
+public:
   /// Test basic operations on all Boolean functions
   void basic() const {
     const unsigned nvars = _vars.size();
@@ -280,6 +312,79 @@ template <boolean_function_manager M> class test_all_boolean_functions {
           }
         }
       }
+
+      /* pick_cube() etc. */ {
+        // This is a stripped-down version of the Rust test; we only test that
+        // the results of `pick_cube()` and `pick_cube_symbolic()` agree
+        // (therefore, both can be represented as a conjunction of literals),
+        // and that they imply `f`.
+        const util::assignment cube = f.pick_cube();
+        const explicit_b_func actual =
+            _dd_to_boolean_func.at(f.pick_cube_symbolic());
+
+        if (f_explicit == 0) {
+          assert(actual == 0);
+          assert(cube.size() == 0);
+        } else {
+          assert(cube.size() == nvars);
+          assert((actual & ~f_explicit) == 0);
+
+          explicit_b_func cube_func = func_mask;
+          for (unsigned var = 0; var < nvars; ++var) {
+            switch (cube[var]) {
+            case util::opt_bool::NONE:
+              break;
+            case util::opt_bool::FALSE:
+              cube_func &= ~_var_functions[var];
+              break;
+            case util::opt_bool::TRUE:
+              cube_func &= _var_functions[var];
+              break;
+            }
+          }
+
+          assert(cube_func == actual);
+        }
+
+        for (unsigned pos = 0; pos < num_assignments; ++pos) {
+          for (unsigned neg = 0; neg < num_assignments; ++neg) {
+            if ((pos & neg) != 0)
+              continue;
+
+            const explicit_b_func actual = _dd_to_boolean_func.at(
+                f.pick_cube_symbolic_set(make_cube(pos, neg)));
+
+            if (f_explicit == 0) {
+              assert(actual == 0);
+            } else {
+              assert((actual & !f_explicit) == 0);
+
+              for (const auto &[var, var_func] : enumerate(_var_functions)) {
+                if ((actual & var_func) >> (1 << var) == (actual & ~var_func))
+                  continue; // var is don't care
+                explicit_b_func flipped = 0;
+                if ((actual & var_func) == 0) { // selected to be false
+                  if ((pos & (1 << var)) == 0)
+                    continue; // was not requested to be true
+                  flipped = actual << (1 << var);
+                } else {
+                  assert((actual & ~var_func) == 0 &&
+                         "not a conjunction of literals");
+                  // selected to be false
+                  if ((neg & (1 << var)) == 0)
+                    continue; // was not requested to be true
+                  flipped = actual >> (1 << var);
+                }
+
+                // If the variable was selected to be the opposite of the
+                // request, then the reason must be that the cube would not have
+                // implied the function.
+                assert((flipped & ~f_explicit) != 0);
+              }
+            }
+          }
+        }
+      }
     }
   }
 
@@ -356,16 +461,6 @@ template <boolean_function_manager M> class test_all_boolean_functions {
     const explicit_b_func num_functions = 1 << num_assignments;
     const explicit_b_func func_mask = num_functions - 1;
 
-    // Example for 3 vars: [0b01010101, 0b00110011, 0b00001111]
-    std::vector<explicit_b_func> var_functions;
-    var_functions.reserve(nvars);
-    for (unsigned i = 0; i < nvars; ++i) {
-      explicit_b_func f = 0;
-      for (unsigned assignment = 0; assignment < num_assignments; ++assignment)
-        f |= explicit_b_func{(assignment >> i) & 1} << assignment;
-      var_functions.push_back(f);
-    }
-
     // TODO: restrict (once we have it in the C/C++ API)
 
     // quantification
@@ -381,10 +476,10 @@ template <boolean_function_manager M> class test_all_boolean_functions {
       // precompute `assignment_to_mask`
       for (const auto &[assignment, mask] : enumerate(assignment_to_mask)) {
         explicit_b_func tmp = func_mask;
-        for (const auto [i, func] : enumerate(var_functions)) {
+        for (const auto [i, func] : enumerate(_var_functions)) {
           if (((var_set >> i) & 1) != 0)
             continue;
-          const explicit_b_func f = var_functions[i];
+          const explicit_b_func f = _var_functions[i];
           tmp &= ((assignment >> i) & 1) != 0 ? f : ~f;
         }
         mask = tmp;

bindings/python/oxidd/bcdd.py

@@ -347,6 +347,19 @@ def pick_cube(self) -> Optional[util.Assignment]:
         raw = _lib.oxidd_bcdd_pick_cube(self._func)
         return util.Assignment._from_raw(raw) if raw.len > 0 else None
 
+    @override
+    def pick_cube_symbolic(self) -> Self:
+        return self.__class__._from_raw(_lib.oxidd_bcdd_pick_cube_symbolic(self._func))
+
+    @override
+    def pick_cube_symbolic_set(self, literal_set: Self) -> Self:
+        assert (
+            self._func._p == literal_set._func._p
+        ), "`self` and `literal_set` must belong to the same manager"
+        return self.__class__._from_raw(
+            _lib.oxidd_bcdd_pick_cube_symbolic_set(self._func, literal_set._func)
+        )
+
     @override
     def eval(self, args: collections.abc.Collection[tuple[Self, bool]]) -> bool:
         n = len(args)

bindings/python/oxidd/bdd.py

@@ -345,6 +345,19 @@ def pick_cube(self) -> Optional[util.Assignment]:
         raw = _lib.oxidd_bdd_pick_cube(self._func)
         return util.Assignment._from_raw(raw) if raw.len > 0 else None
 
+    @override
+    def pick_cube_symbolic(self) -> Self:
+        return self.__class__._from_raw(_lib.oxidd_bdd_pick_cube_symbolic(self._func))
+
+    @override
+    def pick_cube_symbolic_set(self, literal_set: Self) -> Self:
+        assert (
+            self._func._p == literal_set._func._p
+        ), "`self` and `literal_set` must belong to the same manager"
+        return self.__class__._from_raw(
+            _lib.oxidd_bdd_pick_cube_symbolic_set(self._func, literal_set._func)
+        )
+
     @override
     def eval(self, args: collections.abc.Collection[tuple[Self, bool]]) -> bool:
         n = len(args)

bindings/python/oxidd/protocols.py

@@ -281,6 +281,33 @@ def pick_cube(self) -> Optional[Assignment]:
         """
         raise NotImplementedError
 
+    @abstractmethod
+    def pick_cube_symbolic(self) -> Self:
+        """Pick a satisfying assignment, represented as decision diagram
+
+        Returns ``⊥`` iff ``self`` is unsatisfiable.
+
+        Acquires the manager's lock for shared access.
+        """
+        raise NotImplementedError
+
+    @abstractmethod
+    def pick_cube_symbolic_set(self, literal_set: Self) -> Self:
+        """Pick a satisfying assignment, represented as BDD, using the
+        literals in ``literal_set`` if there is a choice
+
+        ``literal_set`` is represented as a conjunction of literals. Whenever
+        there is a choice for a variable, it will be set to true if the variable
+        has a positive occurrence in ``literal_set``, and set to false if it
+        occurs negated in ``literal_set``. If the variable does not occur in
+        ``literal_set``, then it will be left as don't care if possible,
+        otherwise an arbitrary (not necessarily random) choice will be
+        performed.
+
+        Acquires the manager's lock for shared access.
+        """
+        raise NotImplementedError
+
     @abstractmethod
     def eval(self, args: collections.abc.Collection[tuple[Self, bool]]) -> bool:
         """Evaluate this Boolean function with arguments ``args``