In the 1970's I worked on two
synergistic technologies, non-chronological backtracking
and, with NSF support,
on P-optimal algorithms for MAX-CSP, that have proven to be useful 
in practical applications.
Regarding non-chronological backtracking, I developed a 
proof system, called super-resolution, and proved
it polynomially equivalent to resolution (a result that
was rediscovered in 2005 in a dissertation from the University
of Washington).
Non-chronological backtracking is now used, together with clever
engineering techniques in all state-of-the-art SAT and MAX-SAT solvers.

P-optimal algorithms for MAX-CSP have recently been shown 
to be useful preprocessors for MAX-SAT solvers.
On large MAX-SAT problems where solvers such as Toolbar or yices
time out, a better assignment is reached with preprocessing.
http://www.ccs.neu.edu/research/demeter/biblio/local-search-eg.html
See also the appendix below.

My vision in the 1970's was that there is an inherent synergy
between clause learning and P-optimal algorithms.
The P-optimal algorithms rely on the type of a CNF and the population
vector associated with the type.
Clause learning changes the population vector of a CNF and our hope is that
the the changed population vector helps the P-optimal algorithm 
to find a better solution.
Of course, the clause learning will eventually reach the
maximum and prove that it is a maximum
but the hope is that the P-optimal 
algorithm finds the optimum solution faster
(without a proof that the maximum has been reached).

We prose to further investigate the interaction between
clause learning and P-optimal algorithms, beyond
using P-optimal algorithms merely as a preprocessor
which already turns out to be useful.

Sakallah et al. have investigated the connection between
MAX-SAT and Maximally Satisfiable Subformulas (MSS) in the context of
hardware verification.
An MSS is a satisfiable subformula so that adding any additional clause
from the formula makes it unsatisfiable.
MSS are closely related to MUS, a dual notion, that is
important in hardware verification.
MUS are used in counterexample-guided abstraction
refinement. The Vapor framework applies counterexample-guided
abstraction to Verilog designs.

We would like to investigate how the P-optimal algorithms,
combined with clause learning,
help to find MSS faster.

Questions we would like to answer are:

Are the satisfiable subformulas found by the P-optimal algorithms
often MSS?

How does clause learning influence whether 
the satisfiable subformulas found by the P-optimal algorithms
are MSS? One would expect that clause learning would
help to produce more MSS.

Recent technical reports we have:
http://www.ccs.neu.edu/research/demeter/biblio/POptMAXCSP.html
http://www.ccs.neu.edu/research/demeter/biblio/evergreen.html

Recent workshop presentation:
http://www.ccs.neu.edu/research/demeter/biblio/local-search-eg.html



References:

@TECHREPORT{sakallah:05,
AUTHOR = "M. Liffiton and Z. Andraus and K. Sakallah",
TITLE = "From MAX-SAT to Min-UNSAT: Insights and Applications",
INSTITUTION = "University of Michigan",
YEAR = 2005,
NUMBER = "CSE-TR-506-05"
}



Appendix:

Preprocessing for MAX-SAT based on P-Optimality
Karl Lieberherr
joint work with Christine Hang and Ahmed Abdelmeged

Every conjunctive normal form (CNF) F has a type T that is determined
by the union of the clause types it contains. A clause type
is a pair, consisting of the length of the clause and the number
of positive literals. For any CNF of type T, there is
an assignment that satisfies a constant fraction f[T]
of the clauses and satisfying strictly more than f[T] is NP-complete
for most types T.

We turn this insight into a preprocessor for MAX-SAT.
Given a CNF F, we determine its type T,
find in linear-time an assignment J that satisfies at least f[T]
and we return the n-mapped
formula F so that the assignment "all zero" corresponds to J.
This results in a new, but equally satisfiable, CNF F' of type T'.
We iterate this process until there is no improvement.

Preliminary experimental results indicate that this preprocessing
helps state-of-the-art MAX-SAT solvers find
best assignments faster or better assignments within a time limit.
MAX-SAT has applications
in hardware verification, reasoning with uncertainty
and computational biology.
~