Abstract
The exponential complexity of the satisfiability problem for a given class of Boolean circuits is defined to be the infimum of constants α such that the problem can be solved in time poly(m) 2αn, where m is the circuit size and n is the number of input variables [IP01]. We consider satisfiability of linear Boolean formula over the full binary basis and we show that the corresponding exponential complexities are “interwoven” with those of k-\(\textsf{CNF} \; \textsf{SAT}\) in the following sense. For any constant c, let f c be the exponential complexity of the satisfiability problem for Boolean formulas of size at most cn. Similarly, let s k be the exponential complexity of k-\(\textsf{CNF} \; \textsf{SAT}\). We prove that for any c, there exists a k such that f c ≤ s k . Since the Sparsification Lemma [IPZ01] implies that for any k, there exists a c such that s k ≤ f c , we have sup c {f c } = sup k {s k }. (In fact, we prove this equality for a larger class of linear-size circuits that includes Boolean formulas.) Our work is partly motivated by two recent results. The first one is about a similar “interweaving” between linear-size circuits of constant depth and k-CNFs [SS12]. The second one is that satisfiability of linear-size Boolean formulas can be tested exponentially faster than in O(2n) time [San10, ST12].
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
References
Bodlaender, H.L., Fellows, M.R., Thilikos, D.M.: Derivation of algorithms for cutwidth and related graph layout parameters. Journal of Computer and System Sciences 75(4), 231–244 (2009)
Cygan, M., Dell, H., Lokshtanov, D., Marx, D., Nederlof, J., Okamoto, Y., Paturi, R., Saurabh, S., Wahlström, M.: On problems as hard as CNF-Sat. In: Proceedings of the 27th Annual IEEE Conference on Computational Complexity, CCC 2012, pp. 74–84. IEEE Computer Society (2012)
Calabro, C., Impagliazzo, R., Paturi, R.: The complexity of satisfiability of small depth circuits. In: Chen, J., Fomin, F.V. (eds.) IWPEC 2009. LNCS, vol. 5917, pp. 75–85. Springer, Heidelberg (2009)
Calabro, C., Paturi, R.: k-SAT is no harder than Decision-Unique-k-SAT. In: Frid, A., Morozov, A., Rybalchenko, A., Wagner, K.W. (eds.) CSR 2009. LNCS, vol. 5675, pp. 59–70. Springer, Heidelberg (2009)
Dantsin, E., Hirsch, E.A.: Worst-case upper bounds. In: Handbook of Satisfiability, ch.12, pp. 403–424. IOS Press (2009)
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)
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 (2010)
Pudlák, P.: The length of proofs. In: Buss, S.R. (ed.) Handbook of Proof Theory, pp. 547–637. Elsevier (1998)
Santhanam, R.: Fighting perebor: New and improved algorithms for formula and QBF satisfiability. In: Proceedings of the 51st Annual IEEE Symposium on Foundations of Computer Science, FOCS 2010, pp. 183–192 (2010)
Santhanam, R., Srinivasan, S.: On the Limits of Sparsification. In: Czumaj, A., Mehlhorn, K., Pitts, A., Wattenhofer, R. (eds.) ICALP 2012, Part I. LNCS, vol. 7391, pp. 774–785. Springer, Heidelberg (2012)
Seto, K., Tamaki, S.: A satisfiability algorithm and average-case hardness for formulas over the full binary basis. In: Proceedings of the 27th Annual IEEE Conference on Computational Complexity, CCC 2012, pp. 107–116. IEEE Computer Society (2012)
Tseitin, G.S.: On the complexity of derivation in propositional calculus. In: Slisenko, A.O. (ed.) Studies in Constructive Mathematics and Mathematical Logic, Part II, pp. 115–125 (1968) (in Russian); Reprinted in: Siekmann, J., Wrightson, G. (eds.): Automation of Reasoning 2: Classical Papers on Computational Logic 1967-1970, pp. 466–483. Springer (1983)
Vollmer, H.: Introduction to Circuit Complexity: A Uniform Approach. Springer (1999)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Dantsin, E., Wolpert, A. (2013). Exponential Complexity of Satisfiability Testing for Linear-Size Boolean Formulas. In: Spirakis, P.G., Serna, M. (eds) Algorithms and Complexity. CIAC 2013. Lecture Notes in Computer Science, vol 7878. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-38233-8_10
Download citation
DOI: https://doi.org/10.1007/978-3-642-38233-8_10
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-38232-1
Online ISBN: 978-3-642-38233-8
eBook Packages: Computer ScienceComputer Science (R0)