This web-page is the result of my interactions with the SAT/CSP/AI community after I informed them about my early work in the 1970's on clause learning from conflicts.

As Gerry Sussman wrote: "I think that the problem is that the mathematics world is very fragmented, so an idea written up in math journals is usually read by very few people." Back in the 1970's it was common to put a stake in the sand by publishing an abstract in the Notices of the AMS. I should have followed with a longer paper but my paper was rejected from computer science conferences like FOCS and STOC, the community I was in back then.

It is now clear that the CS community does not read mathematics abstracts. It was my fault that I did not publish my paper in an AI conference or journal. However, dissertations and technical reports from ETH Zurich also count as published works.

Here is an email exchange with Ashish Sabharwal, a 1995 PhD from the University of Washington, supervised by Paul Beame and Henry Kautz, who also saw this communication.

Feb 18, 2007 10:29 AM	 
SAT solvers and proof complexity

Hi Ashish:

thank you for your work on proof complexity and SAT solvers. 
Your papers state very clearly the results and I use the 
"harnessing the potential of clause learning" in my
teaching.

Do you agree with the statements in:
http://www.ccs.neu.edu/home/lieber/clause-learning/comparison-to-newer-works.html
? I was working in this area 30 years ago and discovered recently that there
is a lot of activity in "my" space. Please give me feedback on the above page.

===============
From: Ashish Sabharwal ,
Cc: Paul Beame ,
    Henry Kautz 	 
Mar 6, 2007 4:12 PM	 
Re: SAT solvers and proof complexity

Dear Karl,

Thanks for the link to your 1977 paper on superresolution. I read the
paper, and it is indeed interesting work.

From what I understand, your main result relevant to our work is Lemma 3.1
on page 6 in your paper, which states that for every resolution proof R of
a formula, there is a shorter superresolution proof AR. This appears to be
almost a straightforward "observation" for superresolution, and, as you
mention, does match our relatively easy Theorem 2 concerning CL- with
unlimited restarts.

...

Best,
Ashish
==============
Comment by Karl:
I agree with you that my results were quite simple 
(compared to the P-optimal algorithm work I did simultaneously with Ernst Specker).

I needed many restarts because I used fine-grained P-optimal 
heuristics which dynamically influence the best variable ordering.

However, I needed to formalize clause learning back in 1977
so that I could state and prove theorems. Back then, developing
the succinct definition of superresolution was also a contribution.

Here is another example of such a statement:

Famous person 1 agreed: I am not surprised you already used it [clause learning based on conflict analysis] 30 years ago. Many results are "rediscovered" again and again. See e.g. all the work that has already been done in the 80s, early 90s about SAT in *J. Gu, P. W. Purdom, J. Franco, and B. W. Wah, in "Satisfiability Problem: Theory and Applications", DIMACS Series in Discrete Mathematics and Theoretical Computer Science, American Mathematical Society, 1997, pp. 19-152. (reference 348 [Lieberherr/Specker] in the above paper is about the sister technique that we developed after superresolution.)

Famous person 2 disagreed: My interpretation is that your 1977 AMS paper does not address clause learning from conflicts. ... I kindly ask you not to send me further email messages on this subject. I do not want to get involved in further discussions on this issue.

I believe I convinced Famous person 2 that Famous person 1 is right. But I was quite surprised by the defensiveness of Famous person 2.

As part of the argument to convince famous person 2 I wrote: Superresolution and Comparison and Gerald Sussman's view and My PhD Dissertation (1977).

It does not matter who was first but how we can progress the state-of-the-art now (an insight by Gerry Sussman). That is why we wrote a new paper on this topic in 2007 Integrating Superresolution with P-Optimal Algorithms.