Skip to main content
SpringerLink
Log in

Maximal Falsifiability

Definitions, Algorithms, and Applications

  • Conference paper
Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2013)

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

Abstract

Similarly to Maximum Satisfiability (MaxSAT), Minimum Satisfiability (MinSAT) is an optimization extension of the Boolean Satisfiability (SAT) decision problem. In recent years, both problems have been studied in terms of exact and approximation algorithms. In addition, the MaxSAT problem has been characterized in terms ofMaximal Satisfiable Subsets (MSSes) andMinimal Correction Subsets (MCSes), as well as Minimal Unsatisfiable Subsets (MUSes) and minimal hitting set dualization. However, and in contrast with MaxSAT, no such characterizations exist for MinSAT. This paper addresses this issue by casting the MinSAT problem in a more general framework. The paper studies Maximal Falsifiability, the problem of computing a subset-maximal set of clauses that can be simultaneously falsified, and shows that MinSAT corresponds to the complement of a largest subset-maximal set of simultaneously falsifiable clauses, i.e. the solution of the Maximum Falsifiability (MaxFalse) problem. Additional contributions of the paper include novel algorithms for Maximum and Maximal Falsifiability, as well as minimal hitting set dualization results for the MaxFalse problem. Moreover, the proposed algorithms are validated on practical instances.

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. Akkoyunlu, E.A.: The enumeration of maximal cliques of large graphs. SIAM J. Comput. 2(1), 1–6 (1973)

    Article  MathSciNet  MATH  Google Scholar 

  2. Angel, E., Bampis, E., Gourvès, L.: On the minimum hitting set of bundles problem. Theor. Comput. Sci. 410(45), 4534–4542 (2009)

    Article  MATH  Google Scholar 

  3. Ansótegui, C., Bonet, M.L., Levy, J.: A new algorithm for weighted partial maxsat. In: AAAI (2010)

    Google Scholar 

  4. Ansótegui, C., Bonet, M.L., Levy, J.: Sat-based maxsat algorithms. Artif. Intell. 196, 77–105 (2013)

    Article  MATH  Google Scholar 

  5. Ansotegui, C., Li, C.M., Manya, F., Zhu, Z.: A SAT-based approach to MinSAT. In: CCIA, pp. 185–189 (2012)

    Google Scholar 

  6. 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 

  7. Audemard, G., Simon, L.: Predicting learnt clauses quality in modern sat solvers. In: IJCAI, pp. 399–404 (2009)

    Google Scholar 

  8. Avidor, A., Zwick, U.: Approximating MIN k-SAT. In: Bose, P., Morin, P. (eds.) ISAAC 2002. LNCS, vol. 2518, pp. 465–475. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  9. Avidor, A., Zwick, U.: Approximating MIN 2-SAT and MIN 3-SAT. Theory Comput. Syst. 38(3), 329–345 (2005)

    Article  MathSciNet  MATH  Google Scholar 

  10. Bailey, J., Stuckey, P.J.: Discovery of minimal unsatisfiable subsets of constraints using hitting set dualization. In: Hermenegildo, M.V., Cabeza, D. (eds.) PADL 2004. LNCS, vol. 3350, pp. 174–186. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  11. 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 

  12. Birnbaum, E., Lozinskii, E.L.: Consistent subsets of inconsistent systems: structure and behaviour. J. Exp. Theor. Artif. Intell. 15(1), 25–46 (2003)

    Article  MATH  Google Scholar 

  13. Bourke, C., Deng, K., Scott, S.D., Schapire, R.E., Vinodchandran, N.V.: On reoptimizing multi-class classifiers. Machine Learning 71(2-3), 219–242 (2008)

    Article  Google Scholar 

  14. Brihaye, T., Bruyère, V., Doyen, L., Ducobu, M., Raskin, J.-F.: Antichain-based QBF solving. In: Bultan, T., Hsiung, P.-A. (eds.) ATVA 2011. LNCS, vol. 6996, pp. 183–197. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  15. Butman, A., Hermelin, D., Lewenstein, M., Rawitz, D.: Optimization problems in multiple-interval graphs. ACM Transactions on Algorithms 6(2) (2010)

    Google Scholar 

  16. Chen, T., Filkov, V., Skiena, S.: Identifying gene regulatory networks from experimental data. Parallel Computing 27(1-2), 141–162 (2001)

    Article  MATH  Google Scholar 

  17. Eén, N., Sörensson, N.: An Extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502–518. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  18. Gate, J., Stewart, I.A.: Frameworks for logically classifying polynomial-time optimisation problems. In: Ablayev, F., Mayr, E.W. (eds.) CSR 2010. LNCS, vol. 6072, pp. 120–131. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  19. Goldstein, A., Kolman, P., Zheng, J.: Minimum common string partition problem: Hardness and approximations. Electr. J. Comb. 12 (2005)

    Google Scholar 

  20. Hassin, R., Monnot, J., Segev, D.: Approximation algorithms and hardness results for labeled connectivity problems. J. Comb. Optim. 14(4), 437–453 (2007)

    Article  MathSciNet  MATH  Google Scholar 

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

    Google Scholar 

  22. Ignatiev, A., Janota, M., Marques-Silva, J.: Quantified maximum satisfiability: A core-guided approach. In: Järvisalo, M., Van Gelder, A. (eds.) SAT 2013. LNCS, vol. 7962, pp. 250–266. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  23. Interian, Y., Corvera, G., Selman, B., Williams, R.: Finding small unsatisfiable cores to prove unsatisfiability of QBFs. In: ISAIM (2006)

    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  MathSciNet  MATH  Google Scholar 

  25. Karp, R.M., Wigderson, A.: A fast parallel algorithm for the maximal independent set problem. J. ACM 32(4), 762–773 (1985)

    Article  MathSciNet  MATH  Google Scholar 

  26. Kohli, R., Krishnamurti, R., Jedidi, K.: Subset-conjunctive rules for breast cancer diagnosis. Discrete Applied Mathematics 154(7), 1100–1112 (2006)

    Article  MathSciNet  MATH  Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

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

    Chapter  Google Scholar 

  29. 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  MathSciNet  MATH  Google Scholar 

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

    Google Scholar 

  31. 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 

  32. 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 

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

    Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

  35. Liffiton, M.H., Mneimneh, M.N., Lynce, I., Andraus, Z.S., Marques-Silva, J., Sakallah, K.A.: A branch and bound algorithm for extracting smallest minimal unsatisfiable subformulas. Constraints 14(4), 415–442 (2009)

    Article  MathSciNet  MATH  Google Scholar 

  36. Liffiton, M.H., Sakallah, K.A.: Algorithms for computing minimal unsatisfiable subsets of constraints. J. Autom. Reasoning 40(1), 1–33 (2008)

    Article  MathSciNet  MATH  Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

  38. Marques-Silva, J., Heras, F., Janota, M., Previti, A., Belov, A.: On computing minimal correction subsets. In: IJCAI (to appear 2013)

    Google Scholar 

  39. Morgado, A., Heras, F., Liffiton, M.H., Planes, J., Marques-Silva, J.: Iterative and core-guided maxsat solving: A survey and assessment. Constraints 18(4), 478–534 (2013)

    Article  MathSciNet  Google Scholar 

  40. Morgado, A., Heras, F., Marques-Silva, J.: Improvements to core-guided binary search for maxsat. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 284–297. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  41. Morgado, A., Liffiton, M., Marques-Silva, J.: MaxSAT-based MCS enumeration. In: Biere, A., Nahir, A., Vos, T. (eds.) HVC. LNCS, vol. 7857, pp. 86–101. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  42. Nöhrer, A., Biere, A., Egyed, A.: Managing SAT inconsistencies with HUMUS. In: VaMoS, pp. 83–91 (2012)

    Google Scholar 

  43. Reiter, R.: A theory of diagnosis from first principles. Artif. Intell. 32(1), 57–95 (1987)

    Article  MathSciNet  MATH  Google Scholar 

  44. 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  MathSciNet  MATH  Google Scholar 

  45. 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. Universitat de Lleida, Spain

    Jordi Planes

  4. 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. Jordi Planes
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Joao Marques-Silva
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Microsoft Research, Redmond, WA, USA

    Ken McMillan

  2. University of Innsbruck, Austria

    Aart Middeldorp

  3. University of Manchester, UK

    Andrei Voronkov

Rights and permissions

Reprints and permissions

Copyright information

© 2013 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Ignatiev, A., Morgado, A., Planes, J., Marques-Silva, J. (2013). Maximal Falsifiability. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2013. Lecture Notes in Computer Science, vol 8312. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-45221-5_30

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-45221-5_30

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-45220-8

  • Online ISBN: 978-3-642-45221-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation