Document Open Access Logo

Improved Exact Algorithms for Mildly Sparse Instances of Max SAT

Authors Takayuki Sakai, Kazuhisa Seto, Suguru Tamaki, Junichi Teruyama

PDF
Thumbnail PDF

File

LIPIcs.IPEC.2015.90.pdf
  • Filesize: 0.48 MB
  • 12 pages

Document Identifiers

Author Details

Takayuki Sakai
Kazuhisa Seto
Suguru Tamaki
Junichi Teruyama

Cite AsGet BibTex

Takayuki Sakai, Kazuhisa Seto, Suguru Tamaki, and Junichi Teruyama. Improved Exact Algorithms for Mildly Sparse Instances of Max SAT. In 10th International Symposium on Parameterized and Exact Computation (IPEC 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 43, pp. 90-101, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
https://doi.org/10.4230/LIPIcs.IPEC.2015.90

Abstract

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=cn clauses. In this setting, there are three incomparable currently best algorithms: a deterministic exponential space algorithm with mu(c)=1/O(c * log(c)) due to Dantsin and Wolpert [SAT 2006], a randomized polynomial space algorithm with mu(c)=1/O(c * log^3(c)) and a deterministic polynomial space algorithm with mu(c)=1/O(c^2 * log^2(c)) due to Sakai, Seto and Tamaki [Theory Comput. Syst., 2015]. Our first result is a deterministic polynomial space algorithm with mu(c)=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)=1/O((c * log(c))^{2/3}) and for Max 3-SAT with mu(c)=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.
Keywords
  • maximum satisfiability
  • weighted
  • polynomial space
  • exponential space

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Nikhil Bansal and Venkatesh Raman. Upper bounds for MaxSAT: Further improved. In Proceedings of the 10th International Symposium on Algorithms and Computation (ISAAC), volume 1741 of Lecture Notes in Computer Science, pages 247-258. Springer, 1999. Google Scholar
  2. Daniel Binkele-Raible and Henning Fernau. A new upper bound for Max-2-SAT: A graph-theoretic approach. J. Discrete Algorithms, 8(4):388-401, 2010. Google Scholar
  3. Ivan Bliznets and Alexander Golovnev. A new algorithm for parameterized MAX-SAT. In Proceedings of the 7th International Symposium on Parameterized and Exact Computation (IPEC), volume 7535 of Lecture Notes in Computer Science, pages 37-48. Springer, 2012. Google Scholar
  4. Chris Calabro, Russell Impagliazzo, and Ramamohan Paturi. A duality between clause width and clause density for SAT. In Proceedings of the 21st Annual IEEE Conference on Computational Complexity (CCC), pages 252-260, 2006. Google Scholar
  5. Jianer Chen and Iyad A. Kanj. Improved exact algorithms for MAX-SAT. Discrete Applied Mathematics, 142(1-3):17-27, 2004. Google Scholar
  6. Ruiwen Chen, Valentine Kabanets, Antonina Kolokolova, Ronen Shaltiel, and David Zuckerman. Mining circuit lower bound proofs for meta-algorithms. Computational Complexity, 24(2):333-392, 2015. Google Scholar
  7. Ruiwen Chen and Rahul Santhanam. Improved algorithms for sparse max-sat and max-k-csp. In Proceedings of the 18th International Conference on Theory and Applications of Satisfiability Testing (SAT), 2015. To appear. Google Scholar
  8. Evgeny Dantsin and Edward A. Hirsch. Worst-case upper bounds. In Handbook of Satisfiability, volume 185 of Frontiers in Artificial Intelligence and Applications, pages 403-424. IOS Press, 2009. Google Scholar
  9. Evgeny Dantsin and Alexander Wolpert. MAX-SAT for formulas with constant clause density can be solved faster than in O(2ⁿ) time. In Proceedings of the 9th International Conference on Theory and Applications of Satisfiability Testing (SAT), volume 4121 of Lecture Notes in Computer Science, pages 266-276. Springer, 2006. Google Scholar
  10. Serge Gaspers and Gregory B. Sorkin. A universally fastest algorithm for Max 2-SAT, Max 2-CSP, and everything in between. J. Comput. Syst. Sci., 78(1):305-335, 2012. Google Scholar
  11. Serge Gaspers and Gregory B. Sorkin. Separate, measure and conquer: Faster polynomial-space algorithms for Max 2-CSP and counting dominating sets. In Proceedings of the 42nd International Colloquium on Automata, Languages, and Programming (ICALP), Part I, pages 567-579, 2015. Google Scholar
  12. Alexander Golovnev and Konstantin Kutzkov. New exact algorithms for the 2-constraint satisfaction problem. Theor. Comput. Sci., 526:18-27, 2014. Google Scholar
  13. Jens Gramm, Edward A. Hirsch, Rolf Niedermeier, and Peter Rossmanith. Worst-case upper bounds for MAX-2-SAT with an application to MAX-CUT. Discrete Applied Mathematics, 130(2):139-155, 2003. Google Scholar
  14. Jens Gramm and Rolf Niedermeier. Faster exact solutions for MAX2SAT. In Proceedings of the 4th Italian Conference on Algorithms and Complexity (CIAC), volume 1767 of Lecture Notes in Computer Science, pages 174-186. Springer, 2000. Google Scholar
  15. Gregory Gutin and Anders Yeo. Constraint satisfaction problems parameterized above or below tight bounds: A survey. In The Multivariate Algorithmic Revolution and Beyond, volume 7370 of Lecture Notes in Computer Science, pages 257-286. Springer, 2012. Google Scholar
  16. Edward A. Hirsch. A new algorithm for MAX-2-SAT. In Proceedings of the 17th Annual Symposium on Theoretical Aspects of Computer Science (STACS), volume 1770 of Lecture Notes in Computer Science, pages 65-73. Springer, 2000. Google Scholar
  17. Edward A. Hirsch. Worst-case study of local search for MAX-k-SAT. Discrete Applied Mathematics, 130(2):173-184, 2003. Google Scholar
  18. Russell Impagliazzo, Ramamohan Paturi, and Stefan Schneider. A satisfiability algorithm for sparse depth two threshold circuits. In Proceedings of the 54th Annual IEEE Symposium on Foundations of Computer Science (FOCS), pages 479-488, 2013. Google Scholar
  19. Joachim Kneis, Daniel Mölle, Stefan Richter, and Peter Rossmanith. On the parameterized complexity of exact satisfiability problems. In Proceedings of the 30th International Symposium on Mathematical Foundations of Computer Science (MFCS), volume 3618 of Lecture Notes in Computer Science, pages 568-579. Springer, 2005. Google Scholar
  20. Joachim Kneis, Daniel Mölle, Stefan Richter, and Peter Rossmanith. A bound on the pathwidth of sparse graphs with applications to exact algorithms. SIAM J. Discrete Math., 23(1):407-427, 2009. Google Scholar
  21. Mikko Koivisto. Optimal 2-constraint satisfaction via sum-product algorithms. Inf. Process. Lett., 98(1):24-28, 2006. Google Scholar
  22. Arist Kojevnikov and Alexander S. Kulikov. A new approach to proving upper bounds for MAX-2-SAT. In Proceedings of the 17th Annual ACM-SIAM Symposium on Discrete Algorithms (SODA), pages 11-17, 2006. Google Scholar
  23. Alexander S. Kulikov. Automated generation of simplification rules for SAT and MAXSAT. In Proceedings of the 8th International Conference on Theory and Applications of Satisfiability Testing (SAT), volume 3569 of Lecture Notes in Computer Science, pages 430-436. Springer, 2005. Google Scholar
  24. Alexander S. Kulikov and Konstantin Kutzkov. New bounds for MAX-SAT by clause learning. In Proceedings of the 8th International Computer Science Symposium in Russia (CSR), volume 4649 of Lecture Notes in Computer Science, pages 194-204. Springer, 2007. Google Scholar
  25. François Le Gall. Powers of tensors and fast matrix multiplication. In Proceedings of the 39th International Symposium on Symbolic and Algebraic Computation (ISSAC), pages 296-303, 2014. Google Scholar
  26. Meena Mahajan and Venkatesh Raman. Parameterizing above guaranteed values: MaxSAT and MaxCUT. J. Algorithms, 31(2):335-354, 1999. Google Scholar
  27. Rolf Niedermeier and Peter Rossmanith. New upper bounds for maximum satisfiability. J. Algorithms, 36(1):63-88, 2000. Google Scholar
  28. Takayuki Sakai, Kazuhisa Seto, and Suguru Tamaki. Solving sparse instances of max SAT via width reduction and greedy restriction. Theory Comput. Syst., 57(2):426-443, 2015. Google Scholar
  29. Takayuki Sakai, Kazuhisa Seto, Suguru Tamaki, and Junichi Teruyama. A satisfiability algorithm for depth-2 circuits with a symmetric gate at the top and AND gates at the bottom. Electronic Colloquium on Computational Complexity (ECCC), TR15-136, 2015. Google Scholar
  30. Rahul Santhanam. Fighting perebor: New and improved algorithms for formula and QBF satisfiability. In Proceedings of the 51th Annual IEEE Symposium on Foundations of Computer Science (FOCS), pages 183-192, 2010. Google Scholar
  31. Rainer Schuler. An algorithm for the satisfiability problem of formulas in conjunctive normal form. J. Algorithms, 54(1):40-44, 2005. Google Scholar
  32. Alex D. Scott and Gregory B. Sorkin. Faster algorithms for MAX CUT and MAX CSP, with polynomial expected time for sparse instances. In Proceedings of the 6th International Workshop on Approximation Algorithms for Combinatorial Optimization Problems (APPROX) and the 7th International Workshop on Randomization and Computation (RANDOM), volume 2764 of Lecture Notes in Computer Science, pages 382-395. Springer, 2003. Google Scholar
  33. Alexander D. Scott and Gregory B. Sorkin. Linear-programming design and analysis of fast algorithms for Max 2-CSP. Discrete Optimization, 4(3-4):260-287, 2007. Google Scholar
  34. Kazuhisa Seto and Suguru Tamaki. A satisfiability algorithm and average-case hardness for formulas over the full binary basis. Computational Complexity, 22(2):245-274, 2013. Google Scholar
  35. Ryan Williams. A new algorithm for optimal 2-constraint satisfaction and its implications. Theor. Comput. Sci., 348(2-3):357-365, 2005. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact