Abstract
A propositional proof system based on ordered binary decision diagrams (OBDDs) was introduced by Atserias et al. in [3]. Krajíček proved exponential lower bounds for a strong variant of this system using feasible interpolation [14], and Tveretina et al. proved exponential lower bounds for restricted versions of this system for refuting formulas derived from the Pigeonhole Principle [20]. In this paper we prove the first lower bounds for refuting randomly generated unsatisfiable formulas in restricted versions of this OBDD-based proof system. In particular we consider two systems OBDD* and OBDD+; OBDD* is restricted by having a fixed, predetermined variable order for all OBDDs in its refutations, and OBDD+ is restricted by having a fixed order in which the clauses of the input formula must be processed. We show that for some constant ε > 0, with high probability an OBDD* refutation of an unsatisfiable random 3-CNF formula must be of size at least 2εn, and an OBDD+ refutation of an unsatisfiable random 3-XOR formula must be of size at least 2εn.
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.
References
Achlioptas, D.: Random satisfiability. In: Handbook of Satisfiability, pp. 245–270 (2009)
Alekhnovich, M.: Lower bounds for k-DNF resolution on random 3-CNFs. In: Proceedings of the 37th Annual ACM Symposium on Theory of Computing, pp. 251–256 (2005)
Atserias, A., Kolaitis, P.G., Vardi, M.Y.: Constraint propagation as a proof system. In: Wallace, M. (ed.) CP 2004. LNCS, vol. 3258, pp. 77–91. Springer, Heidelberg (2004)
Bollig, B., Wegener, I.: Improving the variable ordering of OBDDs is NP-complete. IEEE Transactions on Computers 45(9), 993–1002 (1996)
Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computing 35, 677–691 (1986)
Chvátal, V., Szémeredi, E.: Many hard examples for resolution. Journal of the ACM 35(4), 759–768 (1988)
Cook, S., Reckhow, R.: The relative efficiency of propositional proof systems. Journal of Symbolic Logic 44, 36–50 (1979)
Dubois, O., Boufkhad, Y., Mandler, J.: Typical random 3-sat formulae and the satisfiability threshold. Tech. Rep (10)003, ECCC (2003)
Dubois, O., Mandler, J.: The 3-XORSAT threshold. In: Proceedings of the 43rd Annual IEEE Symposium on Foundations of Computer Science, pp. 769–778 (2002)
Friedman, L., Xu, Y.: Exponential lower bounds for refuting random formulas using ordered binary decision diagrams. Tech. Rep. TR13-018, Electronic Colloquium on Computational Complexity (2013)
Groote, J.F., Zantema, H.: Resolution and binary decision diagrams cannot simulate each other polynomially. Discrete Applied Mathematics 130, 157–171 (2003)
Hall, P.: On representatives of subsets. J. London Math. Soc. 10, 26–30 (1935)
Huang, J., Darwiche, A.: Toward good elimination ordering for symbolic SAT solving. In: Proceedings of the Sixteenth IEEE Conference on Tools with Artificial Intelligence, pp. 566–573 (2004)
Krajíček, J.: An exponential lower bound for a constraint propagation proof system based on ordered binary decision diagrams. Tech. Rep. (07)007, Electronic Colloquium on Computational Complexity (2007)
Pan, G., Vardi, M.Y.: Search vs. symbolic techniques in satisfiability solving. In: Hoos, H.H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol. 3542, pp. 235–250. Springer, Heidelberg (2005)
Razborov, A.A.: Pseudorandom generators hard for k-DNF resolution and polynomial calculus resolution (2003) (manuscript)
Segerlind, N.: The complexity of propositional proofs. Bulletin of Symbolic Logic 54, 40–44 (2007)
Seiling, D., Wegener, I.: NC-algorithms for operations on binary decision diagrams. Parallel Processing Letters 3(1), 3–12 (1993)
Tveretina, O., Sinz, C., Zantema, H.: An exponential lower bound on OBDD refutations for pigeonhole formulas. In: Athens Colloquium on Algorithms and Complexity. Electronic Proceedings in Theoretical Computer Science (2009)
Tveretina, O., Sinz, C., Zantema, H.: Ordered binary decision diagrams, pigeonhole formulas and beyond. Journal on Satisfiability, Boolean Modeling and Computation 7, 35–38 (2010)
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
Friedman, L., Xu, Y. (2013). Exponential Lower Bounds for Refuting Random Formulas Using Ordered Binary Decision Diagrams. In: Bulatov, A.A., Shur, A.M. (eds) Computer Science – Theory and Applications. CSR 2013. Lecture Notes in Computer Science, vol 7913. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-38536-0_11
Download citation
DOI: https://doi.org/10.1007/978-3-642-38536-0_11
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-38535-3
Online ISBN: 978-3-642-38536-0
eBook Packages: Computer ScienceComputer Science (R0)