Advertisement

An improved algorithm for the \((n, 3)\)-MaxSAT problem: asking branchings to satisfy the clauses

  • Chao Xu
  • Wenjun Li
  • Jianxin Wang
  • Yongjie YangEmail author
Article
  • 4 Downloads

Abstract

We study the \((n, 3)\)-MaxSAT problem where we are given an integer k and a CNF formula with n variables, each of which appears in at most 3 clauses, and the question is whether there is an assignment that satisfies at least k clauses. Based on refined observations, we propose a branching algorithm for the \((n, 3)\)-MaxSAT problem which significantly improves the previous results. More precisely, the running time of our algorithm can be bounded by \(O^*(1.175^k)\) and \(O^*(1.194^n)\), respectively. Prior to our study, the running time of the best known exact algorithm can be bounded by \(O^*(1.194^k)\) and \(O^*(1.237^n)\), respectively.

Keywords

CNF formula 3-SAT Branching algorithm Complexity Parameterized complexity 

Notes

References

  1. Argelich J, Manyà F (2006) Exact Max-SAT solvers for over-constrained problems. J Heuristics 12(4–5):375–392CrossRefzbMATHGoogle Scholar
  2. Aspvall B, Plass MF, Tarjan RE (1979) A linear-time algorithm for testing the truth of certain quantified boolean formulas. Inf Process Lett 8(3):121–123MathSciNetCrossRefzbMATHGoogle Scholar
  3. Bansal N, Raman V (1999) Upper bounds for MaxSAT: further improved. In: ISAAC, pp 247–258Google Scholar
  4. Berg J, Hyttinen A, Järvisalo M (2015) Applications of MaxSAT in data analysis. In: Pragmatics of SAT workshopGoogle Scholar
  5. Bliznets I, Golovnev A (2012) A new algorithm for parameterized MAX-SAT. In: IPEC, pp 37–48Google Scholar
  6. Bliznets IA (2013) A new upper bound for \((n, 3)\)-MAX-SAT. J Math Sci 188(1):1–6MathSciNetCrossRefzbMATHGoogle Scholar
  7. Bonet ML, Levy J, Manyà F (2007) Resolution for Max-SAT. Artif Intell 171(8–9):606–618MathSciNetCrossRefzbMATHGoogle Scholar
  8. Calabro C, Impagliazzo R, Paturi R (2006) A duality between clause width and clause density for SAT. In: CCC, pp 252–260Google Scholar
  9. Chen J, Kanj IA (2004) Improved exact algorithms for Max-Sat. Discrete Appl Math 142(1–3):17–27MathSciNetCrossRefzbMATHGoogle Scholar
  10. Chen J, Kanj IA, Xia G (2010) Improved upper bounds for vertex cover. Theor Comput Sci 411(40–42):3736–3756MathSciNetCrossRefzbMATHGoogle Scholar
  11. Cook SA (1971) The complexity of theorem-proving procedures. In: STOC, pp 151–158Google Scholar
  12. Cygan M, Fomin FV, Kowalik L, Lokshtanov D, Marx D, Pilipczuk M, Pilipczuk M, Saurabh S (2015) Lower bounds based on the exponential-time hypothesis. Springer, Berlin, pp 467–521Google Scholar
  13. Fomin FV, Kratsch D (2010) Exact exponential algorithms, chapter 2. Texts in theoretical computer science An EATCS series. Springer, Berlin, pp 13–30Google Scholar
  14. Garey M, Johnson D (1979) Computers and intractability: a guide to the theory of NP-completeness. W. H. Freeman, New YorkzbMATHGoogle Scholar
  15. Goemans MX, Williamson DP (1994) New 3/4-approximation algorithms for the maximum satisfiability problem. SIAM J Discrete Math 7(4):656–666MathSciNetCrossRefzbMATHGoogle Scholar
  16. Goemans MX, Williamson DP (1995) Improved approximation algorithms for maximum cut and satisfiability problems using semidefinite programming. J ACM 42(6):1115–1145MathSciNetCrossRefzbMATHGoogle Scholar
  17. Gu J (1994) Global optimization for satisfiability (SAT) problem. IEEE Trans Knowl Data Eng 6(3):361–381CrossRefGoogle Scholar
  18. Hirsch EA (2000) New worst-case upper bounds for SAT. J Autom Reason 24(4):397–420MathSciNetCrossRefzbMATHGoogle Scholar
  19. Hirsch EA, Kojevnikov A (2005) Unitwalk: a new SAT solver that uses local search guided by unit clause elimination. Ann Math Artif Intell 43(1):91–111MathSciNetCrossRefzbMATHGoogle Scholar
  20. Hochbaum D (1997) Approximation algorithms for NP-hard problems. PWS Publishing Company, BostonzbMATHGoogle Scholar
  21. Hutter F, Lindauer M, Balint A, Bayless S, Hoos H, Leyton-Brown K (2017) The configurable SAT solver challenge (CSSC). Artif Intell 243:1–25MathSciNetCrossRefzbMATHGoogle Scholar
  22. Impagliazzo R, Paturi R (2001) On the complexity of \(k\)-SAT. J Comput Syst Sci 62(2):367–375MathSciNetCrossRefzbMATHGoogle Scholar
  23. Karloff HJ, Zwick U (1997) A 7/8-approximation algorithm for MAX 3SAT? In: FOCS, pp 406–415Google Scholar
  24. Kulikov AS (2005) Automated generation of simplification rules for SAT and MAXSAT. In: SAT, pp 430–436Google Scholar
  25. Li W, Xu C, Wang J, Yang Y (2017) An improved branching algorithm for \((n, 3)\)-MaxSAT based on refined observations. In: COCOA, pp 94–108Google Scholar
  26. Lokshtanov D (2009) New methods in parameterized algorithms and complexity. Ph.D. thesis, University of BergenGoogle Scholar
  27. Luo C, Cai S, Su K, Huang W (2017) CCEHC: an efficient local search algorithm for weighted partial maximum satisfiability. Artif Intell 243:26–44MathSciNetCrossRefzbMATHGoogle Scholar
  28. Niedermeier R, Rossmanith P (2000) New upper bounds for maximum satisfiability. J Algorithms 36(1):63–88MathSciNetCrossRefzbMATHGoogle Scholar
  29. Patrascu M, Williams R (2010) On the possibility of faster SAT algorithms. In: SODA, pp 1065–1075Google Scholar
  30. Poloczek M, Schnitger G, Williamson DP, van Zuylen A (2017) Greedy algorithms for the maximum satisfiability problem: simple algorithms and inapproximability bounds. SIAM J Comput 46(3):1029–1061MathSciNetCrossRefzbMATHGoogle Scholar
  31. Raman V, Ravikumar B, Rao SS (1998) A simplified NP-complete MAXSAT problem. Inf Process Lett 65(1):1–6MathSciNetCrossRefzbMATHGoogle Scholar
  32. Saikko P, Malone B, Järvisalo M (2015) MaxSAT-based cutting planes for learning graphical models. In: CPAIOR, pp 347–356Google Scholar
  33. Selman B, Mitchell DG, Levesque HJ (1996) Generating hard satisfiability problems. Artif Intell 81(1–2):17–29MathSciNetCrossRefGoogle Scholar
  34. Shen H, Zhang H (2005) Improving exact algorithms for MAX-2-SAT. Ann Math Artif Intell 44(4):419–436MathSciNetCrossRefzbMATHGoogle Scholar
  35. Xiao M, Nagamochi H (2016) An exact algorithm for maximum independent set in degree-5 graphs. Discrete Appl Math 199:137–155MathSciNetCrossRefzbMATHGoogle Scholar
  36. Xu C, Chen J, Wang J (2016) Resolution and linear CNF formulas: improved \((n, 3)\)-MaxSAT algorithms. Theor Comput Sci (to appear)Google Scholar

Copyright information

© Springer Science+Business Media, LLC, part of Springer Nature 2019

Authors and Affiliations

  1. 1.School of Computer Science and EngineeringCentral South UniversityChangshaChina
  2. 2.Hunan Provincial Key Laboratory of Intelligent Processing of Big Data on TransportationChangsha University of Science and TechnologyChangshaChina
  3. 3.Chair of Economic TheorySaarland UniversitySaarbrückenGermany

Personalised recommendations