Geodesic
Automated proofs of upper bounds on the running time of splitting algorithms
Zapiski Nauchnykh Seminarov POMI, Computational complexity theory. Part IX, Tome 316 (2004), pp. 111-128 Cet article a éte moissonné depuis la source Math-Net.Ru

Voir la notice du chapitre de livre

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 present a program that, given a set of simplification rules, automatically generates a proof of an upper bound on the running time of a splitting algorithm using 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. 
@article{ZNSL_2004_316_a5,
     author = {A. S. Kulikov and S. S. Fedin},
     title = {Automated proofs of upper bounds on the running time of splitting algorithms},
     journal = {Zapiski Nauchnykh Seminarov POMI},
     pages = {111--128},
     year = {2004},
     volume = {316},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/ZNSL_2004_316_a5/}
}
TY  - JOUR
AU  - A. S. Kulikov
AU  - S. S. Fedin
TI  - Automated proofs of upper bounds on the running time of splitting algorithms
JO  - Zapiski Nauchnykh Seminarov POMI
PY  - 2004
SP  - 111
EP  - 128
VL  - 316
UR  - http://geodesic.mathdoc.fr/item/ZNSL_2004_316_a5/
LA  - ru
ID  - ZNSL_2004_316_a5
ER  - 
%0 Journal Article
%A A. S. Kulikov
%A S. S. Fedin
%T Automated proofs of upper bounds on the running time of splitting algorithms
%J Zapiski Nauchnykh Seminarov POMI
%D 2004
%P 111-128
%V 316
%U http://geodesic.mathdoc.fr/item/ZNSL_2004_316_a5/
%G ru
%F ZNSL_2004_316_a5
A. S. Kulikov; S. S. Fedin. Automated proofs of upper bounds on the running time of splitting algorithms. Zapiski Nauchnykh Seminarov POMI, Computational complexity theory. Part IX, Tome 316 (2004), pp. 111-128. http://geodesic.mathdoc.fr/item/ZNSL_2004_316_a5/

[1] J. M. Byskov, B. A. Madsen, B. Skjernaa, “New Algorithms for Exact Satisfiability”, Theoret. Comput. Sci., 332:1-3 (2005), 515–541 | DOI | MR | Zbl

[2] N. Bansal, V. Raman, “Upper Bounds for MaxSat: Further Improved”, Proceedings of ISAAC'99, 1999, 247–258 | MR | Zbl

[3] J. Chen, I. Kanj, Improved exact algorithms for MAX-SAT (to appear)

[4] M. A. Vsemirnov, E. A. Girsh, E. Ya. Dantsin, S. V. Ivanov, “Algoritmy dlya propozitsionalnoi vypolnimosti i verkhnie otsenki ikh slozhnosti”, Zap. nauchn. semin. POMI, 277, 2001, 14–46 | MR | Zbl

[5] M. Davis, G. Logemann, D. Loveland, “A machine program for theorem-proving”, Comm. ACM, 5 (1962), 394–397 | DOI | MR | Zbl

[6] A. S. Kulikov, S. S. Fedin, “Reshenie zadachi o maksimalnom sechenii za vremya $2^{|E|/4}$”, Zap. nauchn. semin. POMI, 293, 2002, 129–138 | MR | Zbl

[7] J. Gramm, J. Guo, F. Hüffner, R. Niedermeier, “Automated Generation of Search Tree Algorithms for Hard Graph Modification Problems Algorithmica”, Algorithmica, 39:4 (2004), 321–347 | DOI | MR | Zbl

[8] J. Gramm, E. A. Hirsch, R. Niedermeier, P. Rossmanith, “New worst-case upper bounds for MAX-2-SAT with application to MAX-CUT”, Discrete Applied Mathematics, 130:2 (2003), 139–155 | DOI | MR | Zbl

[9] E. A. Hirsch, “New worst-case upper bounds for SAT”, J. Automated Reasoning, 24:4 (2000), 397–420 | DOI | MR | Zbl

[10] A. S. Kulikov, “Verkhnyaya otsenka $O(2^{0.16254n})$ dlya { X$3$SAT}: bolee prostoe dokazatelstvo”, Zap. nauchn. semin. POMI, 293, 2002, 118–128 | MR | Zbl

[11] O. Kullmann, H. Luckhardt, “Algorithms for SAT/TAUT decision based on various measures”, Informatics and Computation, 1998 (to appear)

[12] S. I. Nikolenko, A. V. Sirotkin, “Worst-case upper bounds for SAT: automated proof”, Proceedings of the 8th ESSLLI Student Session, 2003, 225–232

[13] V. Raman, B. Ravikumar, S. Srinivasa Rao, “A Simplified NP-complete MAXSAT Problem”, Information Processing Letters, 65 (1998), 1–6 | DOI | MR