Mittagsseminar (in cooperation with A. Steger, D. Steurer and B. Sudakov)

Date and Time: Wednesday, July 18, 2007, 12:15 pm

Duration: This information is not available in the database

Location: OAT S15/S16/S17

Speaker: Karl Lieberherr (Northeastern Univ., Boston)

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

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.

Upcoming talks     |     All previous talks     |     Talks by speaker     |     Upcoming talks in iCal format (beta version!)

Previous talks by year:   2024  2023  2022  2021  2020  2019  2018  2017  2016  2015  2014  2013  2012  2011  2010  2009  2008  2007  2006  2005  2004  2003  2002  2001  2000  1999  1998  1997  1996  

Information for students and suggested topics for student talks

Automatic MiSe System Software Version 1.4803M   |   admin login