The propositional formula checker HeerHugo

HeerHugo is a propositional formula checker that determines whether a given formula is satisfiable or not. Its main ingredient is the branch/merge rule, that is inspired by an algorithm proposed by Staa llmarck, which is protected by a software patent. The algorithm can be interpreted as a breadth first search algorithm. HeerHugo differs substantially from Staa llmarck's algorithm, as it operates on formulas in conjunctive normal form and it is enhanced with many logical rules including unit resolution, 2--satisfiability tests and additional systematic reasoning techniques In this paper, the main elements of the algorithm are discussed, and its remarkable effectiveness is illustrated with some examples and computational results.