Groote, Jan Friso; Warners, Joost P. The propositional formula checker HeerHugo. (English) Zbl 0968.68148 J. Autom. Reasoning 24, No. 1-2, 101-125 (2000). Summary: HeerHugo is a propositional formula checker that determines whether a given formula is satisfiable or not. The underlying algorithm is based on a specific breadth-first search procedure, with several enhancements including unit resolution and 2-satisfiability tests. Its main ingredient is the branch/merge rule inspired by an algorithm proposed by Stållmarck, which is protected by a software patent. In this paper, the main elements of the algorithm are discussed, and its remarkable effectiveness is illustrated with some examples and computational results. Cited in 9 Documents MSC: 68T15 Theorem proving (deduction, resolution, etc.) (MSC2010) Keywords:HeerHugo; propositional formula checker Software:HeerHugo PDFBibTeX XMLCite \textit{J. F. Groote} and \textit{J. P. Warners}, J. Autom. Reasoning 24, No. 1--2, 101--125 (2000; Zbl 0968.68148) Full Text: DOI