×

The propositional formula checker HeerHugo. (English) Zbl 0968.68148

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.

MSC:

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)

Software:

HeerHugo
PDFBibTeX XMLCite
Full Text: DOI