Abstract
We relate the exponential complexities 2s(k)n of \(\textsc {$k$-sat}\) and the exponential complexity \(2^{s(\textsc {eval}(\mathrm {\varPi }_{2} 3\textsc {-cnf}))n}\) of \(\textsc {eval}(\mathrm {\varPi }_{2} 3\textsc {-cnf})\) (the problem of evaluating quantified formulas of the form \(\forall\vec{x} \exists\vec{y} \textsc {F}(\vec {x},\vec{y})\) where F is a 3-cnf in \(\vec{x}\) variables and \(\vec{y}\) variables) and show that s(∞) (the limit of s(k) as k→∞) is at most \(s(\textsc {eval}(\mathrm {\varPi }_{2} 3\textsc {-cnf}))\). Therefore, if we assume the Strong Exponential-Time Hypothesis, then there is no algorithm for \(\textsc {eval}(\mathrm {\varPi }_{2} 3\textsc {-cnf})\) running in time 2cn with c<1. On the other hand, a nontrivial exponential-time algorithm for \(\textsc {eval}(\mathrm {\varPi }_{2} 3\textsc {-cnf})\) would provide a \(\textsc {$k$-sat}\) solver with better exponent than all current algorithms for sufficiently large k. We also show several syntactic restrictions of the evaluation problem \(\textsc {eval}(\mathrm {\varPi }_{2} 3\textsc {-cnf})\) have nontrivial algorithms, and provide strong evidence that the hardest cases of \(\textsc {eval}(\mathrm {\varPi }_{2} 3\textsc {-cnf})\) must have a mixture of clauses of two types: one universally quantified literal and two existentially quantified literals, or only existentially quantified literals. Moreover, the hardest cases must have at least n−o(n) universally quantified variables, and hence only o(n) existentially quantified variables. Our proofs involve the construction of efficient minimally unsatisfiable \(\textsc {$k$-cnf}\)s and the application of the Sparsification lemma.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
References
Aspvall, B., Plass, M.F., Tarjan, R.E.: A linear-time algorithm for testing the truth of certain quantified boolean formulas. Inf. Process. Lett. 8(3), 121–123 (1979)
Kleine Büning, H., Karpinski, M., Flögel, A.: Resolution for quantified boolean formulas. Inf. Comput. 117(1), 12–18 (1995)
Chen, H.: Existentially restricted quantified constraint satisfaction. Inf. Comput. 207(3), 369–388 (2009)
Calabro, C., Impagliazzo, R., Kabanets, V., Paturi, R.: The complexity of unique k-sat: an isolation lemma for k-cnfs. In: Proceedings of the Eighteenth IEEE Conference on Computational Complexity, 386–393 May 2008. Journal of Computer and Systems Sciences, vol. 74, pp. 135–144 (2003). Preliminary version
Calabro, C., Impagliazzo, R., Paturi, R.: A duality between clause width and clause density for sat. In: CCC ’06: Proceedings of the 21st Annual IEEE Conference on Computational Complexity, pp. 252–260. IEEE Computer Society, Washington (2006)
Calabro, C., Impagliazzo, R., Paturi, R.: The complexity of satisfiability of small depth circuits. In: Parameterized and Exact Computation, 4th International Workshop, IWPEC 2009, Copenhagen, Denmark, September 10–11, 2009. Revised Selected Papers, pp. 75–85. Springer, Berlin (2009)
Dantsin, E., Wolpert, A.: An improved upper bound for sat. In: Bacchus, F. (ed.) Lecture Notes in Computer Science, vol. 3569, pp. 400–407. Springer, Berlin (2005)
Timon, H.: 3-sat faster and simpler - unique-sat bounds for PPSZ hold in general. In: Proceedings of the 52nd Annual IEEE Symposium on Foundations of Computer Science, pp. 277–284 (2011)
Impagliazzo, R., Paturi, R.: The complexity of k-sat. In: IEEE Conference on Computational Complexity, vol. 14, pp. 237–240 (1999)
Impagliazzo, R., Paturi, R., Zane, F.: Which problems have strongly exponential complexit? J. Comput. Syst. Sci. 63, 512–530 (1998). Preliminary version In: 39th Annual IEEE Symposium on Foundations of Computer Science, pp. 653–662 (1998)
Iwama, K., Seto, K., Takai, T., Tamaki, S.: Improved randomized algorithms for 3-sat. In: Cheong, O., Chwa, K.-Y., Park, K. (eds.) Algorithms and Computation. Lecture Notes in Computer Science, vol. 6506, pp. 73–84. Springer, Berlin (2010)
Lee, C.: On the size of minimal unsatisfiable formulas. ArXiv E-prints (2008)
Paturi, R., Pudlák, P., Saks, M.E., Zane, F.: An improved exponential-time algorithm for k-sat. J. ACM 52(3), 337–364 (2005). Preliminary version In: 39th Annual IEEE Symposium on Foundations of Computer Science, pp. 628–637 (1998)
Paturi, R., Pudlák, P., Zane, F.: Satisfiability coding lemma. In: Preliminary version in 38th Annual Symposium on Foundations of Computer Science, vol. 566 (1999). 1997
Daniel, R.: Improved bound for the PPSZ/Schöning-algorithm for 3-sat. J. Satisf. Boolean Model. Comput. 1(2), 111–122 (2006)
Schöning, U.: A probabilistic algorithm for k-sat based on limited local search and restart. Algorithmica 32(4), 615–623 (2002)
Schuler, R.: An algorithm for the satisfiability problem of formulas in conjunctive normal form. J. Algorithms 54(1), 40–44 (2005)
Williams, R.: Algorithms for quantified boolean formulas. In: Proceedings of the 13th Annual ACM-SIAM Symposium on Discrete Algorithms, pp. 299–307 (2002)
Acknowledgements
We thank the reviewers for their helpful comments and corrections.
Author information
Authors and Affiliations
Corresponding author
Additional information
R. Impagliazzo research was supported by the Simonyi Fund, the Bell Company Fellowship and the Fund for Math, and NSF grants DMS-083573, CNS-0716790 and CCF-0832797.
R. Paturi research was supported by NSF grant CCF-0947262 from the Division of Computing and Communication Foundations. Any opinions, findings and conclusions or recommendations expressed in this material are those of the authors and do not necessarily reflect the views of the National Science Foundation.
Rights and permissions
About this article
Cite this article
Calabro, C., Impagliazzo, R. & Paturi, R. On the Exact Complexity of Evaluating Quantified k -CNF . Algorithmica 65, 817–827 (2013). https://doi.org/10.1007/s00453-012-9648-0
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s00453-012-9648-0