Name
Abstract | ||
|---|---|---|
We relate the exponential complexities 2(s(k)n) of k-SAT and the exponential complexity 2(s(Pi 23-SAT)n) of Pi(2)3-SAT (evaluating formulas of the form for all x there exists y phi(x, y) where phi is a 3-CNF in x variables and y variables) and show that s(infinity) (the limit of s(k) as k -> infinity) is at most s(Pi(2)3-SAT). Therefore; if we assume the Strong Exponential-Time Hypothesis, then there is no algorithm for Pi(2)3-SAT running in time 2(cn) with c < 1. On the other hand, a nontrivial exponential-time algorithm for Pi(2)3-SAT would provide a k-SAT solver with better exponent than all current algorithms for sufficiently large k. We also show several syntactic restrictions of Pi(2)3-SAT have nontrivial algorithms, and provide strong evidence that the hardest cases of Pi(2)3-SAT must have a mixture of clauses of two types: one universal literal and two existential literals, or only existential literals. Moreover, the hardest cases must have at least n - o(n) universal variables, and hence only o(n) existential variables. Our proofs involve the construction of efficient minimally unsatisfiable k-cNFs and the application of the Sparsification Lemma. |
Year | DOI | Venue |
|---|---|---|
2013 | 10.1007/978-3-642-17493-3_7 | PARAMETERIZED AND EXACT COMPUTATION |
DocType | Volume | Issue |
Journal | 6478 | 4 |
ISSN | Citations | PageRank |
0302-9743 | 1 | 0.34 |
References | Authors | |
10 | 3 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Chris Calabro | 1 | 140 | 6.13 |
| Russell Impagliazzo | 2 | 5444 | 482.13 |
| Ramamohan Paturi | 3 | 1260 | 92.20 |