Skip to main content
SpringerLink
Log in

Solving Sparse Instances of Max SAT via Width Reduction and Greedy Restriction

  • Conference paper
Theory and Applications of Satisfiability Testing – SAT 2014 (SAT 2014)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 8561))

Abstract

We present a moderately exponential time polynomial space algorithm for sparse instances of Max SAT. Our algorithms run in time of the form O(2(1 − μ(c))n) for instances with n variables and cn clauses. Our deterministic and randomized algorithm achieve \(\mu(c) = \Omega(\frac{1}{c^2\log^2 c})\) and \(\mu(c) = \Omega(\frac{1}{c \log^3 c})\) respectively. Previously, an exponential space deterministic algorithm with \(\mu(c) = \Omega(\frac{1}{c\log c})\) was shown by Dantsin and Wolpert [SAT 2006] and a polynomial space deterministic algorithm with \(\mu(c) = \Omega(\frac{1}{2^{O(c)}})\) was shown by Kulikov and Kutzkov [CSR 2007].

Our algorithms have three new features. They can handle instances with (1) weights and (2) hard constraints, and also (3) they can solve counting versions of Max SAT. Our deterministic algorithm is based on the combination of two techniques, width reduction of Schuler and greedy restriction of Santhanam. Our randomized algorithm uses random restriction instead of greedy restriction.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Bansal, N., Raman, V.: Upper bounds for MaxSAT: Further improved. In: Aggarwal, A.K., Pandu Rangan, C. (eds.) ISAAC 1999. LNCS, vol. 1741, pp. 247–258. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  2. Binkele-Raible, D., Fernau, H.: A new upper bound for Max-2-SAT: A graph-theoretic approach. J. Discrete Algorithms 8(4), 388–401 (2010)

    Article  MATH  MathSciNet  Google Scholar 

  3. Bliznets, I., Golovnev, A.: A new algorithm for parameterized MAX-SAT. In: Thilikos, D.M., Woeginger, G.J. (eds.) IPEC 2012. LNCS, vol. 7535, pp. 37–48. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  4. Calabro, C., Impagliazzo, R., Paturi, R.: A duality between clause width and clause density for SAT. In: Proceedings of the 21st Annual IEEE Conference on Computational Complexity (CCC), pp. 252–260 (2006)

    Google Scholar 

  5. Calabro, C., Impagliazzo, R., Paturi, R.: The complexity of satisfiability of small depth circuits. In: Chen, J., Fomin, F.V. (eds.) IWPEC 2009. LNCS, vol. 5917, pp. 75–85. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  6. Chen, J., Kanj, I.A.: Improved exact algorithms for MAX-SAT. Discrete Applied Mathematics 142(1-3), 17–27 (2004)

    Article  MATH  MathSciNet  Google Scholar 

  7. Chen, R., Kabanets, V., Kolokolova, A., Shaltiel, R., Zuckerman, D.: Mining circuit lower bound proofs for meta-algorithms. Electronic Colloquium on Computational Complexity (ECCC) TR13-057 (2013)

    Google Scholar 

  8. Dantsin, E., Wolpert, A.: AX-SAT for formulas with constant clause density can be solved faster than in O(2n) time. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 266–276. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  9. Gaspers, S., Sorkin, G.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)

    Article  MATH  MathSciNet  Google Scholar 

  10. Gramm, J., Hirsch, E.A., Niedermeier, R., Rossmanith, P.: Worst-case upper bounds for MAX-2-SAT with an application to MAX-CUT. Discrete Applied Mathematics 130(2), 139–155 (2003)

    Article  MATH  MathSciNet  Google Scholar 

  11. Gramm, J., Niedermeier, R.: Faster exact solutions for MAX2SAT. In: Bongiovanni, G., Petreschi, R., Gambosi, G. (eds.) CIAC 2000. LNCS, vol. 1767, pp. 174–186. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  12. Gutin, G., Yeo, A.: Constraint satisfaction problems parameterized above or below tight bounds: A survey. In: Bodlaender, H.L., Downey, R., Fomin, F.V., Marx, D. (eds.) Fellows Festschrift 2012. LNCS, vol. 7370, pp. 257–286. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  13. Håstad, J.: The shrinkage exponent of De Morgan formulas is 2. SIAM J. Comput. 27(1), 48–64 (1998)

    Article  MATH  MathSciNet  Google Scholar 

  14. Hirsch, E.A.: A new algorithm for MAX-2-SAT. In: Reichel, H., Tison, S. (eds.) STACS 2000. LNCS, vol. 1770, pp. 65–73. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  15. Hirsch, E.A.: Worst-case study of local search for MAX-k-SAT. Discrete Applied Mathematics 130(2), 173–184 (2003)

    Article  MATH  MathSciNet  Google Scholar 

  16. Horowitz, E., Sahni, S.: Computing partitions with applications to the knapsack problem. J. ACM 21(2), 277–292 (1974)

    Article  MATH  MathSciNet  Google Scholar 

  17. Impagliazzo, R., Matthews, W., Paturi, R.: A satisfiability algorithm for AC0. In: Proceedings of the 23rd Annual ACM-SIAM Symposium on Discrete Algorithms (SODA), pp. 961–972 (2012)

    Google Scholar 

  18. Impagliazzo, R., Paturi, R., Schneider, S.: A satisfiability algorithm for sparse depth two threshold circuits. In: Proceedings of the 54th Annual IEEE Symposium on Foundations of Computer Science (FOCS), pp. 479–488 (2013)

    Google Scholar 

  19. Kneis, J., Mölle, D., Richter, S., Rossmanith, P.: On the parameterized complexity of exact satisfiability problems. In: Jedrzejowicz, J., Szepietowski, A. (eds.) MFCS 2005. LNCS, vol. 3618, pp. 568–579. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  20. Kneis, J., Mölle, D., Richter, S., Rossmanith, P.: A bound on the pathwidth of sparse graphs with applications to exact algorithms. SIAM J. Discrete Math. 23(1), 407–427 (2009)

    Article  MATH  Google Scholar 

  21. Koivisto, M.: Optimal 2-constraint satisfaction via sum-product algorithms. Inf. Process. Lett. 98(1), 24–28 (2006)

    Article  MATH  MathSciNet  Google Scholar 

  22. Kojevnikov, A., Kulikov, A.S.: A new approach to proving upper bounds for MAX-2-SAT. In: Proceedings of the 17th Annual ACM-SIAM Symposium on Discrete Algorithms (SODA), pp. 11–17 (2006)

    Google Scholar 

  23. Kulikov, A.S.: Automated generation of simplification rules for SAT and MAXSAT. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol. 3569, pp. 430–436. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  24. Kulikov, A.S., Kutzkov, K.: New bounds for MAX-SAT by clause learning. In: Diekert, V., Volkov, M.V., Voronkov, A. (eds.) CSR 2007. LNCS, vol. 4649, pp. 194–204. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  25. Mahajan, M., Raman, V.: Parameterizing above guaranteed values: MaxSAT and MaxCUT. J. Algorithms 31(2), 335–354 (1999)

    Article  MATH  MathSciNet  Google Scholar 

  26. Niedermeier, R., Rossmanith, P.: New upper bounds for maximum satisfiability. J. Algorithms 36(1), 63–88 (2000)

    Article  MATH  MathSciNet  Google Scholar 

  27. Santhanam, R.: 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), pp. 183–192 (2010)

    Google Scholar 

  28. Schuler, R.: An algorithm for the satisfiability problem of formulas in conjunctive normal form. J. Algorithms 54(1), 40–44 (2005)

    Article  MATH  MathSciNet  Google Scholar 

  29. Scott, A.D., Sorkin, G.B.: Faster algorithms for MAX CUT and MAX CSP, with polynomial expected time for sparse instances. In: Arora, S., Jansen, K., Rolim, J.D.P., Sahai, A. (eds.) RANDOM 2003 and APPROX 2003. LNCS, vol. 2764, pp. 382–395. Springer, Heidelberg (2003)

    Google Scholar 

  30. Scott, A.D., Sorkin, G.B.: Linear-programming design and analysis of fast algorithms for Max 2-CSP. Discrete Optimization 4(3-4), 260–287 (2007)

    Article  MATH  MathSciNet  Google Scholar 

  31. Seto, K., Tamaki, S.: A satisfiability algorithm and average-case hardness for formulas over the full binary basis. Computational Complexity 22(2), 245–274 (2013)

    Article  MATH  MathSciNet  Google Scholar 

  32. Williams, R.: A new algorithm for optimal 2-constraint satisfaction and its implications. Theor. Comput. Sci. 348(2-3), 357–365 (2005)

    Article  MATH  Google Scholar 

  33. Williams, R.: Non-uniform ACC circuit lower bounds. In: Proceedings of the 26th Annual IEEE Conference on Computational Complexity (CCC), pp. 115–125 (2011)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Kyoto University, Yoshida Honmachi, Sakyo-ku, Kyoto, 606-8501, Japan

    Takayuki Sakai & Suguru Tamaki

  2. Seikei University, Musashino-shi, Tokyo, 180-8633, Japan

    Kazuhisa Seto

Authors
  1. Takayuki Sakai
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Kazuhisa Seto
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Suguru Tamaki
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Karlsruher Institut für Technologie (KIT), Am Fasanengarten 5, 76131, Karlsruhe, Germany

    Carsten Sinz

  2. TU Wien, Favoritenstraße 9-11, 1040, Wien, Austria

    Uwe Egly

Rights and permissions

Reprints and permissions

Copyright information

© 2014 Springer International Publishing Switzerland

About this paper

Cite this paper

Sakai, T., Seto, K., Tamaki, S. (2014). Solving Sparse Instances of Max SAT via Width Reduction and Greedy Restriction. In: Sinz, C., Egly, U. (eds) Theory and Applications of Satisfiability Testing – SAT 2014. SAT 2014. Lecture Notes in Computer Science, vol 8561. Springer, Cham. https://doi.org/10.1007/978-3-319-09284-3_4

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-09284-3_4

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-09283-6

  • Online ISBN: 978-3-319-09284-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation