Skip to main content
SpringerLink
Log in

On Reducing Maximum Independent Set to Minimum Satisfiability

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

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

Abstract

Maximum Independent Set (MIS) is a well-known NP-hard graph problem, tightly related with other well known NP-hard graph problems, namely Minimum Vertex Cover (MVC) and Maximum Clique (MaxClq). This paper introduces a novel reduction of MIS into Minimum Satisfiability (MinSAT), thus, providing an alternative approach for solving MIS. The reduction naturally maps the vertices of a graph into clauses, without requiring the inclusion of hard clauses. Moreover, it is shown that the proposed reduction uses fewer variables and clauses than the existing alternative of mapping MIS into Maximum Satisfiability (MaxSAT). The paper develops a number of optimizations to the basic reduction, which significantly reduce the total number of variables used. The experimental evaluation considered the reductions described in the paper as well as existing state-of-the-art approaches. The results show that the proposed approaches based on MinSAT are competitive with existing approaches.

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. Andrade, D.V., Resende, M.G.C., Werneck, R.F.F.: Fast local search for the maximum independent set problem. J. Heuristics 18(4), 525–547 (2012)

    Article  Google Scholar 

  2. Ansotegui, C., Li, C.M., Manya, F., Zhu, Z.: A SAT-based approach to MinSAT. In: Escrig, M.T., Toledo, F.J., Golobardes, E. (eds.) CCIA 2002. LNCS (LNAI), vol. 2504, pp. 185–189. Springer, Heidelberg (2002)

    Google Scholar 

  3. Argelich, J., Li, C.-M., Manyà, F., Zhu, Z.: MinSAT versus MaxSAT for optimization problems. In: Schulte, C. (ed.) CP 2013. LNCS, vol. 8124, pp. 133–142. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  4. Battiti, R., Protasi, M.: Reactive local search for the maximum clique problem. Algorithmica 29(4), 610–637 (2001)

    Article  MATH  MathSciNet  Google Scholar 

  5. Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185. IOS Press (2009)

    Google Scholar 

  6. Bomze, I.M., Budinich, M., Pardalos, P.M., Pelillo, M.: The maximum clique problem. In: Handbook of Combinatorial Optimization, pp. 1–74. Springer (1999)

    Google Scholar 

  7. Cai, S., Su, K., Chen, Q.: EWLS: A new local search for minimum vertex cover. In: Fox, M., Poole, D. (eds.) AAAI. AAAI Press (2010)

    Google Scholar 

  8. Cai, S., Su, K., Luo, C., Sattar, A.: NuMVC: An efficient local search algorithm for minimum vertex cover. J. Artif. Intell. Res. (JAIR) 46, 687–716 (2013)

    Google Scholar 

  9. Cai, S., Su, K., Sattar, A.: Local search with edge weighting and configuration checking heuristics for minimum vertex cover. Artif. Intell. 175(9-10), 1672–1696 (2011)

    Article  MATH  MathSciNet  Google Scholar 

  10. Cai, S., Su, K., Sattar, A.: Two new local search strategies for minimum vertex cover. In: Hoffmann, J., Selman, B. (eds.) AAAI. AAAI Press (2012)

    Google Scholar 

  11. Carraghan, R., Pardalos, P.M.: An exact algorithm for the maximum clique problem. Operations Research Letters 9(6), 375–382 (1990)

    Article  MATH  Google Scholar 

  12. Chamaret, B., Josselin, S., Kuonen, P., Pizarroso, M., Salas-Manzanedo, B., Ubeda, S., Wagner, D.: Radio network optimization with maximum independent set search. In: IEEE 47th Vehicular Technology Conference, 1997, vol. 2, pp. 770–774 (May 1997)

    Google Scholar 

  13. Cormen, T.H., Leiserson, C.E., Rivest, R.L., Stein, C.: Introduction to algorithms. The MIT press (2009)

    Google Scholar 

  14. Coudert, O.: On solving covering problems. In: DAC, pp. 197–202 (1996)

    Google Scholar 

  15. Fahle, T.: Simple and fast: Improving a branch-and-bound algorithm for maximum clique. In: Möhring, R., Raman, R. (eds.) ESA 2002. LNCS, vol. 2461, pp. 485–498. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  16. Fu, Z., Malik, S.: On solving the partial MAX-SAT problem. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 252–265. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  17. Garey, M.R., Johnson, D.S.: Computers and Intractability: A Guide to the Theory of NP-Completeness. W. H. Freeman (1979)

    Google Scholar 

  18. Gavril, F.: Algorithms for minimum coloring, maximum clique, minimum covering by cliques, and maximum independent set of a chordal graph. SIAM J. Comput. 1(2), 180–187 (1972)

    Article  MATH  MathSciNet  Google Scholar 

  19. Heras, F., Morgado, A., Planes, J., Marques-Silva, J.: Iterative SAT solving for minimum satisfiability. In: ICTAI, pp. 922–927 (2012)

    Google Scholar 

  20. Heras, F., Morgado, A., Planes, J., Marques-Silva, J.: Iterative sat solving for minimum satisfiability. In: ICTAI, vol. 1, pp. 922–927. IEEE (2012)

    Google Scholar 

  21. Hopcroft, J.E., Motwani, R., Ullman, J.D.: Introduction to automata theory, languages, and computation - international edition, 2nd edn. Addison-Wesley (2003)

    Google Scholar 

  22. Ignatiev, A., Morgado, A., Planes, J., Marques-Silva, J.: Maximal falsifiability: Definitions, algorithms, and applications. In: LPAR, pp. 439–456 (2013)

    Google Scholar 

  23. Jain, K., Padhye, J., Padmanabhan, V.N., Qiu, L.: Impact of interference on multi-hop wireless network performance. Wireless Networks 11(4), 471–487 (2005)

    Article  Google Scholar 

  24. Johnson, D.S., Papadimitriou, C.H., Yannakakis, M.: On generating all maximal independent sets. Inf. Process. Lett. 27(3), 119–123 (1988)

    Article  MATH  MathSciNet  Google Scholar 

  25. Joseph, D., Meidanis, J., Tiwari, P.: Determining dna sequence similarity using maximum independent set algorithms for interval graphs. In: Nurmi, O., Ukkonen, E. (eds.) SWAT 1992. LNCS, vol. 621, pp. 326–337. Springer, Heidelberg (1992)

    Chapter  Google Scholar 

  26. Kohavi, Z.: Switching and Finite Automata Theory. Tata McGraw-Hill (1978)

    Google Scholar 

  27. Kohli, R., Krishnamurti, R., Mirchandani, P.: The minimum satisfiability problem. SIAM J. Discrete Math. 7(2), 275–283 (1994)

    Article  MATH  MathSciNet  Google Scholar 

  28. Konc, J., Janezic, D.: An improved branch and bound algorithm for the maximum clique problem. In: MATCH, vol. 58, pp. 560–590 (2007)

    Google Scholar 

  29. Kügel, A.: Natural Max-SAT encoding of Min-SAT. In: Hamadi, Y., Schoenauer, M. (eds.) LION 2012. LNCS, vol. 7219, pp. 431–436. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  30. Lawler, E.L., Lenstra, J.K., Kan, A.H.G.R.: Generating all maximal independent sets: NP-hardness and polynomial-time algorithms. SIAM J. Comput. 9(3), 558–565 (1980)

    Article  MATH  MathSciNet  Google Scholar 

  31. Li, C.M., Fang, Z., Xu, K.: Combining maxsat reasoning and incremental upper bound for the maximum clique problem. In: ICTAI, pp. 939–946 (2013)

    Google Scholar 

  32. Li, C.M., Manya, F.: MaxSAT, hard and soft constraints. In: Biere, et al. (eds.) [5], pp. 613–631

    Google Scholar 

  33. Li, C.M., Manyà, F., Planes, J.: New inference rules for max-sat. J. Artif. Intell. Res.(JAIR) 30, 321–359 (2007)

    Google Scholar 

  34. Li, C.M., Manyà, F., Quan, Z., Zhu, Z.: Exact MinSAT solving. In: Strichman, O., Szeider, S. (eds.) SAT 2010. LNCS, vol. 6175, pp. 363–368. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  35. Li, C.M., Quan, Z.: Combining graph structure exploitation and propositional reasoning for the maximum clique problem. In: ICTAI, pp. 344–351 (2010)

    Google Scholar 

  36. Li, C.M., Quan, Z.: An efficient branch-and-bound algorithm based on maxsat for the maximum clique problem. In: AAAI, vol. 10, pp. 128–133 (2010)

    Google Scholar 

  37. Li, C.M., Zhu, Z., Manya, F., Simon, L.: Minimum satisfiability and its applications. In: IJCAI, pp. 605–610 (2011)

    Google Scholar 

  38. Li, C.M., Zhu, Z., Manya, F., Simon, L.: Optimizing with minimum satisfiability. Artif. Intell. 190, 32–44 (2012)

    Article  MATH  MathSciNet  Google Scholar 

  39. Manquinho, V.M., Silva, J.P.M.: Satisfiability-based algorithms for boolean optimization. Ann. Math. Artif. Intell. 40(3-4), 353–372 (2004)

    Article  MATH  MathSciNet  Google Scholar 

  40. Marathe, M.V., Ravi, S.S.: On approximation algorithms for the minimum satisfiability problem. Inf. Process. Lett. 58(1), 23–29 (1996)

    Article  MATH  MathSciNet  Google Scholar 

  41. MiFuMaX — a Literate MaxSAT Solver, http://sat.inesc-id.pt/~mikolas/sw/mifumax/book.pdf (accessed: January 31, 2014)

  42. Östergård, P.R.J.: A fast algorithm for the maximum clique problem. Discrete Applied Mathematics 120(1-3), 197–207 (2002)

    Article  MATH  MathSciNet  Google Scholar 

  43. Pardalos, P.M., Xue, J.: The maximum clique problem. Journal of Global Optimization 4(3), 301–328 (1994)

    Article  MATH  MathSciNet  Google Scholar 

  44. Pullan, W.J.: Approximating the maximum vertex/edge weighted clique using local search. J. Heuristics 14(2), 117–134 (2008)

    Article  Google Scholar 

  45. Pullan, W.J., Hoos, H.H.: Dynamic local search for the maximum clique problem. J. Artif. Intell. Res. (JAIR) 25, 159–185 (2006)

    Google Scholar 

  46. Ramaswami, R., Sivarajan, K.N.: Routing and wavelength assignment in all-optical networks. IEEE/ACM Trans. Netw. 3(5), 489–500 (1995)

    Article  Google Scholar 

  47. Régin, J.-C.: Using constraint programming to solve the maximum clique problem. In: Rossi, F. (ed.) CP 2003. LNCS, vol. 2833, pp. 634–648. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  48. Resende, M.G.C., Feo, T.A., Smith, S.H.: Algorithm 787: Fortran subroutines for approximate solution of maximum independent set problems using GRASP. ACM Trans. Math. Softw. 24(4), 386–394 (1998)

    Article  MATH  Google Scholar 

  49. Robson, J.M.: Algorithms for maximum independent sets. J. Algorithms 7(3), 425–440 (1986)

    Article  MATH  MathSciNet  Google Scholar 

  50. San Segundo, P., Rodríguez-Losada, D., Jiménez, A.: An exact bit-parallel algorithm for the maximum clique problem. Computers & Operations Research 38(2), 571–581 (2011)

    Article  MATH  MathSciNet  Google Scholar 

  51. Tarjan, R.E., Trojanowski, A.E.: Finding a maximum independent set. SIAM J. Comput. 6(3), 537–546 (1977)

    Article  MATH  MathSciNet  Google Scholar 

  52. Tomita, E., Kameda, T.: An efficient branch-and-bound algorithm for finding a maximum clique with computational experiments. Journal of Global Optimization 37(1), 95–111 (2007)

    Article  MATH  MathSciNet  Google Scholar 

  53. Tomita, E., Seki, T.: An efficient branch-and-bound algorithm for finding a maximum clique. In: Calude, C.S., Dinneen, M.J., Vajnovszki, V. (eds.) DMTCS 2003. LNCS, vol. 2731, pp. 278–289. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  54. Tomita, E., Sutani, Y., Higashi, T., Takahashi, S., Wakatsuki, M.: A simple and faster branch-and-bound algorithm for finding a maximum clique. In: Rahman, M. S., Fujita, S. (eds.) WALCOM 2010. LNCS, vol. 5942, pp. 102–112. Springer, Heidelberg (2010)

    Google Scholar 

  55. Tseitin, G.S.: On the complexity of derivation in propositional calculus. Studies in Constructive Mathematics and Mathematical Logic 2(115-125), 10–13 (1968)

    Google Scholar 

  56. Tsukiyama, S., Ide, M., Ariyoshi, H., Shirakawa, I.: A new algorithm for generating all the maximal independent sets. SIAM J. Comput. 6(3), 505–517 (1977)

    Article  MATH  MathSciNet  Google Scholar 

  57. Villa, T., Kam, T., Brayton, R.K., Sangiovanni-Vincentelli, A.L.: Explicit and implicit algorithms for binate covering problems. IEEE Trans. on CAD of Integrated Circuits and Systems 16(7), 677–691 (1997)

    Article  Google Scholar 

  58. Zhu, Z., Li, C.-M., Manyà, F., Argelich, J.: A new encoding from MinSAT into MaxSAT. In: Milano, M. (ed.) CP 2012. LNCS, vol. 7514, pp. 455–463. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. IST/INESC-ID, Lisbon, Portugal

    Alexey Ignatiev, Antonio Morgado & Joao Marques-Silva

  2. University College Dublin, Ireland

    Joao Marques-Silva

  3. ISDCT SB RAS, Irkutsk, Russia

    Alexey Ignatiev

Authors
  1. Alexey Ignatiev
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Antonio Morgado
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Joao Marques-Silva
    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

Ignatiev, A., Morgado, A., Marques-Silva, J. (2014). On Reducing Maximum Independent Set to Minimum Satisfiability. 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_9

Download citation

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

  • 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