This pull request supersedes #20. It introduces BddPartialValuations and allows for them to be used to create CNF/DNF formulas. In particular, this includes:
Declaration of BddPartialValuation as a wrapper around Vec<Option<bool>> with some useful utility APIs.
Optimised functions for creating conjunctive and disjunctive clauses based on partial valuations. These methods should be much faster than creating the resulting Bdd manually.
Naive implementation of cnf/dnf creation using the optimised methods.
Proper documentation and tutorial section.
What is not covered in this pull request:
A truly efficient CNF/DNF creation algorithm along the lines of #19.
A valuation iterator based on partial valuations. This requires an extensive rewrite of _impl_bdd_satisfying_valuations which we leave for future PRs.
A way to obtain partial valuations from a Bdd, such as least/greatest (in terms of number of fixed variables) partial valuations.
This pull request supersedes #20. It introduces
BddPartialValuationsand allows for them to be used to create CNF/DNF formulas. In particular, this includes:BddPartialValuationas a wrapper aroundVec<Option<bool>>with some useful utility APIs.Bddmanually.cnf/dnfcreation using the optimised methods.What is not covered in this pull request:
_impl_bdd_satisfying_valuationswhich we leave for future PRs.Bdd, such as least/greatest (in terms of number of fixed variables) partial valuations.