New upper bounds for the problem of maximal satisfiability
Diskretnaya Matematika, Tome 21 (2009) no. 1, pp. 139-157.

Voir la notice de l'article provenant de la source Math-Net.Ru

In this paper we present relatively simple proofs of the following new upper bounds: $c^N$, where $c2$ is a constant and $N$ is the number of variables, for MAX-SAT for formulas with constant clause density; $2^{K/6}$, where $K$ is the number of clauses, for MAX-2-SAT; $2^{N/6,7}$ for $(n,3)$-MAX-2-SAT. All bounds are proved by the splitting method. The main two techniques are combined complexity measures and clause learning.
@article{DM_2009_21_1_a7,
     author = {A. S. Kulikov and K. Kutskov},
     title = {New upper bounds for the problem of maximal satisfiability},
     journal = {Diskretnaya Matematika},
     pages = {139--157},
     publisher = {mathdoc},
     volume = {21},
     number = {1},
     year = {2009},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/DM_2009_21_1_a7/}
}
TY  - JOUR
AU  - A. S. Kulikov
AU  - K. Kutskov
TI  - New upper bounds for the problem of maximal satisfiability
JO  - Diskretnaya Matematika
PY  - 2009
SP  - 139
EP  - 157
VL  - 21
IS  - 1
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/DM_2009_21_1_a7/
LA  - ru
ID  - DM_2009_21_1_a7
ER  - 
%0 Journal Article
%A A. S. Kulikov
%A K. Kutskov
%T New upper bounds for the problem of maximal satisfiability
%J Diskretnaya Matematika
%D 2009
%P 139-157
%V 21
%N 1
%I mathdoc
%U http://geodesic.mathdoc.fr/item/DM_2009_21_1_a7/
%G ru
%F DM_2009_21_1_a7
A. S. Kulikov; K. Kutskov. New upper bounds for the problem of maximal satisfiability. Diskretnaya Matematika, Tome 21 (2009) no. 1, pp. 139-157. http://geodesic.mathdoc.fr/item/DM_2009_21_1_a7/

[1] Beame P., Impagliazzo R., Pitassi T., Segerlind N., “Memorization and DPLL: formula caching proof systems”, Proc. 18th IEEE Annual Conf. Computational Complexity, 2003, 248–259

[2] Chen J., Kanj I., “Improved exact algorithms for MAX-SAT”, Lecture Notes Computer Sci., 2286, 2002, 341–355 | MR | Zbl

[3] Dantsin E., Wolpert A., “MAX-SAT for formulas with constant clause density can be solved faster than in $O(2^n)$ time”, Lecture Notes Computer Sci., 4121, 2006, 266–276 | MR | Zbl

[4] Fedin S. S., Kulikov A. S., “Automated proofs of upper bounds on running time of splitting algorithms”, J. Math. Sci., 134:5 (2006), 2383–2391 | DOI | MR

[5] Fomin F. V., Grandoni F., Kratsch D., A Measure Conquer approach for the analysis of exact algorithms, Techn. Rep. 359, Univ. Bergen, 2007

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

[7] Hirsch E. A., A $2^{K/4}$-time algorithm for MAX-2-SAT: Corrected version, ECCC Report TR99-036, Rev. 02, 2000

[8] Kneis J., Moelle D., Richter S., Rossmanith P., “Algorithms based on the treewidth of sparse graphs”, Lecture Notes Computer Sci., 3787, 2005, 385–396 | MR | Zbl

[9] Kneis J., Rossmanith P., A new satisfiability algorithm with applications to MAX-CUT, Techn. Rep. AIB2005-08, Dept. Computer Sci. RWTH Aachen Univ., 2005

[10] Kojevnikov A., Kulikov A. S., “A new approach to proving upper bounds for MAX-2-SAT”, Proc. 17th Annual ACM-SIAM Symp. Discrete Algorithms, 2006, 11–17

[11] Kulikov A. S., “Automated generation of simplification rules for SAT and MAXSAT”, Lecture Notes Computer Sci., 3569, 2005, 430–436 | Zbl

[12] Kulikov A. S., Kutzkov K., “New bounds for MAX-SAT by clause learning”, Lecture Notes Computer Sci., 4549, 2007, 194–204

[13] Kullmann O., “New methods for 3-SAT decision and worst-case analysis”, Theoret. Computer Sci., 223 (1997), 1–72 | DOI | MR

[14] Marques-Silva J. P., Sakallah K. A., “GRASP: a search algorithm for propositional satisfiability”, IEEE Trans. Comput., 48:5 (1999), 506–521 | DOI | MR

[15] Moskewicz M. W., Madigan C. F., Zhao Y., Zhang L., Malik S., “CHAFF: engineering an efficient SAT solver”, Proc. 38th Design Automation Conf., 2001, 530–535

[16] Niedermeier R., Rossmanith P., “New upper bounds for MAX-SAT”, Lecture Notes Computer Sci., 1644, 1999, 575–585 | MR

[17] Poljak S., Tuza Z., “Maximum cuts and largest bipartite subgraphs”, DIMACS Ser. Discrete Math. Theor. Comput. Sci., 20, 1995, 181–244 | MR | Zbl

[18] Raible D., Fernau H., “A new upper bound for MAX-2-SAT: A graph-theoretic approach”, Mathematical foundations of computer science, Lecture Notes Computer Sci., 5162, 2008, 551–562 | Zbl

[19] Raman V., Ravikumar B., Srinivasa Rao S., “A simplified NP-complete MAXSAT problem”, Inform. Process. Lett., 65:1 (1998), 1–6 | DOI | MR

[20] Robson J. M., “Algorithms for maximum independent sets”, J. Algorithms, 7:3 (1986), 425–440 | DOI | MR | Zbl

[21] Scott A. D., Sorkin G. B., “Linear-programming design and analysis of fast algorithms for MAX-2-SAT and MAX-2-CSP”, Discrete Optimization, 4 (2007), 260–287 | DOI | MR | Zbl

[22] Scott A. D., Sorkin G. B., “Faster algorithms for MAX-CUT and MAX-CSP, with polynomial expected time for sparse instances”, Lecture Notes Computer Sci., 2764, 2003, 382–395 | MR

[23] Williams R., “On computing $k$-CNF formula properties”, Lecture Notes Computer Sci., 2919, 2003, 330–340

[24] Williams R., “A new algorithm for optimal 2-constraint satisfaction and its implications”, Theoret. Computer Sci., 348 (2005), 357–365 | DOI | MR | Zbl

[25] Zhang H., “An efficient propositional prover”, Lecture Notes Computer Sci., 1249, 1997, 272–275