Karl Lieberherr Invented Non-Chronological Backtracking at about the same time as Gerry Sussman and Richard Stallman

In the seventies I invented non-chronological backtracking based on clause learning and published a complete proof system called superresolution. Superreolution is a clause learning scheme and I showed that it is polynomially equivalent to general resolution. Discussion of related work that re-invented and improved my early work on non-chronological backtracking and the complexity of proof procedures.

This was my PhD thesis at ETH Zurich in 1977:

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

AUTHOR = "{Karl Lieberherr}",
TITLE  = "Information Condensation of Models in the Propositional Calculus and the P=NP Problem",
SCHOOL = "ETH Zurich",
YEAR   = "1977",
NOTE = "145 pages, in German"

The most accessible paper about superresolution is the following (1977) with an earlier (1975) technical report at ETH Zurich mentioned below.

AUTHOR = "Karl Lieberherr",
TITLE = "Complexity of superresolution",
JOURNAL = "Notices of the American Mathematical Society",
YEAR = 1977,
PAGES = "A-433",
VOLUME = 24,
NOTE = "abstract only, full version on web (see below)"
Here is what is published by AMS in 1977:

KARL LIEBERHERR, SWISS Federal Institute of Technology,
Institute fuer Informatik, CH-8092 Zuerich.
Complexity of Superresolution. Preliminary Report.

A complete proof system, called Superresolution, for
conjunctive normal forms (cnf's) of the propositional calculus is investigated.
Let s be a cnf, L(s) the set of literals of s and I a partial
interpretation of the variables of s, described by a subset of L(s).
k in L(s) is simply determined by I, (I->k), if a clause of s
is unsatisfied under the interpretation I union {k'} or if k in I.
A literal k is determined by I (I=>k), if there are literals
g1,g2,.. gn=k (in L(s)) such that I union {g1, g2,.. gi-1)->gi
for 1 <= i <= n. Let D(I) = {k | k in L(s) and I=>k}.
Define P(E) for E subset L(s) by: E contains a complementary
pair of literals. A clause c is a superresolvent of s,
if for I={k'|k in c} we have !P(D(I)) and there is a variable v with
P(D(I union {v})) and P(D(I union {v'})). Theorem (1) For
each nontrivial Resolution proof there exists a Superresolution 
proof which is shorter (less clauses). (2) No input resolvent of a cnf
(except the empty clause) can be a superresolvent. (3) One
application of Superresolution and its 
checking only need linear time (4)Superresolution and Resolution 
are polynomially equivalent.
Note: (1) A modern DPLL-style proof system with a simple clause learning scheme of negating the decision literals will produce superresolvents (after it produced semi-superresolvents). (2) The full paper introduces a more elaborate conflict-analysis technique to learn minimal superresolvents.

There is an earlier reference to the idea of Superresolution: Institut fuer Informatik, ETHZ Zurich, Technical report 14. This is the same series of reports that disseminated Niklaus Wirth's programming languages Pascal, Modula, Modula-2 and Oberon.

Full 1977 Paper on Superresolution. | Related info.

Notes by Karl:

Clause Learning

Clause learning turns out to be a very important feature of state-of-the-art algorithms (this is written in July 2006) for Satisfiability. The idea of superresolution is to learn from mistakes, i.e., the failure to find a satisfying assignment. Superresolution adds a clause of "minimal" length to the set of clauses so that the same mistake will not happen again later in the search process.

Superresolution is the theoretical foundation for non-chronological backtracking based on learned clauses.

Correspondence between new and old terminology

According to Daniel Le Berre, the current vocabulary about conflict and nogood clauses which is now widely used, is the one defined by Joao Marques Silva in his PhD thesis about GRASP SAT solver:

Marques-Silva, J. P. and Sakallah, K. A. (1996) GRASP: A New Search Algorithm for Satisfiability . In Proceedings of International Conference on Computer-Aided Design, pp. 220-227, Santa Clara, California, U.S.A.

New terminology  		Old terminology used by
Marques-Silva 			Karl Lieberherr		

nogood clause			superresolvent

records reason to		same definition 
avoid making the same 
mistake again

decision level
of variable

decision variable		An element in CHOSEN in algorithm SR0

real decision variable		An element in CH in algorithm SR ?

unique implication point	A learning variable of a superresolvent

make nogood clause 		normal superresolvent
as small as possible

asserting clause		???

Daniel Berre also recommends this paper which uses conflict clauses: Robert Nieuwenhuis, Albert Oliveras and Cesare Tinelli * Solving SAT and SAT Modulo Theories: From an Abstract Davis-Putnam-Logemann-Loveland Procedure to DPLL(T)*. http://www.lsi.upc.es/~roberto/papers/JACM2006revision.pdf

The combination of Max-SAT generalized resolution and algorithm MAXMEAN seems to be very interesting.

Search techniques for constraint satisfaction problems with a finite domain can be made more efficient in two ways: look-ahead techniques (exploit information about the remaining search space) and look-back techniques (exploit information about the search which has already taken place) (See Bayardo/Schrag: Using CSP look-Back Techniques ... 1997). Look-ahead techniques include: variable ordering heuristics, value ordering heuristics and constraint propagation. Look-back techniques include: learning and backjumping.

Superresolution is a look-back technique. The ideas behind MAXMEAN result probably in very useful look-ahead techniques, both for variable ordering and value ordering. MAXMEAN is a look-ahead technique because it looks-ahead over the average of all assignments where k variables are set to true.

How can we generalize Superresolution from SAT to Max-SAT? We cannot rely on propagating unit clauses because for a maximal assignment a unit clause might have to be unsatisfied.

What is the best way to generalize Superresolution from SAT to MaxSAT? We want to give a generalized superresolution proof that shows that in cnf S at most c clauses can be satisfied. We would like the generalized superresolvents to be short.

My 1977 paper is for SAT what the following 2006 paper is for MaxSAT:
Can this be improved?

author    = {Maria Luisa Bonet and 
Jordi Levy and    Felip Many{\`a}},                
title     = {A Complete Calculus for Max-SAT.},
booktitle = {SAT},                   
year      = {2006},                    
pages     = {240-251},                   
ee        = {http://dx.doi.org/10.1007/11814948_24}, 
crossref  = {DBLP:conf/sat/2006},            
bibsource = {DBLP, http://dblp.uni-trier.de}   
editor    = {Armin Biere and
Carla P. Gomes},
title     = {Theory and Applications of Satisfiability Testing - SAT 
2006, 9th International Conference, Seattle, WA, USA, August               
12-15, 2006, Proceedings},                                                 
booktitle = {SAT},                                                         
publisher = {Springer},                                                    
series    = {Lecture Notes in Computer Science},                           
volume    = {4121},                                                        
year      = {2006},                                                        
isbn      = {3-540-37206-7},                                               
bibsource = {DBLP, http://dblp.uni-trier.de}