A Simple yet Efficient MCSes Enumeration with SAT Oracles

  • Miyuki KoshimuraEmail author
  • Ken Satoh
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 12033)


The enumeration of the maximal satisfiable subsets (MSSes) or the minimal correction subsets (MCSes) of conjunctive normal form (CNF) formulas is a cornerstone task in various AI domains. This paper presents an algorithm that enumerates all MCSes with SAT oracles. Our algorithm is simple because it follows a plain algorithm without any techniques that decrease the number of calls to a SAT oracle. The experimental results show that our proposed method is more efficient than state-of-the-art MCS enumerators on average to deal with Partial-MaxSAT instances.


Minimal correction subset Enumeration SAT oracle 



This work was supported by JSPS KAKENHI Grant Numbers JP17K00307 and JP19H04175.


  1. 1.
    Alviano, M.: Model enumeration in propositional circumscription via unsatisfiable core analysis. TPLP 17(5–6), 708–725 (2017)MathSciNetzbMATHGoogle Scholar
  2. 2.
    Argelich, J.: Max-sat formalisms with hard and soft constraints. AI Commun. 24(1), 101–103 (2011)MathSciNetCrossRefGoogle Scholar
  3. 3.
    Audemard, G., Lagniez, J.-M., Simon, L.: Improving glucose for incremental SAT solving with assumptions: application to MUS extraction. In: Järvisalo, M., Van Gelder, A. (eds.) SAT 2013. LNCS, vol. 7962, pp. 309–317. Springer, Heidelberg (2013). Scholar
  4. 4.
    Audemard, G., Simon, L.: Predicting learnt clauses quality in modern SAT solvers. In: Boutilier, C. (ed.) Proceedings of the 21st International Joint Conference on Artificial Intelligence, IJCAI 2009, Pasadena, California, USA, 11–17 July 2009, pp. 399–404 (2009)Google Scholar
  5. 5.
    Belov, A., Marques-Silva, J.: Accelerating MUS extraction with recursive model rotation. In: Bjesse, P., Slobodová, A. (eds.) International Conference on Formal Methods in Computer-Aided Design, FMCAD 2011, Austin, TX, USA, 30 October–02 November 2011, pp. 37–40. FMCAD Inc. (2011)Google Scholar
  6. 6.
    Berre, D.L., Parrain, A.: The sat4j library, release 2.2. JSAT 7(2–3), 59–64 (2010)Google Scholar
  7. 7.
    Birnbaum, E., Lozinskii, E.L.: Consistent subsets of inconsistent systems: structure and behaviour. J. Exp. Theor. Artif. Intell. 15(1), 25–46 (2003)CrossRefGoogle Scholar
  8. 8.
    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). Scholar
  9. 9.
    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). Scholar
  10. 10.
    Grégoire, É., Izza, Y., Lagniez, J.: Boosting MCSes enumeration. In: Lang, J. (ed.) [12], pp. 1309–1315Google Scholar
  11. 11.
    Koshimura, M., Nabeshima, H., Fujita, H., Hasegawa, R.: Minimal model generation with respect to an atom set. In: Peltier, N., Sofronie-Stokkermans, V. (eds.) Proceedings of the 7th International Workshop on First-Order Theorem Proving, FTP 2009, Oslo, Norway, 6–7 July 2009. CEUR Workshop Proceedings, vol. 556 (2009).
  12. 12.
    Lang, J. (ed.): Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence, IJCAI 2018, 13–19 July 2018, Stockholm, Sweden (2018).
  13. 13.
    Marques-Silva, J., Heras, F., Janota, M., Previti, A., Belov, A.: On computing minimal correction subsets. In: Rossi, F. (ed.) Proceedings of the 23rd International Joint Conference on Artificial Intelligence, IJCAI 2013, Beijing, China, 3–9 August 2013, pp. 615–622. IJCAI/AAAI (2013)Google Scholar
  14. 14.
    Marques-Silva, J., Janota, M., Ignatiev, A., Morgado, A.: Efficient model based diagnosis with maximum satisfiability. In: Yang, Q., Wooldridge, M.J. (eds.) Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, IJCAI 2015, Buenos Aires, Argentina, 25–31 July 2015, pp. 1966–1972. AAAI Press (2015)Google Scholar
  15. 15.
    Morgado, A., Liffiton, M., Marques-Silva, J.: MaxSAT-based MCS enumeration. In: Biere, A., Nahir, A., Vos, T. (eds.) HVC 2012. LNCS, vol. 7857, pp. 86–101. Springer, Heidelberg (2013). Scholar
  16. 16.
    Narodytska, N., Bjørner, N., Marinescu, M.V., Sagiv, M.: Core-guided minimal correction set and core enumeration. In: Lang, J. (ed.) [12], pp. 1353–1361Google Scholar
  17. 17.
    Previti, A., Mencía, C., Järvisalo, M., Marques-Silva, J.: Improving MCS enumeration via caching. In: Gaspers, S., Walsh, T. (eds.) SAT 2017. LNCS, vol. 10491, pp. 184–194. Springer, Cham (2017). Scholar
  18. 18.
    Previti, A., Mencía, C., Järvisalo, M., Marques-Silva, J.: Premise set caching for enumerating minimal correction subsets. In: McIlraith, S.A., Weinberger, K.Q. (eds.) Proceedings of the Thirty-Second AAAI Conference on Artificial Intelligence, (AAAI-18), the 30th Innovative Applications of Artificial Intelligence (IAAI-18), and the 8th AAAI Symposium on Educational Advances in Artificial Intelligence (EAAI-18), New Orleans, Louisiana, USA, 2–7 February 2018, pp. 6633–6640. AAAI Press (2018)Google Scholar
  19. 19.
    Reiter, R.: A theory of diagnosis from first principles. Artif. Intell. 32(1), 57–95 (1987)MathSciNetCrossRefGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2020

Authors and Affiliations

  1. 1.Kyushu UniversityFukuokaJapan
  2. 2.National Institute of InformaticsTokyoJapan

Personalised recommendations