##
Talk Proposal:
The Evergreen Game: The Promise of Polynomials to Boost Boolean MAX-CSP Solvers

Speaker:
Karl Lieberherr, Northeastern University

Abstract:
Alice and Bob play the following MAX-SAT game,
called Evergreen:
Alice and Bob agree on a "type T" of SAT formulae
and on a wager W, say W = 1 million dollars.
The type describes what kind of clauses may be used,
e.g., the type might be T = {!A, A or B}.
A SAT formula is a bag of clauses, i.e., the same clause may be repeated.
Alice gives to Bob a formula F1 of type T and has to pay
to Bob W * the fraction of the clauses that Bob satisfies in F1.
(Example: For the above T, if Alice plays optimally, she will have to pay to Bob only about the
golden ratio (0.618 ...) * W.)
Then Bob gives to Alice a formula F2 of type T and has to pay
to Alice W * the fraction that Alice satisfies in F2.
While Alice is given unlimited resources to do
her moves, Bob has only bounded time available.
How much time does Bob need to guarantee a draw?

While the first impression of Evergreen is that Bob needs
exponential time (it seems that
he has to solve an NP-hard optimization problem, namely MAX-SAT),
the problem can be solved in polynomial time.
We present the search space reduction techniques that
are needed to create this exponential speedup.
A crucial ingredient to playing the game efficiently are polynomials
that serve as abstract representations of formulae.

The technique is applicable to all Boolean MAX-CSP problems of which
MAX-SAT is a special case.
We illustrate the beneficial effect of Evergreen on state-of-the-art MAX-SAT and SAT solvers
by using the Evergreen game playing algorithm as a preprocessor.
For many formalae we tested so far, the preprocessor either
speeds up the MAX-SAT or SAT solvers or produces a better satisfaction
ratio in case of the MAX-SAT solvers. For example, on a formula called
v2000-c8400, the award winning solver yices achieves a satisfaction ratio
of 0.947 after 888 seconds and with Evergreen preprocessing yices
achieves a satisfaction ratio of 1 after 0.03 seconds.
The preprocessing time is negligible because the preprocessing is
linear time.

Joint work with:
Ahmed Abdelmeged and Christine Hang and Daniel Rinehart