Explicit Versus Symbolic Algorithms for Solving ALFP Constraints

ALFP, Alternation-free Least Fixed Point logic, has successfully been used as an intermediate language in the implementation of static analysis and model checking problems. Clearly different analysis problems may give rise to ALFP clauses with different characteristics. There are also different approaches to solving ALFP clauses and some of those are better suited for certain kinds of clauses than others. The aim of this paper is to present two algorithms, one that is based on differential worklists and one based on BDD's, and experiment with them.