Abstract
The usual DPLL algorithm uses splittings (branchings) on single Boolean variables. We consider an extension to allow splitting on linear combinations mod 2, which yields a search tree called a linear splitting tree. We prove that the pigeonhole principle has linear splitting trees of size \(2^{O(n)}\). This is near-optimal since Itsykson and Sokolov [1] proved a \(2^{\varOmega (n)}\) lower bound. It improves on the size \(2^{\varTheta (n \log n)}\) for splitting on single variables; thus the pigeonhole principle has a gap between linear splitting and the usual splitting on single variables. This is of particular interest since the pigeonhole principle is not based on linear constraints. We further prove that the perfect matching principle has splitting trees of size \(2^{O(n)}\).
Research is partially supported by the Government of the Russian Federation under Grant 14.Z50.31.0030.
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
Similar content being viewed by others
References
Itsykson, D., Sokolov, D.: Lower bounds for splittings by linear combinations. In: Csuhaj-Varjú, E., Dietzfelbinger, M., Ésik, Z. (eds.) MFCS 2014, Part II. LNCS, vol. 8635, pp. 372–383. Springer, Heidelberg (2014)
Davis, M., Logemann, G., Loveland, D.: A machine program for theorem-proving. Commun. ACM 5, 394–397 (1962)
Davis, M., Putnam, H.: A computing procedure for quantification theory. J. ACM 7, 201–215 (1960)
Tseitin, G.S.: On the complexity of derivation in the propositional calculus. Zapiski nauchnykh seminarov LOMI 8, 234–259 (1968). English translation of this volume: Consultants Bureau, N.Y., 1970, pp. 115–125
Urquhart, A.: Hard examples for resolution. JACM 34(1), 209–219 (1987)
Alekhnovich, M., Hirsch, E.A., Itsykson, D.: Exponential lower bounds for the running time of DPLL algorithms on satisfiable formulas. J. Autom. Reasoning 35(1–3), 51–72 (2005)
Seto, K., Tamaki, S.: A satisfiability algorithm and average-case hardness for formulas over the full binary basis. In: 2012 IEEE 27th Annual Conference on Computational Complexity (CCC), pp. 107–116, June 2012
Demenkov, E., Kulikov, A.S.: An elementary proof of a 3n-o(n) lower bound on the circuit complexity of affine dispersers. In: Murlak, F., Sankowski, P. (eds.) MFCS 2011. LNCS, vol. 6907, pp. 256–265. Springer, Heidelberg (2011)
Dantchev, S., Riis, S.: Tree resolution proofs of the weak pigeon-hole principle. In: 16th Annual IEEE Conference on Computational Complexity, pp. 69–75 (2001)
Acknowledgements
The work is performed according to the Russian Government Program of Competitive Growth of Kazan Federal University. The author is grateful to Dmitry Itsykson for fruitful discussions and to Sam Buss for valuable advices that improve readability of the paper.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing Switzerland
About this paper
Cite this paper
Oparin, V. (2016). Tight Upper Bound on Splitting by Linear Combinations for Pigeonhole Principle. In: Creignou, N., Le Berre, D. (eds) Theory and Applications of Satisfiability Testing – SAT 2016. SAT 2016. Lecture Notes in Computer Science(), vol 9710. Springer, Cham. https://doi.org/10.1007/978-3-319-40970-2_6
Download citation
DOI: https://doi.org/10.1007/978-3-319-40970-2_6
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-40969-6
Online ISBN: 978-3-319-40970-2
eBook Packages: Computer ScienceComputer Science (R0)