×

zbMATH — the first resource for mathematics

Improved exact algorithms for mildly sparse instances of MAX SAT. (English) Zbl 1379.68178
Summary: We present improved exponential time exact algorithms for Max SAT. Our algorithms run in time of the form \(O(2^{(1 - \mu(c)) n})\) for instances with \(n\) variables and \(m = c n\) clauses. In this setting, there are three incomparable currently best algorithms: a deterministic exponential space algorithm with \(\mu(c) = \frac{1}{O(c \log c)}\) due to E. Dantsin and A. Wolpert [Lect. Notes Comput. Sci. 4121, 266–276 (2006; Zbl 1187.68258)], a randomized polynomial space algorithm with \(\mu(c) = \frac{1}{O(c \log^3 c)}\) and a deterministic polynomial space algorithm with \(\mu(c) = \frac{1}{O(c^2 \log^2 c)}\) due to T. Sakai et al. [Theory Comput. Syst. 57, No. 2, 426–443 (2015; Zbl 1347.68312)]. Our first result is a deterministic polynomial space algorithm with \(\mu(c) = \frac{1}{O(c \log c)}\) that achieves the previous best time complexity without exponential space or randomization. Furthermore, this algorithm can handle instances with exponentially large weights and hard constraints. The previous algorithms and our deterministic polynomial space algorithm run super-polynomially faster than \(2^n\) only if \(m = O(n^2)\). Our second results are deterministic exponential space algorithms for Max SAT with \(\mu(c) = \frac{1}{O((c \log c)^{2 / 3})}\) and for Max 3-SAT with \(\mu(c) = \frac{1}{O(c^{1 / 2})}\) that run super-polynomially faster than \(2^n\) when \(m = o(n^{5 / 2} / \log^{5 / 2} n)\) and \(m = o(n^3 / \log^2 n)\) respectively. Our third result is a randomized exponential space algorithm for Max SAT with \(\mu(c) = \frac{1}{O(c^{1 / 2} \log^{3 / 2} c)}\) that run super-polynomially faster than \(2^n\) when \(m = o(n^3 / \log^5 n)\).
MSC:
68Q25 Analysis of algorithms and problem complexity
68W05 Nonnumerical algorithms
68W20 Randomized algorithms
68W40 Analysis of algorithms
Software:
MAX-2-SAT
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Bansal, Nikhil; Raman, Venkatesh, Upper bounds for maxsat: further improved, (Proceedings of the 10th International Symposium on Algorithms and Computation, ISAAC, Lecture Notes in Computer Science, vol. 1741, (1999), Springer), 247-258 · Zbl 0971.68069
[2] Binkele-Raible, Daniel; Fernau, Henning, A new upper bound for MAX-2-SAT: a graph-theoretic approach, J. Discrete Algorithms, 8, 4, 388-401, (2010) · Zbl 1203.90130
[3] Bliznets, Ivan; Golovnev, Alexander, A new algorithm for parameterized MAX-SAT, (Proceedings of the 7th International Symposium on Parameterized and Exact Computation, IPEC, Lecture Notes in Computer Science, vol. 7535, (2012), Springer), 37-48 · Zbl 1360.68494
[4] Calabro, Chris; Impagliazzo, Russell; Paturi, Ramamohan, A duality between clause width and clause density for SAT, (Proceedings of the 21st Annual IEEE Conference on Computational Complexity, CCC, (2006)), 252-260
[5] Chen, Jianer; Kanj, Iyad A., Improved exact algorithms for MAX-SAT, Discrete Appl. Math., 142, 1-3, 17-27, (2004) · Zbl 1077.68116
[6] Chen, Ruiwen; Kabanets, Valentine; Kolokolova, Antonina; Shaltiel, Ronen; Zuckerman, David, Mining circuit lower bound proofs for meta-algorithms, Comput. Complexity, 24, 2, 333-392, (2015) · Zbl 1401.68116
[7] Chen, Ruiwen; Santhanam, Rahul, Improved algorithms for sparse MAX-SAT and MAX-k-CSP, (Proceedings of the 18th International Conference on Theory and Applications of Satisfiability Testing, SAT, (2015)), 33-45 · Zbl 06512563
[8] Dantsin, Evgeny; Hirsch, Edward A., Worst-case upper bounds, (Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol. 185, (2009), IOS Press), 403-424
[9] Dantsin, Evgeny; Wolpert, Alexander, MAX-SAT for formulas with constant clause density can be solved faster than in \(O(2^n)\) time, (Proceedings of the 9th International Conference on Theory and Applications of Satisfiability Testing, SAT, Lecture Notes in Computer Science, vol. 4121, (2006), Springer), 266-276 · Zbl 1187.68258
[10] Eppstein, David, Quasiconvex analysis of multivariate recurrence equations for backtracking algorithms, ACM Trans. Algorithms, 2, 4, 492-509, (2006) · Zbl 1321.68558
[11] Fomin, Fedor V.; Grandoni, Fabrizio; Kratsch, Dieter, A measure & conquer approach for the analysis of exact algorithms, J. ACM, 56, 5, 25:1-25:32, (2009) · Zbl 1325.68311
[12] Gaspers, Serge; Sorkin, Gregory B., A universally fastest algorithm for MAX 2-SAT, MAX 2-CSP, and everything in between, J. Comput. Syst. Sci., 78, 1, 305-335, (2012) · Zbl 1238.68066
[13] Gaspers, Serge; Sorkin, Gregory B., Separate, measure and conquer: faster polynomial-space algorithms for MAX 2-CSP and counting dominating sets, (Proceedings of the 42nd International Colloquium on Automata, Languages, and Programming, ICALP, Part I, (2015)), 567-579 · Zbl 1436.68393
[14] Golovnev, Alexander; Kutzkov, Konstantin, New exact algorithms for the 2-constraint satisfaction problem, Theoret. Comput. Sci., 526, 18-27, (2014) · Zbl 1290.68144
[15] Gramm, Jens; Hirsch, Edward A.; Niedermeier, Rolf; Rossmanith, Peter, Worst-case upper bounds for MAX-2-SAT with an application to MAX-CUT, Discrete Appl. Math., 130, 2, 139-155, (2003) · Zbl 1051.68078
[16] Gramm, Jens; Niedermeier, Rolf, Faster exact solutions for MAX2SAT, (Proceedings of the 4th Italian Conference on Algorithms and Complexity, CIAC, Lecture Notes in Computer Science, vol. 1767, (2000), Springer), 174-186 · Zbl 0971.68598
[17] Gutin, Gregory; Yeo, Anders, Constraint satisfaction problems parameterized above or below tight bounds: a survey, (The Multivariate Algorithmic Revolution and Beyond, Lecture Notes in Computer Science, vol. 7370, (2012), Springer), 257-286 · Zbl 1358.68135
[18] Hirsch, Edward A., A new algorithm for MAX-2-SAT, (Proceedings of the 17th Annual Symposium on Theoretical Aspects of Computer Science, STACS, Lecture Notes in Computer Science, vol. 1770, (2000), Springer), 65-73 · Zbl 0959.68047
[19] Hirsch, Edward A., Worst-case study of local search for MAX-k-SAT, Discrete Appl. Math., 130, 2, 173-184, (2003) · Zbl 1051.68079
[20] Impagliazzo, Russell; Paturi, Ramamohan; Schneider, Stefan, A satisfiability algorithm for sparse depth two threshold circuits, (Proceedings of the 54th Annual IEEE Symposium on Foundations of Computer Science, FOCS, (2013)), 479-488
[21] Kneis, Joachim; Mölle, Daniel; Richter, Stefan; Rossmanith, Peter, On the parameterized complexity of exact satisfiability problems, (Proceedings of the 30th International Symposium on Mathematical Foundations of Computer Science, MFCS, Lecture Notes in Computer Science, vol. 3618, (2005), Springer), 568-579 · Zbl 1156.68404
[22] Kneis, Joachim; Mölle, Daniel; Richter, Stefan; Rossmanith, Peter, A bound on the pathwidth of sparse graphs with applications to exact algorithms, SIAM J. Discrete Math., 23, 1, 407-427, (2009) · Zbl 1219.05187
[23] Koivisto, Mikko, Optimal 2-constraint satisfaction via sum-product algorithms, Inform. Process. Lett., 98, 1, 24-28, (2006) · Zbl 1186.68439
[24] Kojevnikov, Arist; Kulikov, Alexander S., A new approach to proving upper bounds for MAX-2-SAT, (Proceedings of the 17th Annual ACM-SIAM Symposium on Discrete Algorithms, SODA, (2006)), 11-17 · Zbl 1192.68368
[25] Kulikov, Alexander S., Automated generation of simplification rules for SAT and MAXSAT, (Proceedings of the 8th International Conference on Theory and Applications of Satisfiability Testing, SAT, Lecture Notes in Computer Science, vol. 3569, (2005), Springer), 430-436 · Zbl 1128.68469
[26] Kulikov, Alexander S.; Kutzkov, Konstantin, New bounds for MAX-SAT by clause learning, (Proceedings of the 8th International Computer Science Symposium in Russia, CSR, Lecture Notes in Computer Science, vol. 4649, (2007), Springer), 194-204 · Zbl 1188.68272
[27] Le Gall, François, Powers of tensors and fast matrix multiplication, (Proceedings of the 39th International Symposium on Symbolic and Algebraic Computation, ISSAC, (2014)), 296-303 · Zbl 1325.65061
[28] Mahajan, Meena; Raman, Venkatesh, Parameterizing above guaranteed values: maxsat and maxcut, J. Algorithms, 31, 2, 335-354, (1999) · Zbl 0921.68052
[29] Niedermeier, Rolf; Rossmanith, Peter, New upper bounds for maximum satisfiability, J. Algorithms, 36, 1, 63-88, (2000) · Zbl 0959.68049
[30] Sakai, Takayuki; Seto, Kazuhisa; Tamaki, Suguru, Solving sparse instances of MAX SAT via width reduction and greedy restriction, Theory Comput. Syst., 57, 2, 426-443, (2015) · Zbl 1347.68312
[31] Sakai, Takayuki; Seto, Kazuhisa; Tamaki, Suguru; Teruyama, Junichi, Improved exact algorithms for mildly sparse instances of MAX SAT, (Proceedings of the 10th International Symposium on Parameterized and Exact Computation, IPEC, (2015)), 90-101 · Zbl 1378.68091
[32] Santhanam, Rahul, Fighting perebor: new and improved algorithms for formula and QBF satisfiability, (Proceedings of the 51th Annual IEEE Symposium on Foundations of Computer Science, FOCS, (2010)), 183-192
[33] Schuler, Rainer, An algorithm for the satisfiability problem of formulas in conjunctive normal form, J. Algorithms, 54, 1, 40-44, (2005) · Zbl 1090.68052
[34] Scott, Alex D.; Sorkin, Gregory B., Faster algorithms for MAX CUT and MAX CSP, with polynomial expected time for sparse instances, (Proceedings of the 6th International Workshop on Approximation Algorithms for Combinatorial Optimization Problems (APPROX) and the 7th International Workshop on Randomization and Computation (RANDOM), Lecture Notes in Computer Science, vol. 2764, (2003), Springer), 382-395 · Zbl 1279.68108
[35] Scott, Alexander D.; Sorkin, Gregory B., Linear-programming design and analysis of fast algorithms for MAX 2-CSP, Discrete Optim., 4, 3-4, 260-287, (2007) · Zbl 1153.90505
[36] Seto, Kazuhisa; Tamaki, Suguru, A satisfiability algorithm and average-case hardness for formulas over the full binary basis, Comput. Complexity, 22, 2, 245-274, (2013) · Zbl 1286.68208
[37] Williams, Ryan, A new algorithm for optimal 2-constraint satisfaction and its implications, Theoret. Comput. Sci., 348, 2-3, 357-365, (2005) · Zbl 1081.68095
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.