I want to emphasize the pairs [Paturi etal, 1998] --> [Iwama, Tamaki, 2003] and [Dantsin etal, 2002] --> [Brueggemann, Kern, 2004]. Each paper can be chosen individually, but the arrows indicate dependencies. So if you want to work out topics in pairs, this would be an ideal option, which we support. The four papers above should lead us, based on the course, to the currently best known bounds for k-SAT.
The list is not meant to be exclusive. If you find another paper in the area that you would like to present, please propose.
Please respect the copyright of original journal files I have provided below.
gone := topic already taken.
gone [Alt etal, 1996]
Helmut Alt, Leonidas J. Guibas, Kurt Mehlhorn,
Richard M. Karp, Avi Widgerson
A method for obtaining randomized algorithms with small tail probabilities
ALGOR{16:4-5}{1996}{543}{547}
The idea of restarts for randomized algorithms is discussed
here on an abstract level. This is nothing particular to SAT,
but since it was an issue in the SAT course, it may be interesting to
see, and it should be well presentable.
[Ben-Sasson, Widgerson, 2001]
Eli Ben-Sasson, Avi Widgerson
Short proofs are narrow --- resolution made simple
pdf
JACM{48:2}{2001}{149}{169}
Gives simple proofs for exponential lower bounds on the
size of resolution proofs. A key concept is the width of a
resolution proof that is defined as the maximal size of
a clause occurring in the proof. This width is related to the
length of proofs, and leads to simpler proofs and new results.
[Brueggemann, Kern, 2004]
Tobias Brueggemann, Walter Kern
An improved local search algorithm for 3-SAT
pdf
The story goes on. The deterministic bound for 3-SAT
is improved to O(1.473).
[Dantsin etal, 2002]
Evgeny Dantsin, Andreas Goerdt, Edward A. Hirsch,
R. Kannan, J. Kleinberg,
Christos H. Papadimitriou, Uwe Schöning
A deterministic (2-2/(k+1))^n algorithm for k-SAT based on
local search
pdf
TCS{289:1}{2002}{69}{83}
Was done in the course, except for the tailored improvement
to O(1.481^n) (from O(1.5^n)) for 3-SAT, but see [Brueggemann, Kern, 2004].
[Dantsin, Wolpert, 2004]
Evgeny Dantsin, Alexander Wolpert
Derandomization of Schuler's Algorithm for SAT
pdf
ECCC{11}{1004}{}
[Schuler, 2005] presented a randomized algorithm that
solves SAT in expected time at most 2^{n(1-1/log_2(2m))} up to
a polynomial factor, where n and m are, respectively, the
number of variables and the number of clauses in the input formula.
This bound is the best known upper bound for testing satisfiability
of formulas in CNF with no restriction on clause length (for the case
when m is not too large comparing to n). This paper derandomizes this
algorithm using deterministic k-SAT algorithms based on search
in Hamming balls, and proves that the deterministic algorithm
has the same upper bound on the running time as Schuler's
randomized algorithm.
[Dantsin etal, 2004]
Evgeny Dantsin, Edward A. Hirsch, Alexander Wolpert
Algorithms for SAt based on search in Hamming balls
pdf
manuscript (2004)
This is a paper on general SAT (in CNF with no bound on the
clause size) in the spirit of [Schuler, 2005], actually with a
worse bound than there, but with a different idea.
[Formann, Wagner, 1991]
Michael Formann. Frank Wagner
A packing problem with applications to lettering of maps
pdf
SoCG{7th}{1991}{281}{288}
This is a nice application of 2-SAT to an approximation
algorithm for map labeling.
[Hofmeister, 2003]
Thomas Hofmeister
An approximation algorithm for MAX-2-SAT with cardinality constraints
pdf
ESA{11th}{2832}{2003}{301}{312}
[Hoos, Stützle, 2005]
Holger H. Hoos, Thomas Stützle
Stochastic Local Search --- Foundations and Algorithms
Elsevier, Amsterdam (2005) (the book is available in Franziska Hefti's office,
IFW B49.1)
This is a book about randomized local search techniques,
and it refers a lot to SAT as a running application example.
So one could go through it and collect ideas, problems, and
solutions relevant to SAT.
[Iwama, Tamaki, 2003]
Kazuo Iwama, Suguru Tamaki
Improved upper bounds for 3-SAT
pdf
ECCC{53}{2003}{3}
Decribes the currently best bound of O(1.3324^n) for a randomized algorithm
for 3-SAT (and also the best bound for 4-SAT). It is a combination
of Schöning's algorithm with [Paturi etal, 1998].
gone [Král', 2003]
Daniel Král'
Locally satisfiable formulas
ps
Proceedings of the 15th annual ACM-SIAM symposium on Discrete
algorithms (SODA)
(2004) 330-339.
[Paturi etal, 1998]
Ramamohan Paturi, Pavel Pudlák, Michael E. Saks, Francis Zane
An improved exponential-time algorithm for k-SAT,
FOCS{39th}{1998}{628}{637}
This gives the best bound for k-SAT, k>4, and it is
a vital ingredient for the best bounds for 3- and 4-SAT.
That's a challenging one, but we have to see it and
understand it to the extent possible. Also, the
part necessary for [Iwama, Tamaki, 2003] is somewhat more
accessible.
[Schuler, 2005]
Rainer Schuler
An algorithm for the satisfiability problem of formulas
in conjuntive normal form
pdf
Journal of Algorithms, 54:1 (2005) 40-44
gone [Trevisan, 2004]
Luca Trevisan
On Local Versus Global Satisfiability
ps
SIAM Journal on Discrete Mathematics, 17:4 (2004)541-547.
[Paturi etal, 1998] --> [Iwama, Tamaki, 2003]
[Schuler, 2005] --> [Dantsin, Wolpert, 2004]
[Dantsin etal, 2002] --> [Brueggemann, Kern, 2004]