Informationsverdichtung von Modellen in der Aussagenlogik und das P=NP Problem

Abstract: The thesis deals with the problem of deciding, whether a given formula of the propositional calculus is satisfiable. In the first part, a deduction rule, called Superresolution is introduced and compared with known proof systems and decision procedures. In the second part, probabilistic algorithms for NP-complete languages are investigated.

Note added in 2006: The term "information condensation" or "information compaction" is used in the title, because the thesis conjectures that the extra superresolvents added will positively influence the value ordering in Johnson's fair coin flipping algorithms and in Lieberherr's and Specker's biased coin-flipping algorithms.

In modern terminology (added in 2006): The thesis explores the idea of non-chronological backtracking for satisfiability. An algorithm SR1 is proposed which, based on superresolution, learns new clauses that are added to the CNF. The intuition is that the added clauses will not only help to avoid the same "mistake" but the new clauses will also help MAXMEAN-based algorithms that are based on biased coin flipping to better compute the bias of the coin.