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/.
@PHDTHESIS{karl:thesis,
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.
@ARTICLE{lieber:superresolution,
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:
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
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 ??? (UIP)
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?
@inproceedings{DBLP:conf/sat/BonetLM06,
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}
}
@proceedings{DBLP:conf/sat/2006,
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}
}