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

My 1977 ETH Dissertation at http://e-collection.ethbib.ethz.ch/.

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.

Karl Lieberherr's 1977 ETH Zurich Dissertation (the first 48 pages)

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 P-optimal algorithms for the Generalized Satisfiability problem.

In modern terminology (added in 2006): The thesis explores the idea of non-chronological backtracking for satisfiability. An algorithms are proposed and analyzed which, based on superresolution, learn 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.

The algorithm SR introduced in the dissertation gives a specific operational strategy for deriving superesolvents and resolvents. While superresolution has a very general definition, the thesis explores several limited forms of superresolution. The dissertation also introduces the concept of an implication graph. The concept of an implication graph actually came first, followed by an abstraction into a pure proof system that is free from too many algorithmic details.

Because the following relatively recent paper is exploring the same space as my dissertation, I will refer to this paper by using the phrase "SAT community".

@ARTICLE{beame04understanding,
author = "P. Beame and H. Kautz and A. Sabharwal",
title = "Towards Understanding and Harnessing the Potential of Clause Learning",
JOURNAL = "Journal of Artificial Intelligence Research",
YEAR = 2004,
PAGES = "319-351",
VOLUME = 31,
url = "citeseer.ist.psu.edu/beame03understanding.html" }

This paper contains several new results that are not covered in my dissertation. One important category of results in the paper concerns clause learning without restarts while we only deal with restarts. It is fair to say that superresolution subsumes what is now considered clause learning with restarts. Superresolution, as discussed in the dissertation only, includes also the concept of implication graph for conflict analysis.

In the following I give some Selective translations to make it easier for English readers to follow the German text. The English papers that have been published on this topic have not gone to the same level of detail as my dissertation. I assume that the readers has read those English papers available from: http://www.ccs.neu.edu/research/demeter/papers/publications.html

page 25: Algorithm SR uses a procedure SETZEB(l, UEBRIG, WIDERSPRUCH)

SETZEB records its processing in a data structure WALD (forest). WALD is later used to construct the superresolvent.

SETZEB sets the literal l to true and literals forced by unit propagation are also set and stored in the partial assignment I. When a uniquely determined literal is found, SETZEB extends WALD[l] with a new edge. As the label of this edge we set the set of literals clause that determined the uniquely determined literal.

The WALD datastructure corresponds to the implication graph concept used now by the SAT community.

Page 37: 1.3 The connection between SR and Superresolution: The claim is that SR generates only a subset of all possible superresolvents.

Page 38: Introduces the concept of a superresolvent with foreign literals. A literal in a superresolvent is foreign, if the clause with the literal deleted is still a superresolvent plus a second condition.

Page 39: the notion of a technically minimal superresolvent is introduced. It must not contain foreign literals, be independent and maximally shortened. "independent" and "maximally shortened" are introduced later.

Page 40: 1.4 The connection between Resolution and Superresolution.

Lemma 1.4.1 : Each superresolvent generated by SR is the result of a sequence of Resolution steps. This shows that Superresolution is polynomially reducible to Resolution. This result has been discovered independently by the SAT community.

Page 47: 1.6 Resolution can be shortened to superresolution. This result was also discovered independently by the SAT community.

The first 48 pages show that algorithm SR constructs a conflict graph and uses it to build superresolvents in an "intelligent" way. Some of that intelligence is in later pages.