{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T19:22:14Z","timestamp":1743103334817,"version":"3.40.3"},"publisher-location":"Cham","reference-count":25,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030802226"},{"type":"electronic","value":"9783030802233"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"DOI":"10.1007\/978-3-030-80223-3_16","type":"book-chapter","created":{"date-parts":[[2021,7,1]],"date-time":"2021-07-01T14:13:49Z","timestamp":1625148829000},"page":"225-241","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Efficient SAT-Based Minimal Model Generation Methods for Modal Logic S5"],"prefix":"10.1007","author":[{"given":"Pei","family":"Huang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rundong","family":"Li","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Minghao","family":"Liu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Feifei","family":"Ma","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jian","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,7,2]]},"reference":[{"key":"16_CR1","unstructured":"Abate, P., Gor\u00e9, R., Widmann, F.: Cut-free single-pass tableaux for the logic of common knowledge. In: Workshop on Agents and Deduction at TABLEAUX. vol. 2007. Citeseer (2007)"},{"key":"16_CR2","unstructured":"Aguilera, J.P., Fern\u00e1ndez-Duque, D.: Verification logic: an arithmetical interpretation for negative introspection. In: Advances in Modal Logic 11, proceedings of the 11th conference on Advances in Modal Logic, held in Budapest, Hungary, August 30 - September 2, 2016. pp. 1\u201320 (2016)"},{"key":"16_CR3","unstructured":"Audemard, G., Simon, L.: Predicting learnt clauses quality in modern SAT solvers. In: IJCAI 2009, Proceedings of the 21st International Joint Conference on Artificial Intelligence, Pasadena, California, USA, 11\u201317 July 2009, pp. 399\u2013404 (2009)"},{"issue":"3","key":"16_CR4","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1023\/A:1006249507577","volume":"24","author":"P Balsiger","year":"2000","unstructured":"Balsiger, P., Heuerding, A., Schwendimann, S.: A benchmark method for the propositional modal logics k, kt, S4. J. Autom. Reason. 24(3), 297\u2013317 (2000)","journal-title":"J. Autom. Reason."},{"key":"16_CR5","unstructured":"Bienvenu, M., Fargier, H., Marquis, P.: Knowledge compilation in the modal logic S5. In: Proceedings of the Twenty-Fourth AAAI Conference on Artificial Intelligence, AAAI 2010, Atlanta, Georgia, USA, July 11\u201315, 2010 (2010)"},{"key":"16_CR6","doi-asserted-by":"crossref","unstructured":"Caridroit, T., Lagniez, J., Berre, D.L., de Lima, T., Montmirail, V.: A SAT-based approach for solving the modal logic S5-satisfiability problem. In: Proceedings of the Thirty-First AAAI Conference on Artificial Intelligence, 4\u20139 February 2017, San Francisco, California, USA. pp. 3864\u20133870 (2017)","DOI":"10.1609\/aaai.v31i1.11128"},{"issue":"1","key":"16_CR7","doi-asserted-by":"publisher","first-page":"86","DOI":"10.1007\/s11704-018-7107-z","volume":"13","author":"Y Chu","year":"2019","unstructured":"Chu, Y., Luo, C., Cai, S., You, H.: Empirical investigation of stochastic local search for maximum satisfiability. Frontiers Comput. Sci. 13(1), 86\u201398 (2019). https:\/\/doi.org\/10.1007\/s11704-018-7107-z","journal-title":"Frontiers Comput. Sci."},{"key":"16_CR8","doi-asserted-by":"crossref","unstructured":"Fagin, R., Halpern, J.Y., Moses, Y., Vardi, M.: Reasoning about knowledge. MIT press, Cambridge (2004)","DOI":"10.7551\/mitpress\/5803.001.0001"},{"issue":"1\u20133","key":"16_CR9","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1016\/S0168-0072(98)00034-7","volume":"96","author":"M Fitting","year":"1999","unstructured":"Fitting, M.: A simple propositional S5 tableau system. Ann. Pure Appl. Log. 96(1\u20133), 107\u2013115 (1999)","journal-title":"Ann. Pure Appl. Log."},{"key":"16_CR10","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/10722086_2","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"M Fitting","year":"2000","unstructured":"Fitting, M.: Modality and databases. In: Dyckhoff, R. (ed.) TABLEAUX 2000. LNCS (LNAI), vol. 1847, pp. 19\u201339. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/10722086_2"},{"key":"16_CR11","doi-asserted-by":"crossref","unstructured":"Goranko, V., Otto, M.: Model theory of modal logic. In: Handbook of Modal Logic, pp. 249\u2013329 (2007)","DOI":"10.1016\/S1570-2464(07)80008-5"},{"key":"16_CR12","unstructured":"Grossi, D., Rey, S.: Credulous acceptability, poison games and modal logic. In: Proceedings of the 18th International Conference on Autonomous Agents and MultiAgent Systems, AAMAS 2019, Montreal, QC, Canada, 13\u201317 May 2019, pp. 1994\u20131996 (2019)"},{"issue":"1","key":"16_CR13","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/s00446-013-0202-3","volume":"28","author":"L Hella","year":"2013","unstructured":"Hella, L., et al.: Weak models of distributed computing, with connections to modal logic. Distrib. Comput. 28(1), 31\u201353 (2013). https:\/\/doi.org\/10.1007\/s00446-013-0202-3","journal-title":"Distrib. Comput."},{"key":"16_CR14","doi-asserted-by":"crossref","unstructured":"Huang, P., Liu, M., Wang, P., Zhang, W., Ma, F., Zhang, J.: Solving the satisfiability problem of modal logic S5 guided by graph coloring. In: Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence, IJCAI 2019, Macao, China, 10\u201316 August 2019. pp. 1093\u20131100 (2019)","DOI":"10.24963\/ijcai.2019\/153"},{"issue":"1","key":"16_CR15","first-page":"53","volume":"11","author":"A Ignatiev","year":"2019","unstructured":"Ignatiev, A., Morgado, A., Marques-Silva, J.: RC2: an efficient maxsat solver. J. Satisf. Boolean Model. Comput. 11(1), 53\u201364 (2019)","journal-title":"J. Satisf. Boolean Model. Comput."},{"issue":"3","key":"16_CR16","doi-asserted-by":"publisher","first-page":"467","DOI":"10.1137\/0206033","volume":"6","author":"RE Ladner","year":"1977","unstructured":"Ladner, R.E.: The computational complexity of provability in systems of modal propositional logic. SIAM J. Comput. 6(3), 467\u2013480 (1977)","journal-title":"SIAM J. Comput."},{"key":"16_CR17","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-319-94205-6_1","volume-title":"Automated Reasoning","author":"J-M Lagniez","year":"2018","unstructured":"Lagniez, J.-M., Le Berre, D., de Lima, T., Montmirail, V.: An assumption-based approach for solving the minimal S5-satisfiability problem. In: Galmiche, D., Schulz, S., Sebastiani, R. (eds.) IJCAR 2018. LNCS (LNAI), vol. 10900, pp. 1\u201318. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-94205-6_1"},{"key":"16_CR18","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"446","DOI":"10.1007\/978-3-030-29026-9_25","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"I Leu\u015ftean","year":"2019","unstructured":"Leu\u015ftean, I., Moang\u0103, N., \u015eerb\u0103nu\u0163\u0103, T.F.: Operational semantics and program verification using many-sorted hybrid modal logic. In: Cerrito, S., Popescu, A. (eds.) TABLEAUX 2019. LNCS (LNAI), vol. 11714, pp. 446\u2013476. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-29026-9_25"},{"key":"16_CR19","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1007\/3-540-48754-9_2","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"F Massacci","year":"1999","unstructured":"Massacci, F.: Design and results of the tableaux-99 non-classical (Modal) systems comparison. In: Murray, N.V. (ed.) TABLEAUX 1999. LNCS (LNAI), vol. 1617, pp. 14\u201318. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48754-9_2"},{"key":"16_CR20","unstructured":"Niveau, A., Zanuttini, B.: Efficient representations for the modal logic S5. In: Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence, IJCAI 2016, New York, 9\u201315 July 2016. pp. 1223\u20131229 (2016)"},{"key":"16_CR21","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1016\/j.entcs.2011.10.013","volume":"278","author":"F Papacchini","year":"2011","unstructured":"Papacchini, F., Schmidt, R.A.: A tableau calculus for minimal modal model generation. Electron. Notes Theor. Comput. Sci. 278, 159\u2013172 (2011)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"16_CR22","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"381","DOI":"10.1007\/978-3-319-08587-6_30","volume-title":"Automated Reasoning","author":"F Papacchini","year":"2014","unstructured":"Papacchini, F., Schmidt, R.A.: Terminating minimal model generation procedures for propositional modal logics. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS (LNAI), vol. 8562, pp. 381\u2013395. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08587-6_30"},{"key":"16_CR23","doi-asserted-by":"publisher","first-page":"351","DOI":"10.1613\/jair.1166","volume":"18","author":"PF Patel-Schneider","year":"2003","unstructured":"Patel-Schneider, P.F., Sebastiani, R.: A new general method to generate random modal formulae for testing decision procedures. J. Artif. Intell. Res. 18, 351\u2013389 (2003)","journal-title":"J. Artif. Intell. Res."},{"issue":"18","key":"16_CR24","doi-asserted-by":"publisher","first-page":"2281","DOI":"10.1016\/j.dam.2011.08.005","volume":"159","author":"M Soto","year":"2011","unstructured":"Soto, M., Rossi, A., Sevaux, M.: Three new upper bounds on the chromatic number. Discret. Appl. Math. 159(18), 2281\u20132289 (2011)","journal-title":"Discret. Appl. Math."},{"key":"16_CR25","unstructured":"Wan, H., Yang, R., Fang, L., Liu, Y., Xu, H.: A complete epistemic planner without the epistemic closed world assumption. In: Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, IJCAI 2015, Buenos Aires, Argentina, 25\u201331 July 2015. pp. 3257\u20133263 (2015)"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing \u2013 SAT 2021"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-80223-3_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,2]],"date-time":"2023-01-02T09:42:41Z","timestamp":1672652561000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-80223-3_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030802226","9783030802233"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-80223-3_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"2 July 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SAT","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Theory and Applications of Satisfiability Testing","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Barcelona","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Spain","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"5 July 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 July 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"sat2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.iiia.csic.es\/sat2021\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}