Prof. Emo Welzl and Prof. Bernd Gärtner
|Mittagsseminar Talk Information|
Date and Time: Thursday, June 06, 2013, 12:15 pm
Duration: 30 minutes
Location: OAT S15/S16/S17
Speaker: Timon Hertli
The Exponential Time Hypothesis (ETH) conjectures that algorithms for k-SAT run in time at least 2skn, for sk>0. The Strong ETH furthermore states that sk goes to 1 as k goes to infinity. That is, for large k, brute-force search is close to optimal.
I will present a very recent result by C. Beck and R. Impagliazzo [STOC 13] that gives Strong ETH lower bounds for a large class of SAT algorithms. They showed that k-CNF formulas exist for which regular resolution needs almost 2n steps. Such lower bounds were previously only known for the weaker tree-like resolution. They also give a (3/2)n lower bound for full resolution.
The construction is based on a random system of linear equations over a finite field GF(p). This system is converted into a k-CNF, where each variable in GF(p) corresponds to the sum of Θ(p) Boolean variables. Using expansion properties of the equations, the claimed lower bound is first shown for tree-like resolution and then for regular resolution.
Automatic MiSe System Software Version 1.4803M | admin login