Abstract
We give a deterministic #SAT algorithm for de Morgan formulas of size up to n 2.63, which runs in time \(2^{n-n^{\Omega(1)}}\). This improves upon the deterministic #SAT algorithm of [3], which has similar running time but works only for formulas of size less than n 2.5.
Our new algorithm is based on the shrinkage of de Morgan formulas under random restrictions, shown by Paterson and Zwick [12]. We prove a concentrated and constructive version of their shrinkage result. Namely, we give a deterministic polynomial-time algorithm that selects variables in a given de Morgan formula so that, with high probability over the random assignments to the chosen variables, the original formula shrinks in size, when simplified using a deterministic polynomial-time formula-simplification algorithm.
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
Andreev, A.E.: On a method of obtaining more than quadratic effective lower bounds for the complexity of π-schemes. Vestnik Moskovskogo Universiteta. Matematika 42(1), 70–73 (1987); english translation in Moscow University Mathematics Bulletin
Beame, P., Impagliazzo, R., Srinivasan, S.: Approximating AC 0 by small height decision trees and a deterministic algorithm for #AC 0SAT. In: Proceedings of the Twenty-Seventh Annual IEEE Conference on Computational Complexity, pp. 117–125 (2012)
Chen, R., Kabanets, V., Kolokolova, A., Shaltiel, R., Zuckerman, D.: Mining circuit lower bound proofs for meta-algorithms. In: Proceedings of the Twenty-Ninth Annual IEEE Conference on Computational Complexity (2014)
Chen, R., Kabanets, V., Saurabh, N.: An improved deterministic #SAT algorithm for small De Morgan formulas. Electronic Colloquium on Computational Complexity (ECCC)Â 20, 150 (2013)
Håstad, J.: Almost optimal lower bounds for small depth circuits. In: Proceedings of the Eighteenth Annual ACM Symposium on Theory of Computing, pp. 6–20 (1986)
Håstad, J.: The shrinkage exponent of de Morgan formulae is 2. SIAM Journal on Computing 27, 48–64 (1998)
Impagliazzo, R., Matthews, W., Paturi, R.: A satisfiability algorithm for AC0. In: Proceedings of the Twenty-Third Annual ACM-SIAM Symposium on Discrete Algorithms, pp. 961–972 (2012)
Impagliazzo, R., Meka, R., Zuckerman, D.: Pseudorandomness from shrinkage. In: Proceedings of the Fifty-Third Annual IEEE Symposium on Foundations of Computer Science, pp. 111–119 (2012)
Impagliazzo, R., Nisan, N.: The effect of random restrictions on formula size. Random Structures and Algorithms 4(2), 121–134 (1993)
Komargodski, I., Raz, R.: Average-case lower bounds for formula size. In: Proceedings of the Forty-Fifth Annual ACM Symposium on Theory of Computing, pp. 171–180 (2013)
Komargodski, I., Raz, R., Tal, A.: Improved average-case lower bounds for DeMorgan formula size. In: Proceedings of the Fifty-Fourth Annual IEEE Symposium on Foundations of Computer Science, pp. 588–597 (2013)
Paterson, M., Zwick, U.: Shrinkage of de Morgan formulae under restriction. Random Structures and Algorithms 4(2), 135–150 (1993)
Paturi, R., Pudlák, P., Zane, F.: Satisfiability coding lemma. Chicago Journal of Theoretical Computer Science (1999)
Santhanam, R.: Fighting perebor: New and improved algorithms for formula and QBF satisfiability. In: Proceedings of the Fifty-First Annual IEEE Symposium on Foundations of Computer Science, pp. 183–192 (2010)
Seto, K., Tamaki, S.: A satisfiability algorithm and average-case hardness for formulas over the full binary basis. In: Proceedings of the Twenty-Seventh Annual IEEE Conference on Computational Complexity, pp. 107–116 (2012)
Subbotovskaya, B.: Realizations of linear function by formulas using ∨, &,  −. Doklady Akademii Nauk SSSR 136(3), 553–555 (1961); english translation in Soviet Mathematics Doklady
Trevisan, L., Xue, T.: A derandomized switching lemma and an improved derandomization of AC0. In: Proceedings of the Twenty-Eighth Annual IEEE Conference on Computational Complexity, pp. 242–247 (2013)
Williams, R.: Improving exhaustive search implies superpolynomial lower bounds. In: Proceedings of the Forty-Second Annual ACM Symposium on Theory of Computing, pp. 231–240 (2010)
Williams, R.: Non-uniform ACC circuit lower bounds. In: Proceedings of the Twenty-Sixth Annual IEEE Conference on Computational Complexity, pp. 115–125 (2011)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Chen, R., Kabanets, V., Saurabh, N. (2014). An Improved Deterministic #SAT Algorithm for Small De Morgan Formulas. In: Csuhaj-Varjú, E., Dietzfelbinger, M., Ésik, Z. (eds) Mathematical Foundations of Computer Science 2014. MFCS 2014. Lecture Notes in Computer Science, vol 8635. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-44465-8_15
Download citation
DOI: https://doi.org/10.1007/978-3-662-44465-8_15
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-44464-1
Online ISBN: 978-3-662-44465-8
eBook Packages: Computer ScienceComputer Science (R0)