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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
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)