{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T10:00:44Z","timestamp":1776333644390,"version":"3.51.2"},"publisher-location":"Cham","reference-count":40,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032227737","type":"print"},{"value":"9783032227744","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-3-032-22774-4_6","type":"book-chapter","created":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T09:22:18Z","timestamp":1776331338000},"page":"107-125","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Formally Correct Search for Interpretable DNFs"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0003-0951-0752","authenticated-orcid":false,"given":"Imane","family":"Bousdira","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4853-053X","authenticated-orcid":false,"given":"Martin","family":"Cooper","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3266-6080","authenticated-orcid":false,"given":"Aur\u00e9lie","family":"Hurault","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2026,4,17]]},"reference":[{"key":"6_CR1","doi-asserted-by":"publisher","unstructured":"Amgoud, L., Ben-Naim, J.: Axiomatic foundations of explainability. In: Raedt, L.D. (ed.) IJCAI. pp. 636\u2013642. ijcai.org (2022). https:\/\/doi.org\/10.24963\/ijcai.2022\/90","DOI":"10.24963\/ijcai.2022\/90"},{"key":"6_CR2","doi-asserted-by":"publisher","unstructured":"Amgoud, L., Cooper, M.C., Debbaoui, S.: Axiomatic characterisations of sample-based explainers. In: ECAI. Frontiers in Artificial Intelligence and Applications, vol.\u00a0392, pp. 770\u2013777. IOS Press (2024). https:\/\/doi.org\/10.3233\/FAIA240561","DOI":"10.3233\/FAIA240561"},{"key":"6_CR3","unstructured":"Audemard, G., Lagniez, J., Marquis, P., Szczepanski, N.: Deriving provably correct explanations for decision trees: The impact of domain theories. In: IJCAI. pp. 3688\u20133696. ijcai.org (2024), https:\/\/www.ijcai.org\/proceedings\/2024\/408"},{"key":"6_CR4","doi-asserted-by":"publisher","unstructured":"Avellaneda, F.: Efficient inference of optimal decision trees. In: AAAI. pp. 3195\u20133202. AAAI Press (2020). https:\/\/doi.org\/10.1609\/AAAI.V34I04.5717","DOI":"10.1609\/AAAI.V34I04.5717"},{"key":"6_CR5","doi-asserted-by":"publisher","unstructured":"Avellaneda, F.: Learning optimal oblique decision trees with (max)sat. In: IJCAI 2025. pp. 2558\u20132565. ijcai.org (2025). https:\/\/doi.org\/10.24963\/IJCAI.2025\/285","DOI":"10.24963\/IJCAI.2025\/285"},{"key":"6_CR6","unstructured":"Barcel\u00f3, P., Monet, M., P\u00e9rez, J., Subercaseaux, B.: Model interpretability through the lens of computational complexity. In: Larochelle, H., Ranzato, M., Hadsell, R., Balcan, M., Lin, H. (eds.) NeurIPS (2020), https:\/\/proceedings.neurips.cc\/paper\/2020\/hash\/b1adda14824f50ef24ff1c05bb66faf3-Abstract.html"},{"key":"6_CR7","unstructured":"Bassan, S., Amir, G., Katz, G.: Local vs. global interpretability: A computational complexity perspective. In: ICML. Proceedings of Machine Learning Research, vol.\u00a0235, pp. 3133\u20133167 (2024), https:\/\/openreview.net\/forum?id=veEjiN2w9F"},{"key":"6_CR8","doi-asserted-by":"publisher","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development - Coq\u2019Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. An EATCS Series, Springer (2004). https:\/\/doi.org\/10.1007\/978-3-662-07964-5","DOI":"10.1007\/978-3-662-07964-5"},{"key":"6_CR9","doi-asserted-by":"publisher","unstructured":"Bessiere, C., Hebrard, E., O\u2019Sullivan, B.: Minimising decision tree size as combinatorial optimisation. In: Gent, I.P. (ed.) CP 2009. LNCS, vol.\u00a05732, pp. 173\u2013187. Springer (2009). https:\/\/doi.org\/10.1007\/978-3-642-04244-7_16","DOI":"10.1007\/978-3-642-04244-7_16"},{"key":"6_CR10","unstructured":"Bobot, F., Filli\u00e2tre, J.C., March\u00e9, C., Paskevich, A.: Why3: Shepherd your herd of provers. In: Boogie 2011: First International Workshop on Intermediate Verification Languages. pp. 53\u201364 (2011)"},{"key":"6_CR11","doi-asserted-by":"publisher","unstructured":"Cooper, M.C., Bousdira, I., Carbonnel, C.: Interpretable DNFs. In: IJCAI. pp. 4985\u20134993 (2025). https:\/\/doi.org\/10.24963\/IJCAI.2025\/555","DOI":"10.24963\/IJCAI.2025\/555"},{"key":"6_CR12","doi-asserted-by":"publisher","unstructured":"Cooper, M.C., Marques-Silva, J.: Tractability of explaining classifier decisions. Artif. Intell. 316 (2023). https:\/\/doi.org\/10.1016\/J.ARTINT.2022.103841","DOI":"10.1016\/J.ARTINT.2022.103841"},{"key":"6_CR13","unstructured":"Demirovic, E., Hebrard, E., Jean, L.: Blossom: an anytime algorithm for computing optimal decision trees. In: Krause, A., Brunskill, E., Cho, K., Engelhardt, B., Sabato, S., Scarlett, J. (eds.) ICML. vol.\u00a0202, pp. 7533\u20137562. PMLR (2023)"},{"key":"6_CR14","doi-asserted-by":"publisher","unstructured":"Feldman, V.: Hardness of approximate two-level logic minimization and PAC learning with membership queries. J. Comput. Syst. Sci. 75(1), 13\u201326 (2009). https:\/\/doi.org\/10.1016\/J.JCSS.2008.07.007","DOI":"10.1016\/J.JCSS.2008.07.007"},{"key":"6_CR15","doi-asserted-by":"publisher","unstructured":"Hu, H., Siala, M., Hebrard, E., Huguet, M.: Learning optimal decision trees with MaxSAT and its integration in AdaBoost. In: Bessiere, C. (ed.) IJCAI. pp. 1170\u20131176 (2020). https:\/\/doi.org\/10.24963\/IJCAI.2020\/163","DOI":"10.24963\/IJCAI.2020\/163"},{"key":"6_CR16","doi-asserted-by":"publisher","unstructured":"Hurault, A., Marques-Silva, J.: Certified logic-based explainable AI - the case of monotonic classifiers. In: Prevosto, V., Seceleanu, C. (eds.) Tests and Proofs - 17th International Conference, TAP 2023. LNCS, vol. 14066, pp. 51\u201367. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-38828-6_4","DOI":"10.1007\/978-3-031-38828-6_4"},{"key":"6_CR17","doi-asserted-by":"publisher","unstructured":"Ignatiev, A., Lam, E., Stuckey, P.J., Marques-Silva, J.: A scalable two stage approach to computing optimal decision sets. In: AAAI. pp. 3806\u20133814. AAAI Press (2021). https:\/\/doi.org\/10.1609\/AAAI.V35I5.16498","DOI":"10.1609\/AAAI.V35I5.16498"},{"key":"6_CR18","doi-asserted-by":"publisher","unstructured":"Ignatiev, A., Marques-Silva, J., Narodytska, N., Stuckey, P.J.: Reasoning-based learning of interpretable ML models. In: Zhou, Z. (ed.) IJCAI. pp. 4458\u20134465. ijcai.org (2021). https:\/\/doi.org\/10.24963\/IJCAI.2021\/608","DOI":"10.24963\/IJCAI.2021\/608"},{"key":"6_CR19","doi-asserted-by":"publisher","unstructured":"Ignatiev, A., Pereira, F., Narodytska, N., Marques-Silva, J.: A sat-based approach to learn explainable decision sets. In: Galmiche, D., Schulz, S., Sebastiani, R. (eds.) IJCAR 2018. LNCS, vol. 10900, pp. 627\u2013645. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-94205-6_41","DOI":"10.1007\/978-3-319-94205-6_41"},{"key":"6_CR20","doi-asserted-by":"crossref","unstructured":"Izza, Y., Ignatiev, A., Marques-Silva, J.: On tackling explanation redundancy in decision trees. J. Artif. Intell. Res. 75, 261\u2013321 (2022)","DOI":"10.1613\/jair.1.13575"},{"key":"6_CR21","doi-asserted-by":"publisher","unstructured":"Janota, M., Morgado, A.: SAT-based encodings for optimal decision trees with explicit paths. In: Pulina, L., Seidl, M. (eds.) SAT 2020. LNCS, vol. 12178, pp. 501\u2013518. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-51825-7_35","DOI":"10.1007\/978-3-030-51825-7_35"},{"key":"6_CR22","doi-asserted-by":"publisher","unstructured":"Klivans, A.R., Servedio, R.A.: Learning DNF in time $$2^{{\\tilde{{\\rm o}}}}({\\rm n}^{1\/3})$$. J. Comput. Syst. Sci. 68(2), 303\u2013318 (2004). https:\/\/doi.org\/10.1016\/J.JCSS.2003.07.007","DOI":"10.1016\/J.JCSS.2003.07.007"},{"key":"6_CR23","doi-asserted-by":"publisher","unstructured":"L\u00e9toff\u00e9, O., Huang, X., Marques-Silva, J.: Towards trustable SHAP scores. In: Walsh, T., Shah, J., Kolter, Z. (eds.) AAAI-25. pp. 18198\u201318208. AAAI Press (2025). https:\/\/doi.org\/10.1609\/AAAI.V39I17.34002","DOI":"10.1609\/AAAI.V39I17.34002"},{"key":"6_CR24","unstructured":"Lundberg, S.M., Lee, S.I.: A unified approach to interpreting model predictions. Curran Associates, Inc. (2017), http:\/\/papers.nips.cc\/paper\/7062-a-unified-approach-to-interpreting-model-predictions.pdf"},{"key":"6_CR25","doi-asserted-by":"publisher","unstructured":"Marques-Silva, J.: Disproving XAI myths with formal methods - initial results. In: A\u00eft-Ameur, Y., Khendek, F., M\u00e9ry, D. (eds.) ICECCS 2023. pp. 12\u201321. IEEE (2023). https:\/\/doi.org\/10.1109\/ICECCS59891.2023.00012","DOI":"10.1109\/ICECCS59891.2023.00012"},{"key":"6_CR26","unstructured":"Marques-Silva, J.: Logic-based explainability: Past, present & future. CoRR abs\/2406.11873 (2024), https:\/\/doi.org\/10.48550\/arXiv.2406.11873"},{"key":"6_CR27","doi-asserted-by":"publisher","unstructured":"Marques-Silva, J., Huang, X.: Explainability is Not a game. Commun. ACM 67(7), 66\u201375 (2024). https:\/\/doi.org\/10.1145\/3635301","DOI":"10.1145\/3635301"},{"key":"6_CR28","doi-asserted-by":"publisher","unstructured":"McCluskey, E.J.: Minimization of boolean functions. The Bell System Technical Journal 35(6), 1417\u20131444 (1956). https:\/\/doi.org\/10.1002\/j.1538-7305.1956.tb03835.x","DOI":"10.1002\/j.1538-7305.1956.tb03835.x"},{"key":"6_CR29","doi-asserted-by":"crossref","unstructured":"de\u00a0Moura, L., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. pp. 337\u2013340. Springer (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"6_CR30","doi-asserted-by":"publisher","unstructured":"Narodytska, N., Ignatiev, A., Pereira, F., Marques-Silva, J.: Learning optimal decision trees with SAT. In: Lang, J. (ed.) IJCAI 2018. pp. 1362\u20131368. ijcai.org (2018). https:\/\/doi.org\/10.24963\/IJCAI.2018\/189","DOI":"10.24963\/IJCAI.2018\/189"},{"key":"6_CR31","doi-asserted-by":"publisher","unstructured":"Pitt, L., Valiant, L.G.: Computational limitations on learning from examples. J. ACM 35(4), 965\u2013984 (1988). https:\/\/doi.org\/10.1145\/48014.63140","DOI":"10.1145\/48014.63140"},{"key":"6_CR32","doi-asserted-by":"crossref","unstructured":"Quine, W.V.: The problem of simplifying truth functions. The American Mathematical Monthly 59(8), 521\u2013531 (1952), http:\/\/www.jstor.org\/stable\/2308219","DOI":"10.1080\/00029890.1952.11988183"},{"key":"6_CR33","doi-asserted-by":"crossref","unstructured":"Ribeiro, M.T., Singh, S., Guestrin, C.: \u201cWhy should I trust you?\": Explaining the predictions of any classifier. In: Proceedings of the 22nd ACM SIGKDD International Conference on Knowledge Discovery and Data Mining. pp. 1135\u20131144 (2016)","DOI":"10.1145\/2939672.2939778"},{"key":"6_CR34","doi-asserted-by":"publisher","unstructured":"Ribeiro, M.T., Singh, S., Guestrin, C.: Anchors: High-precision model-agnostic explanations. In: McIlraith, S.A., Weinberger, K.Q. (eds.) AAAI. pp. 1527\u20131535. AAAI Press (2018). https:\/\/doi.org\/10.1609\/AAAI.V32I1.11491","DOI":"10.1609\/AAAI.V32I1.11491"},{"key":"6_CR35","doi-asserted-by":"publisher","unstructured":"Schidler, A., Szeider, S.: SAT-based decision tree learning for large data sets. J. Artif. Intell. Res. 80, 875\u2013918 (2024). https:\/\/doi.org\/10.1613\/JAIR.1.15956","DOI":"10.1613\/JAIR.1.15956"},{"key":"6_CR36","doi-asserted-by":"publisher","unstructured":"Shati, P., Cohen, E., McIlraith, S.A.: Sat-based learning of compact binary decision diagrams for classification. In: Yap, R.H.C. (ed.) CP 2023. LIPIcs, vol.\u00a0280, pp. 33:1\u201333:19. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2023). https:\/\/doi.org\/10.4230\/LIPICS.CP.2023.33","DOI":"10.4230\/LIPICS.CP.2023.33"},{"key":"6_CR37","doi-asserted-by":"crossref","unstructured":"Shih, A., Choi, A., Darwiche, A.: A symbolic approach to explaining bayesian network classifiers. In: IJCAI. pp. 5103\u20135111 (2018)","DOI":"10.24963\/ijcai.2018\/708"},{"key":"6_CR38","doi-asserted-by":"publisher","unstructured":"T\u00f6rnblom, J., Nadjm-Tehrani, S.: Formal verification of input-output mappings of tree ensembles. Sci. Comput. Program. 194, 102450 (2020). https:\/\/doi.org\/10.1016\/J.SCICO.2020.102450","DOI":"10.1016\/J.SCICO.2020.102450"},{"key":"6_CR39","doi-asserted-by":"crossref","unstructured":"Valiant, L.G.: A theory of the learnable. Communications of the ACM 27, 1134\u20131142 (1984)","DOI":"10.1145\/1968.1972"},{"key":"6_CR40","doi-asserted-by":"publisher","unstructured":"Yu, J., Ignatiev, A., Stuckey, P.J., Bodic, P.L.: Learning optimal decision sets and lists with SAT. J. Artif. Intell. Res. 72, 1251\u20131279 (2021). https:\/\/doi.org\/10.1613\/JAIR.1.12719","DOI":"10.1613\/JAIR.1.12719"}],"container-title":["Lecture Notes in Computer Science","Fundamental Approaches to Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-22774-4_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T09:22:31Z","timestamp":1776331351000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-22774-4_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032227737","9783032227744"],"references-count":40,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-22774-4_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"17 April 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FASE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Fundamental Approaches to Software Engineering","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Turin","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 April 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16 April 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fase2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2026\/conferences\/fase\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}