Abstract
The splitting method is one of the most powerful and well-studied approaches for solving various NP-hard problems. The main idea of this method is to split an input instance of a problem into several simpler instances (further simplified by certain simplification rules), such that when the solution for each of them is found, one can construct the solution for the initial instance in polynomial time. There exists a huge number of articles describing algorithms of this type and usually a considerable part of such an article is devoted to case analysis. In this paper we show how it is possible to write a program that given simplification rules would automatically generate a proof of an upper bound on the running time of a splitting algorithm that uses these rules. As an example we report the results of experiments with such a program for the SAT, MAXSAT, and (n,3)-MAXSAT (the MAXSAT problem for the case where every variable in the formula appears at most three times) problems.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Byskov, J.M., Madsen, B.A., Skjernaa, B.: New Algorithms for Exact Satisfiability. Theoretical Computer Science Preprint (2003)
Bansal, N., Raman, V.: Upper Bounds for MaxSat: Further Improved. In: Aggarwal, A.K., Pandu Rangan, C. (eds.) ISAAC 1999. LNCS, vol. 1741, pp. 247–258. Springer, Heidelberg (1999)
Chen, J., Kanj, I.: Improved exact algorithms for MAX-SAT. In: Rajsbaum, S. (ed.) LATIN 2002. LNCS, vol. 2286, pp. 341–355. Springer, Heidelberg (2002)
Dantsin, E., Hirsch, E.A., Ivanov, S., Vsemirnov, M.: Algorithms for SAT and Upper Bounds on Their Complexity. ECCC Technical Report 01-012 (2001), Electronic address: ftp://ftp.eccc.unitrier.de/pub/eccc/reports/2001/TR01-012/index.html , A Russian version appears in Zapiski Nauchnykh Seminarov POMI, 277, pp. 14–46 (2001)
Davis, M., Logemann, G., Loveland, D.: A machine program for theoremproving. Comm. ACM 5, 394–397 (1962)
Fedin, S.S., Kulikov, A.S.: A 2|E|/4-time Algorithm for MAX-CUT. Zapiski nauchnykh seminarov POMI 293, 129–138 (2002), English translation is to appear in Journal of Mathematical Sciences
Gramm, J., Guo, J., Hüffner, F., Niedermeier, R.: Automated Generation of Search Tree Algorithms for Hard GraphModification Problems. In: Proceedings of 11th Annual European Symposium on Algorithms, pp. 642–653 (2003)
Gramm, J., Hirsch, E.A., Niedermeier, R., Rossmanith, P.: New worstcase upper bounds for MAX-2-SAT with application to MAX-CUT. Discrete Applied Mathematics 130(2), 139–155 (2003)
Hirsch, E.A.: New worst-case upper bounds for SAT. Journal of Automated Reasoning 24(4), 397–420 (2000)
Kulikov, A.S.: An upper bound O(20.16254n) for Exact 3-Satisfiability: A simpler proof. Zapiski nauchnykh seminarov POMI 293, 118–128 (2002), English translation is to appear in Journal of Mathematical Sciences
Kullmann, O., Luckhardt, H.: Algorithms for SAT/TAUT decision based on various measures. Informatics and Computation (1998)
Nikolenko, S.I., Sirotkin, A.V.: Worst-case upper bounds for SAT: automated proof. In: Proceedings of the Eight ESSLI Student Session, pp. 225–232 (2003), Available from http://logic.pdmi.ras.ru/~sergey
Raman, V., Ravikumar, B., Srinivasa Rao, S.: A Simplified NP-complete MAXSAT Problem. Information Processing Letters 65, 1–6 (1998)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Fedin, S.S., Kulikov, A.S. (2004). Automated Proofs of Upper Bounds on the Running Time of Splitting Algorithms. In: Downey, R., Fellows, M., Dehne, F. (eds) Parameterized and Exact Computation. IWPEC 2004. Lecture Notes in Computer Science, vol 3162. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-28639-4_22
Download citation
DOI: https://doi.org/10.1007/978-3-540-28639-4_22
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-23071-7
Online ISBN: 978-3-540-28639-4
eBook Packages: Springer Book Archive