Abstract
Itsykson and Sokolov in 2014 introduced the class of \(\mathrm {DPLL}(\oplus )\) algorithms that solve Boolean satisfiability problem using the splitting by linear combinations of variables modulo 2. This class extends the class of \(\mathrm {DPLL}\) algorithms that split by variables. \(\mathrm {DPLL}(\oplus )\) algorithms solve in polynomial time systems of linear equations modulo 2 that are hard for \(\mathrm {DPLL}\), \(\mathrm {PPSZ}\) and \(\mathrm {CDCL}\) algorithms. Itsykson and Sokolov have proved first exponential lower bounds for \(\mathrm {DPLL}(\oplus )\) algorithms on unsatisfiable formulas.
In this paper we consider a subclass of \(\mathrm {DPLL}(\oplus )\) algorithms that arbitrary choose a linear form for splitting and randomly (with equal probabilities) choose a value to investigate first; we call such algorithms drunken \(\mathrm {DPLL}(\oplus )\). We give a construction of a family of satisfiable CNF formulas \(\varPsi _n\) of size \(\mathrm {poly}(n)\) such that any drunken \(\mathrm {DPLL}(\oplus )\) algorithm with probability at least \(1 - 2^{-\varOmega (n)}\) runs at least \(2^{\varOmega (n)}\) steps on \(\varPsi _n\); thus we solve an open question stated in the paper [12]. This lower bound extends the result of Alekhnovich, Hirsch and Itsykson [1] from drunken \(\mathrm {DPLL}\) to drunken \(\mathrm {DPLL}(\oplus )\).
The research is partially supported by the Government of the Russia (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
Alekhnovich, M., Hirsch, E.A., Itsykson, D.: Exponential lower bounds for the running time of DPLL algorithms on satisfiable formulas. J. Autom. Reason. 35(1–3), 51–72 (2005)
Ben-Sasson, E.: Hard examples for bounded depth frege. In: Proceedings of the Thiry-Fourth Annual ACM Symposium on Theory of Computing, pp. 563–572. ACM (2002)
Beame, P., Kautz, H.A., Sabharwal, A.: Towards understanding and harnessing the potential of clause learning. J. Artif. Intell. Res. (JAIR) 22, 319–351 (2004)
Beame, P., Pitassi, T.: An exponential separation between the parity principle and the pigeonhole principle. Ann. Pure Appl. Logic 80(3), 195–228 (1996)
Cook, J., Etesami, O., Miller, R., Trevisan, L.: Goldreich’s one-way function candidate and myopic backtracking algorithms. In: Reingold, O. (ed.) TCC 2009. LNCS, vol. 5444, pp. 521–538. Springer, Heidelberg (2009). doi:10.1007/978-3-642-00457-5_31
Dantchev, S.S., Riis, S.: Tree resolution proofs of the weak pigeon-hole principle. In: Proceedings of the 16th Annual IEEE Conference on Computational Complexity, Chicago, Illinois, USA, pp. 69–75. IEEE Computer Society, 18–21 June 2001
Davis, M., Logemann, G., Loveland, D.W.: A machine program for theorem-proving. Commun. ACM 5(7), 394–397 (1962)
Davis, M., Putnam, H.: A computing procedure for quantification theory. J. ACM 7(3), 201–215 (1960)
Garlík, M., Kołodziejczyk, L.A.: Some subsystems of constant-depth Frege with parity (2017, Preprint)
Itsykson, D.: Lower bound on average-case complexity of inversion of Goldreich’s function by drunken backtracking algorithms. Theor. Comput. Syst. 54(2), 261–276 (2014)
Itsykson, D., Sokolov, D.: The complexity of inverting explicit Goldreich’s function by DPLL algorithms. J. Math. Sci. 188(1), 47–58 (2013)
Itsykson, D., Sokolov, D.: Lower bounds for splittings by linear combinations. In: Csuhaj-Varjú, E., Dietzfelbinger, M., Ésik, Z. (eds.) MFCS 2014. LNCS, vol. 8635, pp. 372–383. Springer, Heidelberg (2014). doi:10.1007/978-3-662-44465-8_32
Krajiček, J.: Randomized feasible interpolation and monotone circuits with a local oracle. CoRR, abs/1611.0 (2016)
Oparin, V.: Tight upper bound on splitting by linear combinations for pigeonhole principle. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 77–84. Springer, Cham (2016). doi:10.1007/978-3-319-40970-2_6
Pudlák, P., Impagliazzo, R.: A lower bound for DLL algorithms for k-SAT (preliminary version). In: Proceedings of the Eleventh Annual ACM-SIAM Symposium on Discrete Algorithms, San Francisco, CA, USA, pp. 128–136, 9–11 January 2000
Pudlák, P., Scheder, D., Talebanfard, N.: Tighter Hard Instances for PPSZ. CoRR, abs/1611.0 (2016)
Razborov, A.A.: Resolution lower bounds for perfect matching principles. J. Comput. Syst. Sci. 69(1), 3–27 (2004)
Scheder, D., Tang, B., Chen, S., Talebanfard, N.: Exponential Lower Bounds for the PPSZ k-SAT Algorithm. In: Khanna, S. (ed.) Proceedings of the Twenty-Fourth Annual ACM-SIAM Symposium on Discrete Algorithms, SODA 2013, New Orleans, Louisiana, USA, pp. 1253–1263. SIAM, 6–8 January 2013
Urquhart, A.: Hard examples for resolution. J. ACM 34(1), 209–219 (1987)
Acknowledgements
The authors are grateful to Dmitry Sokolov for fruitful discussions.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this paper
Cite this paper
Itsykson, D., Knop, A. (2017). Hard Satisfiable Formulas for Splittings by Linear Combinations. In: Gaspers, S., Walsh, T. (eds) Theory and Applications of Satisfiability Testing – SAT 2017. SAT 2017. Lecture Notes in Computer Science(), vol 10491. Springer, Cham. https://doi.org/10.1007/978-3-319-66263-3_4
Download citation
DOI: https://doi.org/10.1007/978-3-319-66263-3_4
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-66262-6
Online ISBN: 978-3-319-66263-3
eBook Packages: Computer ScienceComputer Science (R0)