search

sybila / biodivine-lib-bdd

A small library for BDD manipulation in Rust. Part of the BioDivine toolset.
MIT License
20 stars 4 forks source link

Add linear-time algorithm for BDD -> CNF conversion #37

Closed daemontus closed 1 year ago

daemontus commented 1 year ago

See https://cs.stackexchange.com/questions/92879/bdd-to-cnf-in-linear-time

daemontus commented 1 year ago

We now have "efficient" algorithms for BDD ⇒ CNF and BDD ⇒ DNF translation since 0.5.0.

In the end, I decided not to implement the linear algorithm linked above, since it introduces new variables to the CNF, which means the result would not be compatible with the variables of the original BDD.