We present a new method for finding closed forms of recursive Boolean function definitions. Traditionally, these closed forms are found by iteratively approximating until a fixed point is reached. Conceptually, our new method replaces each k-ary function by 2k Boolean variables defined by mutual recursion. The introduction of an exponential number of variables is mitigated by the simplicity of their definitions and by the use of a novel variant of ROBDDs to avoid repeated computation. Experimental evaluation suggests that this approach is significantly faster than Kleene iteration for examples that would require many Kleene iteration steps.
Cite as: Herlihy, B., Schachte, P. and Sondergaard, H. (2006). Boolean equation solving as graph traversal. In Proc. Twelfth Computing: The Australasian Theory Symposium (CATS2006), Hobart, Australia. CRPIT, 51. Gudmundsson, J. and Jay, B., Eds. ACS. 123-132.
(from crpit.com)
(local if available)