Document Open Access Logo

SMT with Uninterpreted Functions and Monotonicity Constraints in Systems Biology

Authors Ondřej Huvar , Martin Jonáš , Samuel Pastva

PDF

File

Thumbnail PDF
PDF
LIPIcs.SAT.2026.19.pdf
  • Filesize: 2.47 MB
  • 18 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Automated reasoning
Keywords
  • satisfiability modulo theories
  • uninterpreted function
  • monotonicity
  • boolean network
  • logic-based modeling

Metrics

Abstract

Uninterpreted functions are a key modeling tool for systems with unknown or abstracted components. Certain domains, such as systems biology, additionally impose monotonicity constraints on these components, requiring specific inputs to have a consistently positive or negative effect on the output. In this paper, we tackle the model inference problem for biological systems by applying the theory of uninterpreted functions with monotonicity constraints. We compare the performance of naive quantified encodings of the problem and the performance of the existing approach based on eager quantifier instantiation, which is based on the fact that a finite set of quantifier-free monotonicity lemmas is sufficient to encode the monotonicity of uninterpreted functions. Additionally, we consider a lazy variant of the approach that introduces the monotonicity lemmas on demand.
We evaluate the SMT-based approach to model inference using a large collection of systems biology benchmarks. The results demonstrate that the instantiation-based encodings significantly outperform quantified encodings, which typically struggle with large function arities and complex instances. As the key result, we show that our approach based on SMT with uninterpreted functions and monotonicity constraints significantly outperforms state-of-the-art domain-specific tools used in systems biology, such as the ASP-based Bonesis and the BDD-based AEON.

Cite As Get BibTex

Ondřej Huvar, Martin Jonáš, and Samuel Pastva. SMT with Uninterpreted Functions and Monotonicity Constraints in Systems Biology. In 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 377, pp. 19:1-19:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.SAT.2026.19

Author Details

Ondřej Huvar
  • Masaryk University, Brno, Czech Republic
Martin Jonáš
  • Masaryk University, Brno, Czech Republic
Samuel Pastva
  • Masaryk University, Brno, Czech Republic

Funding

The work was supported by the MUNI/JS/1954/2025 project of Masaryk University and the GA26-21507S project of the Czech Science Foundation.

Supplementary Materials

References

  1. Clark W. Barrett and Cesare Tinelli. Satisfiability Modulo Theories. In Handbook of Model Checking, pages 305-343. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-10575-8_11.
  2. Sam Bayless, Noah Bayless, Holger Hoos, and Alan Hu. Sat modulo monotonic theories. In Proceedings of the AAAI Conference on Artificial Intelligence, volume 29, 2015. Google Scholar
  3. Nikola Beneš, Luboš Brim, Ondřej Huvar, Samuel Pastva, and David Šafránek. Boolean network sketches: a unifying framework for logical model inference. Bioinformatics, 39(4):btad158, 2023. URL: https://doi.org/10.1093/bioinformatics/btad158.
  4. Nikola Beneš, Luboš Brim, Ondřej Huvar, Samuel Pastva, David Šafránek, and Eva Šmijáková. AEON. py: Python library for attractor analysis in asynchronous Boolean networks. Bioinformatics, 38(21):4978-4980, 2022. URL: https://doi.org/10.1093/bioinformatics/btac624.
  5. David Benque, Sam Bourton, Caitlin Cockerton, Byron Cook, Jasmin Fisher, Samin Ishtiaq, Nir Piterman, Alex Taylor, and Moshe Y. Vardi. Bma: Visual tool for modeling and analyzing biological networks. In Computer Aided Verification, pages 686-692. Springer Berlin Heidelberg, 2012. URL: https://doi.org/10.1007/978-3-642-31424-7_50.
  6. Nikolaj Bjørner, Clemens Eisenhofer, and Laura Kovács. Satisfiability modulo custom theories in Z3. In International Conference on Verification, Model Checking, and Abstract Interpretation, pages 91-105. Springer, 2023. URL: https://doi.org/10.1007/978-3-031-24950-1_5.
  7. Stéphanie Chevalier, Julia Becker, Yujuan Gui, Vincent Noël, Cui Su, Sascha Jung, Laurence Calzone, Andrei Zinovyev, Antonio Del Sol, Jun Pang, et al. Data-driven inference of Boolean networks from transcriptomes to predict cellular differentiation and reprogramming. npj Systems Biology and Applications, 11(1):105, 2025. Google Scholar
  8. Stéphanie Chevalier, Déborah Boyenval, Gustavo Magaña-López, Théo Roncalli, Athénaïs Vaginay, and Loïc Paulevé. Bonesis: a Python-based declarative environment for the verification, reprogramming, and synthesis of most permissive Boolean networks. In International Conference on Computational Methods in Systems Biology, pages 71-79. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-71671-3_6.
  9. Rachael Colley and Umberto Grandi. The spread of opinions via Boolean networks. In European Conference on Multi-Agent Systems, pages 96-115. Springer, 2022. URL: https://doi.org/10.1007/978-3-031-20614-6_6.
  10. Leonardo De Moura and Nikolaj Bjørner. Z3: An efficient SMT solver. In International conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 337-340. Springer, 2008. Google Scholar
  11. Daniela J. Di Bella, Ehsan Habibi, Robert R. Stickels, Gabriele Scalia, Juliana Brown, Payman Yadollahpour, Sung Min Yang, Catherine Abbate, Tommaso Biancalani, Evan Z. Macosko, Fei Chen, Aviv Regev, and Paola Arlotta. Molecular logic of cellular diversification in the mouse cerebral cortex. Nature, 595(7868):554-559, 2021. Google Scholar
  12. Herbert B. Enderton. A Mathematical Introduction to Logic. Academic Press, 1972. Google Scholar
  13. Luca Galbusera, Georgios Giannopoulos, Sotiris Argyroudis, and Kalliopi Kakderi. A Boolean networks approach to modeling and resilience analysis of interdependent critical infrastructures. Computer-Aided Civil and Infrastructure Engineering, 33(12):1041-1055, 2018. URL: https://doi.org/10.1111/mice.12371.
  14. Yuval Gerber, Michelle Aluf-Medina, Ori Ratzon, Leeshay Elimelech, and Hillel Kugler. Reasoning about monotonic regulation conditions for Boolean gene regulatory networks: An algorithmic approach. In 2025 IEEE International Conference on Bioinformatics and Biomedicine (BIBM), pages 4721-4728. IEEE, 2025. URL: https://doi.org/10.1109/BIBM66473.2025.11356159.
  15. Carito Guziolowski, Santiago Videla, Federica Eduati, Sven Thiele, Thomas Cokelaer, Anne Siegel, and Julio Saez-Rodriguez. Exhaustively characterizing feasible logic models of a signaling network using answer set programming. Bioinformatics, 29(18):2320-2326, 2013. URL: https://doi.org/10.1093/bioinformatics/btt393.
  16. Léonard Hérault, Mathilde Poplineau, Estelle Duprez, and Élisabeth Remy. A novel Boolean network inference strategy to model early hematopoiesis aging. Computational and Structural Biotechnology Journal, 21:21-33, 2023. Google Scholar
  17. Claus Kadelka, Taras-Michael Butrie, Evan Hilton, Jack Kinseth, Addison Schmidt, and Haris Serdarevic. A meta-analysis of Boolean network models reveals design principles of gene regulatory networks. Science advances, 10(2), 2024. Google Scholar
  18. Stuart Kauffman. Homeostasis and differentiation in random genetic control networks. Nature, 224(5215):177-178, 1969. Google Scholar
  19. Gustavo Magaña-López, Laurence Calzone, Andrei Zinovyev, and Loïc Paulevé. Scboolseq: linking scrna-seq statistics and Boolean dynamics. PLoS Computational Biology, 20(7):e1011620, 2024. Google Scholar
  20. Salvador A Méndez and Gonzalo A Ruz. Social consensus modeling using threshold Boolean networks. In 2024 43rd International Conference of the Chilean Computer Science Society (SCCC), pages 1-7. IEEE, 2024. URL: https://doi.org/10.1109/SCCC63879.2024.10767649.
  21. Isabella-Hilda Mendler, Barbara Drossel, and Marc-Thorsten Hütt. Microbiome abundance patterns as attractors and the implications for the inference of microbial interaction networks. Physica A: Statistical Mechanics and its Applications, 639:129658, 2024. Google Scholar
  22. Samuel Pastva, David Šafránek, Nikola Beneš, Luboš Brim, and Thomas Henzinger. Repository of logically consistent real-world Boolean network models. bioRxiv, pages 2023-06, 2023. Google Scholar
  23. Loïc Paulevé and Cédric Gaucherel. Inference of ecological networks and possibilistic dynamics based on Boolean networks from observations and prior knowledge. Methods in Ecology and Evolution, 16(8):1851-1867, 2025. Google Scholar
  24. Žiga Pušnik, Miha Mraz, Nikolaj Zimic, and Miha Moškon. Review and assessment of Boolean approaches for inference of gene regulatory networks. Heliyon, 8(8), 2022. Google Scholar
  25. Jordan C Rozum, Colin Campbell, Eli Newby, Fatemeh Sadat Fatemi Nasrollahi, and Réka Albert. Boolean networks as predictive models of emergent biological behaviors. Cambridge University Press, 2024. Google Scholar
  26. Viorica Sofronie-Stokkermans. Hierarchical reasoning in local theory extensions and applications. In Franz Winkler, Viorel Negru, Tetsuo Ida, Tudor Jebelean, Dana Petcu, Stephen M. Watt, and Daniela Zaharie, editors, 16th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2014, Timisoara, Romania, September 22-25, 2014, pages 34-41. IEEE Computer Society, 2014. URL: https://doi.org/10.1109/SYNASC.2014.13.
  27. Viorica Sofronie-Stokkermans and Carsten Ihlemann. Automated reasoning in some local extensions of ordered structures. In 37th International Symposium on Multiple-Valued Logic (ISMVL'07), pages 1-1. IEEE, 2007. Google Scholar
  28. René Thomas. Regulatory networks seen as asynchronous automata: a logical description. Journal of theoretical biology, 153(1):1-23, 1991. Google Scholar
  29. Dénes Türei, Jonathan Schaul, Nicolàs Palacio-Escat, Balázs Bohár, Yunfan Bai, Francesco Ceccarelli, Elif Çevrim, Macabe Daley, Melih Darcan, Daniel Dimitrov, Tunca Doğan, Daniel Domingo-Fernández, Aurelien Dugourd, Attila Gábor, Lejla Gul, Benjamin A Hall, Charles Tapley Hoyt, Olga Ivanova, Michal Klein, Toby Lawrence, Diego Mañanes, Dezső Módos, Sophia Müller-Dott, Márton Ölbei, Christina Schmidt, Bünyamin Şen, Fabian J Theis, Atabey Ünlü, Erva Ulusoy, Alberto Valdeolivas, Tamás Korcsmáros, and Julio Saez-Rodriguez. Omnipath: integrated knowledgebase for multi-omics analysis. Nucleic Acids Research, 54(D1):D652-D660, 2025. Google Scholar
  30. Xiao Yang, Réka Albert, Lauren Elreda Molloy, and Nilam Ram. Modeling and managing behavior change in groups: A Boolean network method. advances.in/psychology, 2:e55226, 2024. Google Scholar
  31. Boyan Yordanov, Sara-jane Dunn, Colin Gravill, Himanshu Arora, Hillel Kugler, and Christoph M Wintersteiger. The reasoning engine: a satisfiability modulo theories-based framework for reasoning about discrete biological models. Journal of Computational Biology, 30(9):1046-1058, 2023. URL: https://doi.org/10.1089/cmb.2023.0117.
  32. Boyan Yordanov, Sara-Jane Dunn, Hillel Kugler, Austin Smith, Graziano Martello, and Stephen Emmott. A method to identify and analyze biological programs through automated reasoning. NPJ systems biology and applications, 2(1):16010, 2016. Google Scholar
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