Department of Computer Science | Institute of Theoretical Computer Science | CADMO

Prof. Emo Welzl and Prof. Bernd Gärtner

Mittagsseminar Talk Information |

**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)

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: 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