Bandido is a library that partially implements Binary Decition Diagrams in FSharp based on what we currently know about the subject [0,1,2,3,4]. Graph based algorithms for boolean manipulation can be used to solve and efficiently represent boolean formulas. Bandido in FSharp is an attempt to implement the algorithms in a functional style. Use bandido library for FSharp at your own logical risk. Happy satisfiability!
Make, Build, Apply and Restrict algorithms are currently implemented. A rudimentary visualisation capability is also available. Given a table t : u -> (i,l,h) [3], the function Plot.t2dot t will translate the table into a dot graph that can be compiled into a picture. Several cases of use are showed in Script.fsx and a set of tests are implemented in the Test folder.
The project requires dotnet core 2.0.
To compile, ensure to be placed into the src/ROBDD folder and type into the console:
dotnet buildto test, go to the Test folder and execute:
dotnet test- Mk
- Build
- Apply
- Restrict (exponential running time)
- Restrict (linear running time)
- SatCount
- Apply Dynamic Programming to SatCount
- AnySat
- function t2svg : T -> Bdd.svg
- AllSat algorithm [3]
- Simplify algorithm [3]
[0] Bryant, "Graph-Based Algorithms for Boolean Function Manipulation" in IEEE Transactions on Computers, vol. C-35, no. 8, pp. 677-691, Aug. 1986.
[1] Brace, K.S., Rudell, R.L., Bryant, R.E.: Efficient implementation of a BDD package. In: Proc. of the 27th ACM/IEEE Design Automation Conf. (DAC), pp. 40–45. ACM/IEEE, New York/Piscataway (1990)
[2] Bryant, Randal E. Symbolic Boolean Manipulation with Ordered Binary Decition Diagrams. 1992. ACM Comput. Surv. 24, 3 (September 1992)
[3] Reif Andersen, Henrik. An Introduction to Binary Decition Diagrams. 1999
[4] Bryant, Randal E. Binary Decision Diagrams in Handbook of Model Checking. Springer International Publishing. pp 191-217, 2018