Document Open Access Logo

Trustable Explainable AI - SAT to the Rescue (Invited Talk)

Author Joao Marques-Silva

PDF

File

Thumbnail PDF
PDF
LIPIcs.SAT.2026.2.pdf
  • Filesize: 0.66 MB
  • 10 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Automated reasoning
  • Theory of computation → Logic and verification
  • Theory of computation → Constraint and logic programming
Keywords
  • Explainable AI
  • Boolean Satisfiability

Metrics

Abstract

Explainable Artificial Intelligence (XAI) aims to help human decision makers in understanding the operation of complex AI models. However, many XAI solutions, based on non-symbolic methods, offer no formal guarantees and can produce erroneous results. In contrast, logic-based XAI guarantees the rigor of computed explanations, and this is paramount in high-stakes uses of AI. This talk overviews several flagship applications of Boolean satisfiability (SAT) solvers in reasoning about logic-based explanations.

Cite As Get BibTex

Joao Marques-Silva. Trustable Explainable AI - SAT to the Rescue (Invited Talk). In 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 377, pp. 2:1-2:10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.SAT.2026.2

Author Details

Joao Marques-Silva
  • ICREA & University of Lleida, Spain

Funding

  • Marques-Silva, Joao: Spanish Government grant PID2023-152814OB-I00.

Acknowledgements

Our work on logic-based XAI builds on the input of past collaborators, from the 1990s until the 2020s, at UofM, UofS, UCD, IST/INESC-ID, FCUL, IRIT/CNRS and ICREA/UdL.

References

  1. Leila Amgoud. Explaining black-box classifiers: Properties and functions. Int. J. Approx. Reason., 155:40-65, 2023. URL: https://doi.org/10.1016/J.IJAR.2023.01.004.
  2. Leila Amgoud and Jonathan Ben-Naim. Axiomatic foundations of explainability. In IJCAI, pages 636-642, 2022. URL: https://doi.org/10.24963/IJCAI.2022/90.
  3. Leila Amgoud, Martin C. Cooper, and Salim Debbaoui. Axiomatic characterisations of sample-based explainers. In ECAI, pages 770-777, 2024. URL: https://doi.org/10.3233/FAIA240561.
  4. Gilles Audemard, Steve Bellart, Jean-Marie Lagniez, and Pierre Marquis. Computing abductive explanations for boosted regression trees. In IJCAI, pages 3432-3441, 2023. URL: https://doi.org/10.24963/IJCAI.2023/382.
  5. Gilles Audemard, Frédéric Koriche, and Pierre Marquis. On tractable XAI queries based on compiled representations. In KR, pages 838-849, 2020. URL: https://doi.org/10.24963/KR.2020/86.
  6. Gilles Audemard, Jean-Marie Lagniez, and Pierre Marquis. On the computation of contrastive explanations for boosted regression trees. In ECAI, pages 1083-1091, 2024. URL: https://doi.org/10.3233/FAIA240600.
  7. Pablo Barceló, Alexander Kozachinskiy, Miguel Romero, Bernardo Subercaseaux, and José Verschae. Explaining k-nearest neighbors: Abductive and counterfactual explanations. Proc. ACM Manag. Data, 3(2):97:1-97:26, 2025. URL: https://doi.org/10.1145/3725234.
  8. Shahaf Bassan, Guy Amir, and Guy Katz. Local vs. global interpretability: A computational complexity perspective. In ICML, pages 3133-3167, 2024. URL: https://proceedings.mlr.press/v235/bassan24a.html.
  9. Anton Belov, Inês Lynce, and Joao Marques-Silva. Towards efficient MUS extraction. AI Commun., 25(2):97-116, 2012. URL: https://doi.org/10.3233/AIC-2012-0523.
  10. Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors. Handbook of Satisfiability - Second Edition, volume 336 of Frontiers in Artificial Intelligence and Applications. IOS Press, 2021. URL: https://doi.org/10.3233/FAIA336.
  11. Gagan Biradar, Yacine Izza, Elita Lobo, Vignesh Viswanathan, and Yair Zick. Axiomatic aggregations of abductive explanations. In AAAI, pages 11096-11104, 2024. URL: https://doi.org/10.1609/AAAI.V38I10.28986.
  12. Clément Carbonnel, Martin C. Cooper, and Joao Marques-Silva. Tractable explaining of multivariate decision trees. In KR, pages 127-135, 2023. URL: https://doi.org/10.24963/KR.2023/13.
  13. Martin C. Cooper and Leila Amgoud. Abductive explanations of classifiers under constraints: Complexity and properties. In ECAI, pages 469-476, 2023. URL: https://doi.org/10.3233/FAIA230305.
  14. Martin C. Cooper and Joao Marques-Silva. On the tractability of explaining decisions of classifiers. In CP, pages 21:1-21:18, 2021. URL: https://doi.org/10.4230/LIPIcs.CP.2021.21.
  15. Martin C. Cooper and Joao Marques-Silva. Tractability of explaining classifier decisions. Artif. Intell., 316:103841, 2023. URL: https://doi.org/10.1016/J.ARTINT.2022.103841.
  16. Adnan Darwiche. Logic for explainable AI. In LICS, pages 1-11, 2023. URL: https://doi.org/10.1109/LICS56636.2023.10175757.
  17. Adnan Darwiche and Chunxi Ji. On the computation of necessary and sufficient explanations. In AAAI, pages 5582-5591, 2022. URL: https://doi.org/10.1609/AAAI.V36I5.20498.
  18. Thomas Eiter and Georg Gottlob. The complexity of logic-based abduction. J. ACM, 42(1):3-42, 1995. URL: https://doi.org/10.1145/200836.200838.
  19. Hao Hu, Alexey Ignatiev, and Joao Marques-Silva. Efficient explanations for rule ensembles. In CP, 2026. Google Scholar
  20. Xuanxiang Huang, Martin C. Cooper, António Morgado, Jordi Planes, and Joao Marques-Silva. Feature necessity & relevancy in ML classifier explanations. In TACAS, pages 167-186, 2023. URL: https://doi.org/10.1007/978-3-031-30823-9_9.
  21. Xuanxiang Huang, Martin C. Cooper, António Morgado, Jordi Planes, and Joao Marques-Silva. Feature necessity and relevancy in machine learning explanations. J. Autom. Reason., 70(1):4, 2026. URL: https://doi.org/10.1007/S10817-026-09748-X.
  22. Xuanxiang Huang, Yacine Izza, Alexey Ignatiev, Martin C. Cooper, Nicholas Asher, and Joao Marques-Silva. Tractable explanations for d-DNNF classifiers. In AAAI, pages 5719-5728, 2022. URL: https://doi.org/10.1609/AAAI.V36I5.20514.
  23. Xuanxiang Huang, Yacine Izza, Alexey Ignatiev, and Joao Marques-Silva. On efficiently explaining graph-based classifiers. In KR, pages 356-367, 2021. URL: https://doi.org/10.24963/KR.2021/34.
  24. Xuanxiang Huang, Yacine Izza, Alexey Ignatiev, and Joao Marques-Silva. Uncovering bugs in formal explainers: A case study with PyXAI. CoRR, abs/2511.03169, 2025. URL: https://doi.org/10.48550/arXiv.2511.03169.
  25. Xuanxiang Huang, Yacine Izza, and Joao Marques-Silva. Solving explainability queries with quantification: The case of feature relevancy. In AAAI, pages 3996-4006, 2023. URL: https://doi.org/10.1609/AAAI.V37I4.25514.
  26. Xuanxiang Huang and Joao Marques-Silva. On the failings of shapley values for explainability. Int. J. Approx. Reason., 171:109112, 2024. URL: https://doi.org/10.1016/J.IJAR.2023.109112.
  27. Aurélie Hurault and Joao Marques-Silva. Certified logic-based explainable AI - the case of monotonic classifiers. In TAP, pages 51-67, 2023. URL: https://doi.org/10.1007/978-3-031-38828-6_4.
  28. Alexey Ignatiev. Towards trustable explainable AI. In IJCAI, pages 5154-5158, 2020. URL: https://doi.org/10.24963/IJCAI.2020/726.
  29. Alexey Ignatiev, Yacine Izza, Peter J. Stuckey, and Joao Marques-Silva. Using maxsat for efficient explanations of tree ensembles. In AAAI, pages 3776-3785, 2022. URL: https://doi.org/10.1609/AAAI.V36I4.20292.
  30. Alexey Ignatiev, Mikolás Janota, and Joao Marques-Silva. Quantified maximum satisfiability. Constraints, 21(2):277-302, 2016. URL: https://doi.org/10.1007/S10601-015-9195-9.
  31. Alexey Ignatiev and Joao Marques-Silva. SAT-based rigorous explanations for decision lists. In SAT, pages 251-269, 2021. URL: https://doi.org/10.1007/978-3-030-80223-3_18.
  32. Alexey Ignatiev, António Morgado, and Joao Marques-Silva. Propositional abduction with implicit hitting sets. In ECAI, pages 1327-1335, 2016. URL: https://doi.org/10.3233/978-1-61499-672-9-1327.
  33. Alexey Ignatiev, Nina Narodytska, Nicholas Asher, and Joao Marques-Silva. From contrastive to abductive explanations and back again. In AIxIA, pages 335-355, 2020. URL: https://doi.org/10.1007/978-3-030-77091-4_21.
  34. Alexey Ignatiev, Nina Narodytska, and Joao Marques-Silva. Abduction-based explanations for machine learning models. In AAAI, pages 1511-1519, 2019. URL: https://doi.org/10.1609/AAAI.V33I01.33011511.
  35. Alexey Ignatiev, Nina Narodytska, and Joao Marques-Silva. On relating explanations and adversarial examples. In NeurIPS, pages 15857-15867, 2019. URL: https://proceedings.neurips.cc/paper/2019/hash/7392ea4ca76ad2fb4c9c3b6a5c6e31e3-Abstract.html.
  36. Alexey Ignatiev, Nina Narodytska, and Joao Marques-Silva. On validating, repairing and refining heuristic ML explanations. CoRR, abs/1907.02509, 2019. URL: https://arxiv.org/abs/1907.02509.
  37. Yacine Izza, Xuanxiang Huang, Alexey Ignatiev, Nina Narodytska, Martin C. Cooper, and Joao Marques-Silva. On computing probabilistic abductive explanations. CoRR, abs/2212.05990, 2022. URL: https://doi.org/10.48550/arXiv.2212.05990.
  38. Yacine Izza, Xuanxiang Huang, Alexey Ignatiev, Nina Narodytska, Martin C. Cooper, and Joao Marques-Silva. On computing probabilistic abductive explanations. Int. J. Approx. Reason., 159:108939, 2023. URL: https://doi.org/10.1016/J.IJAR.2023.108939.
  39. Yacine Izza, Xuanxiang Huang, António Morgado, Jordi Planes, Alexey Ignatiev, and Joao Marques-Silva. Distance-restricted explanations: Theoretical underpinnings & efficient implementation. In KR, 2024. URL: https://doi.org/10.24963/KR.2024/45.
  40. Yacine Izza, Alexey Ignatiev, Xuanxiang Huang, Peter J. Stuckey, and Joao Marques-Silva. Rigorous explanations for tree ensembles. CoRR, abs/2603.29361, 2026. URL: https://doi.org/10.48550/arXiv.2603.29361.
  41. Yacine Izza, Alexey Ignatiev, and Joao Marques-Silva. On explaining decision trees. CoRR, abs/2010.11034, 2020. URL: https://arxiv.org/abs/2010.11034.
  42. Yacine Izza, Alexey Ignatiev, and Joao Marques-Silva. On tackling explanation redundancy in decision trees. J. Artif. Intell. Res., 75:261-321, 2022. URL: https://doi.org/10.1613/JAIR.1.13575.
  43. Yacine Izza, Alexey Ignatiev, Nina Narodytska, Martin C. Cooper, and Joao Marques-Silva. Efficient explanations with relevant sets. CoRR, abs/2106.00546, 2021. URL: https://arxiv.org/abs/2106.00546.
  44. Yacine Izza, Alexey Ignatiev, Nina Narodytska, Martin C. Cooper, and Joao Marques-Silva. Provably precise, succinct and efficient explanations for decision trees. CoRR, abs/2205.09569, 2022. URL: https://doi.org/10.48550/arXiv.2205.09569.
  45. Yacine Izza, Alexey Ignatiev, Sasha Rubin, Joao Marques-Silva, and Peter J. Stuckey. Most general explanations of tree ensembles. In IJCAI, pages 5463-5471, 2025. URL: https://doi.org/10.24963/IJCAI.2025/608.
  46. Yacine Izza, Alexey Ignatiev, Peter J. Stuckey, and Joao Marques-Silva. Delivering inflated explanations. In AAAI, pages 12744-12753, 2024. URL: https://doi.org/10.1609/AAAI.V38I11.29170.
  47. Yacine Izza and Joao Marques-Silva. On explaining random forests with SAT. In IJCAI, pages 2584-2591, 2021. URL: https://doi.org/10.24963/IJCAI.2021/356.
  48. Yacine Izza and Joao Marques-Silva. On computing relevant features for explaining NBCs. CoRR, abs/2207.04748, 2022. URL: https://doi.org/10.48550/arXiv.2207.04748.
  49. Mikolás Janota, William Klieber, Joao Marques-Silva, and Edmund M. Clarke. Solving QBF with counterexample guided refinement. In SAT, pages 114-128, 2012. URL: https://doi.org/10.1007/978-3-642-31612-8_10.
  50. Mikolás Janota, William Klieber, Joao Marques-Silva, and Edmund M. Clarke. Solving QBF with counterexample guided refinement. Artif. Intell., 234:1-25, 2016. URL: https://doi.org/10.1016/J.ARTINT.2016.01.004.
  51. Mikolás Janota and Joao Marques-Silva. Abstraction-based algorithm for 2QBF. In SAT, pages 230-244, 2011. URL: https://doi.org/10.1007/978-3-642-21581-0_19.
  52. Chunxi Ji and Adnan Darwiche. A new class of explanations for classifiers with non-binary features. In JELIA, pages 106-122, 2023. URL: https://doi.org/10.1007/978-3-031-43619-2_8.
  53. Guy Katz, Clark W. Barrett, David L. Dill, Kyle Julian, and Mykel J. Kochenderfer. Reluplex: An efficient SMT solver for verifying deep neural networks. In CAV, pages 97-117, 2017. URL: https://doi.org/10.1007/978-3-319-63387-9_5.
  54. Guy Katz, Derek A. Huang, Duligur Ibeling, Kyle Julian, Christopher Lazarus, Rachel Lim, Parth Shah, Shantanu Thakoor, Haoze Wu, Aleksandar Zeljic, David L. Dill, Mykel J. Kochenderfer, and Clark W. Barrett. The marabou framework for verification and analysis of deep neural networks. In CAV, pages 443-452, 2019. URL: https://doi.org/10.1007/978-3-030-25540-4_26.
  55. Faezeh Labbaf, Tomás Kolárik, Martin Blicha, Grigory Fedyukovich, Michael Wand, and Natasha Sharygina. Space explanations of neural network classification. In CAV, pages 287-303, 2025. URL: https://doi.org/10.1007/978-3-031-98682-6_15.
  56. Olivier Létoffé, Xuanxiang Huang, and Joao Marques-Silva. Towards trustable SHAP scores. In AAAI, pages 18198-18208, 2025. URL: https://doi.org/10.1609/AAAI.V39I17.34002.
  57. Mark H. Liffiton and Ammar Malik. Enumerating infeasibility: Finding multiple MUSes quickly. In CPAIOR, pages 160-175, 2013. URL: https://doi.org/10.1007/978-3-642-38171-3_11.
  58. Mark H. Liffiton, Alessandro Previti, Ammar Malik, and Joao Marques-Silva. Fast, flexible MUS enumeration. Constraints An Int. J., 21(2):223-250, 2016. URL: https://doi.org/10.1007/S10601-015-9183-0.
  59. Xinghan Liu and Emiliano Lorini. A unified logical framework for explanations in classifier systems. J. Log. Comput., 33(2):485-515, 2023. URL: https://doi.org/10.1093/LOGCOM/EXAC102.
  60. Scott M. Lundberg and Su-In Lee. A unified approach to interpreting model predictions. In NeurIPS, pages 4765-4774, 2017. URL: https://proceedings.neurips.cc/paper/2017/hash/8a20a8621978632d76c43dfd28b67767-Abstract.html.
  61. Olivier Létoffé, Xuanxiang Huang, and Joao Marques-Silva. Towards rigorous explainability by feature attribution. CoRR, abs/2604.15898, April 2026. URL: https://arxiv.org/abs/2604.15898.
  62. Joao Marques-Silva. Logic-based explainability in machine learning. In Reasoning Web, pages 24-104, 2022. URL: https://doi.org/10.1007/978-3-031-31414-8_2.
  63. Joao Marques-Silva. Disproving XAI myths with formal methods - initial results. In ICECCS, pages 12-21, 2023. URL: https://doi.org/10.1109/ICECCS59891.2023.00012.
  64. Joao Marques-Silva. Logic-based explainability: Past, present and future. In ISoLA, pages 181-204, 2024. URL: https://doi.org/10.1007/978-3-031-75387-9_12.
  65. Joao Marques-Silva, Thomas Gerspacher, Martin C. Cooper, Alexey Ignatiev, and Nina Narodytska. Explaining naive bayes and other linear classifiers with polynomial time and delay. In NeurIPS, 2020. URL: https://proceedings.neurips.cc/paper/2020/hash/eccd2a86bae4728b38627162ba297828-Abstract.html.
  66. Joao Marques-Silva, Thomas Gerspacher, Martin C. Cooper, Alexey Ignatiev, and Nina Narodytska. Explanations for monotonic classifiers. In ICML, pages 7469-7479, 2021. URL: http://proceedings.mlr.press/v139/marques-silva21a.html.
  67. Joao Marques-Silva, Federico Heras, Mikolás Janota, Alessandro Previti, and Anton Belov. On computing minimal correction subsets. In IJCAI, pages 615-622, 2013. URL: http://www.aaai.org/ocs/index.php/IJCAI/IJCAI13/paper/view/6922.
  68. Joao Marques-Silva and Xuanxiang Huang. Explainability is Not a game. Commun. ACM, 67(7):66-75, 2024. URL: https://doi.org/10.1145/3635301.
  69. Joao Marques-Silva, Xuanxiang Huang, and Olivier Létoffé. The explanation game - rekindled (extended version). CoRR, abs/2501.11429, 2025. URL: https://doi.org/10.48550/arXiv.2501.11429.
  70. Joao Marques-Silva and Alexey Ignatiev. Delivering trustworthy AI through formal XAI. In AAAI, pages 12342-12350, 2022. URL: https://doi.org/10.1609/AAAI.V36I11.21499.
  71. Joao Marques-Silva and Alexey Ignatiev. No silver bullet: interpretable ML models must be explained. Frontiers Artif. Intell., 6, 2023. URL: https://doi.org/10.3389/FRAI.2023.1128212.
  72. Joao Marques-Silva, Mikolás Janota, and Anton Belov. Minimal sets over monotone predicates in boolean formulae. In CAV, pages 592-607, 2013. URL: https://doi.org/10.1007/978-3-642-39799-8_39.
  73. Joao Marques-Silva, Mikolás Janota, and Carlos Mencía. Minimal sets on propositional formulae. problems and reductions. Artif. Intell., 252:22-50, 2017. URL: https://doi.org/10.1016/J.ARTINT.2017.07.005.
  74. Joao Marques-Silva, Jairo A. Lefebre-Lobaina, and Maria Vanina Martinez. Efficient and rigorous model-agnostic explanations. In IJCAI, pages 2637-2646, 2025. URL: https://doi.org/10.24963/IJCAI.2025/294.
  75. Joao Marques-Silva and Inês Lynce. On improving MUS extraction algorithms. In SAT, pages 159-173, 2011. URL: https://doi.org/10.1007/978-3-642-21581-0_14.
  76. Hayden McTavish, Zachery Boner, Jon Donnelly, Margo I. Seltzer, and Cynthia Rudin. Leveraging predictive equivalence in decision trees. In ICML, 2025. URL: https://proceedings.mlr.press/v267/mctavish25a.html.
  77. Carlos Mencía, Raúl Mencía, Ramon Béjar, and Joao Marques-Silva. Model-agnostic explanations by consensus. In KR, 2026. Google Scholar
  78. Carlos Mencía, Alessandro Previti, and Joao Marques-Silva. Literal-based MCS extraction. In IJCAI, pages 1973-1979, 2015. URL: http://ijcai.org/Abstract/15/280.
  79. Christoph Molnar. Interpretable machine learning. Lulu.com, 2020. Google Scholar
  80. Andreas Niskanen, Jeremias Berg, and Matti Järvisalo. Incremental maximum satisfiability. In SAT, pages 14:1-14:19, 2022. URL: https://doi.org/10.4230/LIPIcs.SAT.2022.14.
  81. Alessandro Previti and Joao Marques-Silva. Partial MUS enumeration. In AAAI, 2013. URL: https://doi.org/10.1609/AAAI.V27I1.8657.
  82. Raymond Reiter. A theory of diagnosis from first principles. Artif. Intell., 32(1):57-95, 1987. URL: https://doi.org/10.1016/0004-3702(87)90062-2.
  83. Marco Túlio Ribeiro, Sameer Singh, and Carlos Guestrin. "why should I trust you?": Explaining the predictions of any classifier. In KDD, pages 1135-1144, 2016. URL: https://doi.org/10.1145/2939672.2939778.
  84. Marco Túlio Ribeiro, Sameer Singh, and Carlos Guestrin. Anchors: High-precision model-agnostic explanations. In AAAI, pages 1527-1535, 2018. URL: https://doi.org/10.1609/AAAI.V32I1.11491.
  85. Cynthia Rudin. Stop explaining black box machine learning models for high stakes decisions and use interpretable models instead. Nature Machine Intelligence, 1(5):206-215, 2019. URL: https://doi.org/10.1038/S42256-019-0048-X.
  86. Cynthia Rudin, Chaofan Chen, Zhi Chen, Haiyang Huang, Lesia Semenova, and Chudi Zhong. Interpretable machine learning: Fundamental principles and 10 grand challenges. Statistics Surveys, 16:1-85, 2022. Google Scholar
  87. Cynthia Rudin and Yaron Shaposhnik. Globally-consistent rule-based summary-explanations for machine learning models: Application to credit-risk evaluation. J. Mach. Learn. Res., 24:16:1-16:44, 2023. URL: https://jmlr.org/papers/v24/21-0488.html.
  88. Lloyd S. Shapley. A value for n-person games. Contributions to the Theory of Games, 2(28):307-317, 1953. Google Scholar
  89. Lloyd S Shapley and Martin Shubik. A method for evaluating the distribution of power in a committee system. American political science review, 48(3):787-792, 1954. Google Scholar
  90. Andy Shih, Arthur Choi, and Adnan Darwiche. A symbolic approach to explaining bayesian network classifiers. In IJCAI, pages 5103-5111, 2018. URL: https://doi.org/10.24963/IJCAI.2018/708.
  91. Stephan Wäldchen, Jan MacDonald, Sascha Hauch, and Gitta Kutyniok. The computational complexity of understanding binary classifier decisions. J. Artif. Intell. Res., 70:351-387, 2021. URL: https://doi.org/10.1613/JAIR.1.12359.
  92. Min Wu, Haoze Wu, and Clark W. Barrett. VeriX: Towards verified explainability of deep neural networks. In NeurIPS, 2023. URL: http://papers.nips.cc/paper_files/paper/2023/hash/46907c2ff9fafd618095161d76461842-Abstract-Conference.html.
  93. Jinqiang Yu, Graham Farr, Alexey Ignatiev, and Peter J. Stuckey. Anytime approximate formal feature attribution. In SAT, pages 30:1-30:23, 2024. URL: https://doi.org/10.4230/LIPIcs.SAT.2024.30.
  94. Jinqiang Yu, Alexey Ignatiev, Peter J. Stuckey, Nina Narodytska, and Joao Marques-Silva. Eliminating the impossible, whatever remains must be true: On extracting and applying background knowledge in the context of formal explanations. In AAAI, pages 4123-4131, 2023. URL: https://doi.org/10.1609/AAAI.V37I4.25528.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact