Abstract
It is common to classify satisfiability problems by their time complexity. We consider another complexity measure, namely the length of certificates (witnesses). Our results show that there is a similarity between these two types of complexity if we deal with certificates verifiable in subexponential time. In particular, the well-known result by Impagliazzo and Paturi [IP01] on the dependence of the time complexity of \(k\mbox{\tt-}\mathtt{SAT}\) on k has its counterpart for the certificate complexity: we show that, assuming the exponential time hypothesis (ETH), the certificate complexity of \(k\mbox{\tt-}\mathtt{SAT}\) increases infinitely often as k grows. Another example of time-complexity results that can be translated into the certificate-complexity setting is the results of [CIP06] on the relationship between the complexity of \(k\mbox{\tt-}\mathtt{SAT}\) and the complexity of SAT restricted to formulas of constant clause density. We also consider the certificate complexity of CircuitSAT and observe that if CircuitSAT has subexponential-time verifiable certificates of length cn, where cā<ā1 is a constant and n is the number of inputs, then an unlikely collapse happens (in particular, ETH fails).
Nominated as Best Paper candidate.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Calabro, C., Impagliazzo, R., Paturi, R.: A duality between clause width and clause density for SAT. In: Proceedings of the 21st Annual IEEE Conference on Computational Complexity, CCC 2006, pp. 252ā260. IEEE Computer Society, Los Alamitos (2006)
Dantsin, E., Goerdt, A., Hirsch, E.A., Kannan, R., Kleinberg, J., Papadimitriou, C.H., Raghavan, P., Schƶning, U.: A deterministic (2 ā 2/(k + 1))n algorithm for k-SAT based on local search. Theoretical Computer ScienceĀ 289(1), 69ā83 (2002)
Dantsin, E., Hirsch, E.A.: Worst-case upper bounds. In: Handbook of Satisfiability, ch. 12, pp. 403ā424. IOS Press, Amsterdam (2009)
Flum, J., Grohe, M.: Parameterized Complexity Theory. Texts in Theoretical Computer Science. An EATCS Series. Springer, Heidelberg (2006)
Impagliazzo, R., Paturi, R.: On the complexity of k-SAT. Journal of Computer and System SciencesĀ 62(2), 367ā375 (2001)
Impagliazzo, R., Paturi, R., Zane, F.: Which problems have strongly exponential complexity. Journal of Computer and System SciencesĀ 63(4), 512ā530 (2001)
Knuth, D.E.: Generating All Combinations and Partitions. The Art of Computer Programming, fascicleĀ 3, vol.Ā 4, pp. 1ā6. Addison-Wesley, Reading (2005)
Moser, R.A., Scheder, D.: A full derandomization of Schƶningās k-SAT algorithm. In: Proceedings of the 43rd Annual ACM Symposium on Theory of Computing, STOC 2011. ACM, New York (2011) (to appear)
Paturi, R., PudlĆ”k, P.: On the complexity of circuit satisfiability. In: Proceedings of the 42nd Annual ACM Symposium on Theory of Computing, STOC 2010, pp. 241ā250. ACM, New York (2010)
Paturi, R., PudlĆ”k, P., Saks, M.E., Zane, F.: An improved exponential-time algorithm for k-SAT. In: Proceedings of the 39th Annual IEEE Symposium on Foundations of Computer Science, FOCS 1998, pp. 628ā637 (1998)
Paturi, R., PudlĆ”k, P., Zane, F.: Satisfiability coding lemma. In: Proceedings of the 38th Annual IEEE Symposium on Foundations of Computer Science, FOCS 1997, pp. 566ā574 (1997)
Schƶning, U.: A probabilistic algorithm for k-SAT and constraint satisfaction problems. In: Proceedings of the 40th Annual IEEE Symposium on Foundations of Computer Science, FOCS 1999, pp. 410ā414 (1999)
Schuler, R.: An algorithm for the satisfiability problem of formulas in conjunctive normal form. Journal of AlgorithmsĀ 54(1), 40ā44 (2005)
Williams, R.: Improving exhaustive search implies superpolynomial lower bounds. In: Proceedings of the 42nd Annual ACM Symposium on Theory of Computing, STOC 2010, pp. 231ā240. ACM, New York (2010)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
Ā© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Dantsin, E., Hirsch, E.A. (2011). Satisfiability Certificates Verifiable in Subexponential Time. In: Sakallah, K.A., Simon, L. (eds) Theory and Applications of Satisfiability Testing - SAT 2011. SAT 2011. Lecture Notes in Computer Science, vol 6695. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-21581-0_4
Download citation
DOI: https://doi.org/10.1007/978-3-642-21581-0_4
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-21580-3
Online ISBN: 978-3-642-21581-0
eBook Packages: Computer ScienceComputer Science (R0)