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