Experimental comparison of the two Fredman-Khachiyan-algorithms

We experimentally compare the two algorithms A and B by Fredman and Khachiyan [FK96] for the problem Monet--given two monotone Boolean formulas in DNF and in CNF, decide whether they are equivalent. Currently, algorithm B is the Monet algorithm with the best known worst-case performance. However, there is no experimental evaluation of its practical performance yet, mainly due to the following two reasons. Firstly, implementation of algorithm B is usually considered to be more involved than for algorithm A. Secondly and probably more importantly, there is the assumption that the operations performed by algorithm B to ensure recursion on smaller sub-problems do only pay off theoretically. In this paper, we contrast this assumption by experimentally showing algorithm B to be competitive and even superior to algorithm A on many instances.

• Type: Conference
• Year: 2009
• Where: ALENEX
• Authors: Matthias Hagen, Peter Horatschek, Martin Mundhenk
• Keywords: ALENEX 2007, ALENEX 2009, Algorithm, Monet Algorithm, Monotone Boolean Formulas