For my PhD work I was interested in the satisfiability problem. I studied a search algorithm that added superresolvents to the clauses to prevent the same "mistake" in a future iteration of the algorithm. Initially, a superresolvent involved the complement of all the decision variables. Several refined forms of superresolvents were proposed; the focus was on minimizing them because shorter clauses lead to faster search.

My 1977 ETH Dissertation at http://e-collection.ethbib.ethz.ch/. | My 1977 ETH Dissertation (local copy).

Superresolution and its many variants are an early form of non-chronological backtracking based on learned clauses which has become a key feature of most state-of-the-art SAT solvers. The above link contains more references to my work in this area in the 1970s.

A new paper on this topic in 2007 Integrating Superresolution with P-Optimal Algorithms.

To be done (2008), suggested by Pete Manolios: I went back to my dissertation (in German) and a related technical report (in English) about non-chronological backtracking and found the following ideas about "minimizing" superresolvents. In the technical report http://www.ccs.neu.edu/home/lieber/clause-learning/karl-complexity-superresolution.pdf I published the idea of normal superresolvent which creates shorter superresolvents. On page 39 of my dissertation, I introduce the concept of minimality of a superrresolvent. A superresolvent is minimal if it is not polluted, independent and shortend. I need to describe those ideas in English and compare them to the GRASP ideas.

A start is here: SuperResolution.

Kar Lieberherr, Fall 2008