RSDD CLI is generating a non-reduced BDD with duplicate leaves/redundant nodes. We suspect this is leading to a noticeable performance loss in runtime of programs using larger BDDs. It is unclear if this issue is in the CLI only, or if it is in the core RSDD code.
Repro Steps:
(1) Add print statement to weighted_model_count.rs code to get printed BDD output
Here is the change as a git diff to main branch at commit sha `39aadfb`:
diff --git a/bin/weighted_model_count.rs b/bin/weighted_model_count.rs
index e2359d4..a482696 100644
--- a/bin/weighted_model_count.rs
+++ b/bin/weighted_model_count.rs
@@ -155,6 +155,7 @@ fn single_wmc(
let bdd = builder.smooth(bdd, num_vars);
let res = bdd.unsmoothed_wmc(¶ms);
+ println!("{}", bdd.to_string_debug());
let elapsed = start.elapsed();
Update here -- I added a quickcheck test to test for BDD canonicity during compilation and confirmed that compiled BDDs are reduced, so this is likely a printing issue and not affecting core performance.
Bug:
RSDD CLI is generating a non-reduced BDD with duplicate leaves/redundant nodes. We suspect this is leading to a noticeable performance loss in runtime of programs using larger BDDs. It is unclear if this issue is in the CLI only, or if it is in the core RSDD code.
Repro Steps:
(1) Add print statement to
weighted_model_count.rs
code to get printed BDD outputHere is the change as a git diff to main branch at commit sha `39aadfb`:
(2) Run RSDD CLI
Command:
cargo run --release --bin weighted_model_count --features="cli" -- -f minimal_example.sexp -w minimal_example_weights.json
minimal_example.sexp
:
minimal_example_weights.json
:
Outputs:
Expected Output:
Actual Output: