With #500 we add support for arbitrary variable reorderings. Yet, there are some non-monotone cases we can do faster! For example, if one is only swapping adjacent variables, then one can do it in a single (unnested) sweep! This is essentially the Jump_Down case (see #500 and #730) without the assumption that the target level is empty in the input BDD. Instead, the target level may be remapped to be prior to or later than the jumping level.
See [Sølvsten25] for more details.
References
- [Sølvsten25] S. Sølvsten “I/O-efficient Symbolic Model Checking”. Aarhus University (2025)
With #500 we add support for arbitrary variable reorderings. Yet, there are some non-monotone cases we can do faster! For example, if one is only swapping adjacent variables, then one can do it in a single (unnested) sweep! This is essentially the
Jump_Downcase (see #500 and #730) without the assumption that the target level is empty in the input BDD. Instead, the target level may be remapped to be prior to or later than the jumping level.See [Sølvsten25] for more details.
References