First paper on Clause Learning and Non-Chronological Backtracking

@TechReport{lieber:resolution,
AUTHOR = "Karl Lieberherr",
TITLE = " Toward Feasible Solutions of NP-Complete Problems",
INSTITUTION = "ETH Zurich, Institut fuer Informatik",
YEAR = 1975,
MONTH = "September",
NUMBER = "14"
}

Paper. | Related info.

Notes by Karl:

Clause Learning and Approximation Algorithms

Clause learning turns out to be a very important feature of state-of-the-art algorithms (this is written in November 2006) for Satisfiability. The idea of this paper is to combine Johnson's algorithm for approximating MaxSAT with a learning algorithm based on resolution. The result is a complete algorithm Rj [R for Resolution and j for Johnson] that either finds a satisfying assignment or that provides a resolution proof that there is none. For satisfiable formulas, there is a synergistic interaction between the approximation and the learning algorithm: The learning algorithm adds new clauses that influence the behavior of the approximation algorithm helping it to find better approximations.

The quality of an algorithm like Rj is based on the quality of the approximation algorithm and the quality of the learning algorithm. The approximation algorithm should be P-optimal and based on an optimally biased coin. Johnson's algorithm uses a derandomized version of a fair coin (which is P-optimal only for special cases). The work by Lieberherr and Specker on Generalized Satisfiability (or discrete, uniform Constraint Satisfaction) uses optimally biased coins instead which are guaranteed to satisfy a P-optimal fraction. The quality of the learning algorithm is measured by the effectiveness of the clauses learned. Effectiveness is influenced both by the length of the learned clauses and by how often they are used in future steps of the non-chronological backtracking.

For an improved version of this work, see: SuperResolution. 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.

Karl Lieberherr