Comparing different Boolean unification algorithms

Boolean unification is a procedure to compute the solution of a given Boolean equation or formula. Many problems belonging to very diverse domains have a natural formulation as a Boolean equation, and several methods have been developed in the past for the solution of equations of this type. We compare the relative quality of the solutions that can be obtained with the two classical approaches used to solve Boolean equations, namely, Boole´s (1951) method and Lowenheim´s (1910) method. The implementation of these two solution paradigms features advanced and effective implicit function manipulation primitives implemented with binary decision diagrams (BDDs), which make these solutions applicable to large equations.