arxiv: 2605.07433 · v2 · submitted 2026-05-08 · 🧬 q-bio.MN · cs.LG· cs.LO

Recognition: 2 theorem links

· Lean Theorem

Inference of Qualitative Models from Steady-State Data via Weighted MaxSMT

Ond\v{r}ej Huvar , Nikola Bene\v{s} , Martin Jon\'a\v{s} , David \v{S}afr\'anek , Samuel Pastva

Authors on Pith no claims yet

Pith reviewed 2026-05-14 22:06 UTC · model grok-4.3

classification 🧬 q-bio.MN cs.LGcs.LO

keywords qualitative modelingMaxSMTbiological networksmodel inferencesteady-state datacell differentiationsoft constraintsprior knowledge

0 comments

The pith

Weighted MaxSMT enables inference of qualitative biological models by treating conflicting observations as soft constraints that can be partially relaxed.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper introduces a method for inferring qualitative models of biological systems from steady-state data that remains usable even when some observations conflict due to measurement errors. Standard constraint encodings often produce unsatisfiable problems, leaving no clear way to decide which data points to drop. The new approach encodes uncertain observations as weighted soft constraints inside a MaxSMT solver, so the solver returns the model that satisfies the largest total weight of observations while obeying hard constraints from a prior-knowledge network. The method supports both Boolean and multi-valued variable domains and accepts observations expressed as level constraints from discretization or ordering constraints from differential expression. The authors demonstrate that the technique can infer neural cell differentiation models from prior-knowledge networks containing between 200 and 1300 genes when ordering constraints are supplied for every gene.

Core claim

By encoding uncertain biological observations as weighted soft constraints, the MaxSMT solver can identify a qualitative model that maximizes the total weight of satisfied observations even when some constraints conflict, thereby producing usable models from noisy steady-state data without requiring manual resolution of every inconsistency.

What carries the argument

The weighted MaxSMT solver that maximizes the sum of weights of satisfied soft constraints (derived from biological observations) while enforcing hard constraints (derived from the prior-knowledge network).

If this is right

Models can be inferred from prior-knowledge networks of 200 to 1300 genes even when ordering constraints are supplied for every gene.
Both Boolean and multi-valued variable domains remain supported under the weighted encoding.
Observations obtained by discretization (level constraints) and by differential expression (ordering constraints) can be incorporated directly as soft constraints.
The solver produces a model that satisfies the maximum total weight of observations rather than declaring the entire problem unsatisfiable.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

Biologists could safely add more tentative observations to a model without risking total unsatisfiability.
The same weighted encoding might be applied to other qualitative modeling domains that face noisy steady-state measurements, such as chemical reaction networks.
Calibration of the weight values for different experimental techniques would be needed to keep the distinction between major and minor errors consistent across datasets.

Load-bearing premise

Uncertain biological observations can be encoded as weighted soft constraints so that the solver reliably distinguishes fundamental model errors from minor data inaccuracies without bias introduced by the weight values.

What would settle it

A dataset generated from a known correct qualitative model with controlled noise added to a subset of observations; if the solver returns a model that contradicts the ground-truth structure on a majority of the noisy observations while a lower-weight alternative matches the ground truth, the weighting approach fails to isolate true errors.

Figures

Figures reproduced from arXiv: 2605.07433 by David \v{S}afr\'anek, Martin Jon\'a\v{s}, Nikola Bene\v{s}, Ond\v{r}ej Huvar, Samuel Pastva.

**Figure 1.** Figure 1: (a) An influence graph of a three-variable MVN with regulation constraints. The grey arrow (the self-loop over [PITH_FULL_IMAGE:figures/full_fig_p005_1.png] view at source ↗

**Figure 2.** Figure 2: An overview of the data-informed workflow for MVN inference used for evaluation in this paper. Other [PITH_FULL_IMAGE:figures/full_fig_p007_2.png] view at source ↗

**Figure 3.** Figure 3: Cumulative plots showing the performance of our method on the tested benchmark instances. Left: The [PITH_FULL_IMAGE:figures/full_fig_p010_3.png] view at source ↗

**Figure 4.** Figure 4: Detailed analysis of runtime with respect to specification size (the number of soft constraints) and influence [PITH_FULL_IMAGE:figures/full_fig_p016_4.png] view at source ↗

**Figure 5.** Figure 5: Detailed analysis of the normalized optimization error for [PITH_FULL_IMAGE:figures/full_fig_p016_5.png] view at source ↗

**Figure 5.** Figure 5: Detailed analysis of the normalised optimisation error (size of the error interval relative to the sum of all [PITH_FULL_IMAGE:figures/full_fig_p017_5.png] view at source ↗

**Figure 6.** Figure 6: Runtime comparison of the first 120 problem instances (using two and three cell types) between Boolean and [PITH_FULL_IMAGE:figures/full_fig_p017_6.png] view at source ↗

read the original abstract

Qualitative models provide crucial instruments for modelling complex biological systems. While advances in automated reasoning and symbolic encodings have enabled rigorous inference of these models from data, the process remains highly fragile. First, biological measurement errors inevitably propagate into formal model specifications. Second, when a specification becomes unsatisfiable, distinguishing between fundamental design flaws and minor technical errors is notoriously difficult. This uncertainty often leads to under-specification, as it is unclear which observations are still ``safe'' to incorporate. To overcome these challenges, we introduce a robust inference method based on weighted MaxSMT. By encoding uncertain biological observations as weighted soft constraints, our approach enables the solver to identify a model best reflecting the observations, even with some conflicting constraints. Our method allows for Boolean and multi-valued variable domains, alongside observations derived from discretisation (level constraints) and differential expression (ordering constraints). We show our approach can be used to successfully infer neural cell differentiation models from prior-knowledge networks with 200--1300 genes using ordering constraints on all included genes.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

The paper gives a weighted MaxSMT encoding for inferring qualitative models from noisy steady-state data on networks up to 1300 genes, but leaves weight selection without justification or tests.

read the letter

The main point is a practical encoding that turns uncertain biological observations into weighted soft constraints inside MaxSMT. This lets the solver return a model that satisfies the hard prior-knowledge network plus as many of the soft ordering and level constraints as possible, even when some data conflict. The work shows the method running on neural cell differentiation networks with 200–1300 genes and ordering constraints on every gene, which is a clear step up in scale from earlier qualitative inference tools that often stopped at much smaller systems. It also handles both Boolean and multi-valued variables plus the two main observation types (discretized levels and differential-expression orderings) in one framework. That combination is new enough to be worth attention for anyone building qualitative models from real data. The soft spot is exactly the weighting step. The abstract gives no derivation, calibration procedure, or sensitivity checks for the weights on the soft clauses. When multiple models remain feasible after the hard constraints, the minimal-cost solution can shift with the relative weights, so the claim that the method reliably separates fundamental design problems from minor measurement errors rests on an unexamined modeling choice. No validation against known gold-standard models or discussion of solver timeouts appears either. This paper is for systems biologists who already work with qualitative network models and need a way to absorb noisy steady-state measurements without immediately declaring the whole specification broken. Readers who care about SMT encodings applied to biology will get concrete value from the constraint formulation and the reported scale. It deserves a serious referee because the core problem is real and the scaling result is concrete, even though the weight issue will need concrete evidence before the method can be used with confidence.

Referee Report

2 major / 2 minor

Summary. The paper introduces a weighted MaxSMT encoding for inferring qualitative (Boolean or multi-valued) models from steady-state data. Uncertain observations are represented as soft constraints whose violation penalties are set by user-chosen weights; the solver returns a minimum-cost model that satisfies all hard constraints (prior-knowledge network plus ordering or level constraints) while minimizing total soft-constraint cost. The central empirical claim is that this procedure successfully recovers plausible neural-cell-differentiation models from prior-knowledge networks containing 200–1300 genes when ordering constraints are supplied for every gene.

Significance. A reliable, scalable method for qualitative-model inference that tolerates conflicting or noisy biological observations would be a useful addition to the q-bio.MN toolkit. The reported scale (networks up to 1300 genes) is larger than most existing symbolic-inference demonstrations; if the weighting scheme can be shown to be robust or data-driven, the approach could reduce manual curation effort when building large regulatory models.

major comments (2)

[§3] §3 (Encoding): the central claim that weighted MaxSMT “distinguishes fundamental design flaws from minor data errors” rests on the assumption that the chosen weights produce a biologically meaningful cost ordering. No derivation, empirical calibration procedure, or sensitivity analysis is supplied for these weights; different relative magnitudes can therefore select different minimal-cost models when the hard constraints leave multiple feasible solutions. This is load-bearing for the success reported on 200–1300-gene networks.
[§5] §5 (Results): the abstract and results assert successful inference on networks of 200–1300 genes, yet no quantitative validation against known reference models, no report of solver timeout rates, and no ablation on weight-selection strategies are provided. Without these controls it is impossible to assess whether the reported models are recovered because of the method or because of particular weight choices.

minor comments (2)

[§2] Notation for multi-valued domains and the precise mapping from differential-expression data to ordering constraints should be stated explicitly in a single table or definition block for reproducibility.
[Introduction] The manuscript would benefit from a short paragraph comparing the weighted-MaxSMT formulation to existing MaxSAT or MaxSMT encodings already used in systems biology (e.g., those based on BioASP or similar tools).

Simulated Author's Rebuttal

2 responses · 1 unresolved

We thank the referee for the constructive feedback, which highlights important aspects of weight selection and empirical validation. We address each major comment below and indicate planned revisions.

read point-by-point responses

Referee: [§3] §3 (Encoding): the central claim that weighted MaxSMT “distinguishes fundamental design flaws from minor data errors” rests on the assumption that the chosen weights produce a biologically meaningful cost ordering. No derivation, empirical calibration procedure, or sensitivity analysis is supplied for these weights; different relative magnitudes can therefore select different minimal-cost models when the hard constraints leave multiple feasible solutions. This is load-bearing for the success reported on 200–1300-gene networks.

Authors: We agree that explicit guidance on weight selection strengthens the central claim. Weights are intended to encode user-specified confidence levels in observations (e.g., higher weights for more reliable differential-expression data), allowing the solver to prioritize trusted constraints. To address the concern, we will add a dedicated subsection on weight assignment heuristics, including examples drawn from the neural-differentiation case study, and include a sensitivity analysis that varies relative weight magnitudes and reports the resulting model changes. revision: yes
Referee: [§5] §5 (Results): the abstract and results assert successful inference on networks of 200–1300 genes, yet no quantitative validation against known reference models, no report of solver timeout rates, and no ablation on weight-selection strategies are provided. Without these controls it is impossible to assess whether the reported models are recovered because of the method or because of particular weight choices.

Authors: We acknowledge that the current results section lacks quantitative benchmarks against reference models and ablations. For the reported 200–1300-gene networks, comprehensive ground-truth models are unavailable in the literature, limiting direct quantitative validation. We will nevertheless add solver performance metrics (runtimes and timeout rates), an ablation study comparing multiple weight-selection heuristics, and, where smaller subnetworks with partial reference information exist, additional consistency checks. These additions will clarify the contribution of the weighting scheme. revision: partial

standing simulated objections not resolved

Full quantitative validation against known reference models for the complete 200–1300-gene neural-differentiation networks, as no such comprehensive reference models are available in the literature.

Circularity Check

0 steps flagged

No significant circularity in derivation

full rationale

The paper encodes biological observations directly as weighted soft constraints in a MaxSMT solver and claims successful inference on large networks from ordering constraints. No equation or step reduces a claimed prediction to its own inputs by construction, no parameter is fitted on a subset and then presented as an independent prediction, and no load-bearing uniqueness theorem or ansatz is imported solely via self-citation. The weighting choice is an explicit modeling decision whose justification is external to the derivation itself; the central inference procedure remains self-contained against the stated prior-knowledge networks and ordering data.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The approach rests on standard assumptions about encoding biological data into constraints and the ability of weighted MaxSMT to produce biologically meaningful models from noisy inputs.

axioms (1)

domain assumption Biological measurements can be discretized into level constraints and ordering constraints without loss of essential information
Invoked when observations are turned into soft constraints for the solver.

pith-pipeline@v0.9.0 · 5504 in / 1094 out tokens · 33088 ms · 2026-05-14T22:06:13.723208+00:00 · methodology

Review history (2 revisions) →

discussion (0)

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

IndisputableMonolith/Cost/FunctionalEquation.lean washburn_uniqueness_aczel unclear

?

unclear
Relation between the paper passage and the cited Recognition theorem.

By encoding uncertain biological observations as weighted soft constraints, our approach enables the solver to identify a model best reflecting the observations... w(sa_i < sb_i) = ξ, w(sa_i = sb_i) = 1, w(sa_i > sb_i) = 1−ξ
IndisputableMonolith/Foundation/RealityFromDistinction.lean reality_from_one_distinction unclear

?

unclear
Relation between the paper passage and the cited Recognition theorem.

The regulation constraints are prescribed by a pair of functions (Ess,Mon)... monotonicity of any function g ... via the formula template ψg

What do these tags mean?

matches: The paper's claim is directly supported by a theorem in the formal canon.
supports: The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends: The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses: The paper appears to rely on the theorem as machinery.
contradicts: The paper's claim conflicts with a theorem or certificate in the canon.
unclear: Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

36 extracted references · 36 canonical work pages · 1 internal anchor

[1]

PloS one12(2), e0171097 (2017)

Barman, S., Kwon, Y .K.: A novel mutual information-based Boolean network inference method from time-series gene expression data. PloS one12(2), e0171097 (2017)

work page 2017
[2]

In: Biere, A., Heule, M., van Maaren, H., Walsh, T

Barrett, C.W., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability modulo theories. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability - Second Edition, pp. 1267–1329. Frontiers in Artificial Intelligence and Applications, IOS Press (2021). https://doi.org/10.3233/FAIA201017

work page doi:10.3233/faia201017 2021
[3]

Bioinformatics39(4), btad158 (2023)

Beneš, N., Brim, L., Huvar, O., Pastva, S., Šafránek, D.: Boolean network sketches: a unifying framework for logical model inference. Bioinformatics39(4), btad158 (2023)

work page 2023
[4]

Bioinformatics38(21), 4978–4980 (2022)

Beneš, N., Brim, L., Huvar, O., Pastva, S., Šafránek, D., Šmijáková, E.: AEON.py: Python library for attractor analysis in asynchronous Boolean networks. Bioinformatics38(21), 4978–4980 (2022)

work page 2022
[5]

In: Baier, C., Tinelli, C

Bjørner, N.S., Phan, A., Fleckenstein, L.: νZ - An optimizing SMT solver. In: Baier, C., Tinelli, C. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 21st International Conference, TACAS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings....

work page doi:10.1007/978-3-662-46681-0_14 2015
[6]

Frontiers in Microbiology14, 1274740 (2023)

Chagas, M.d.S., Trindade dos Santos, M., Argollo de Menezes, M., da Silva, F.A.B.: Boolean model of the gene regulatory network of Pseudomonas aeruginosa CCBH4851. Frontiers in Microbiology14, 1274740 (2023)

work page 2023
[7]

npj Systems Biology and Applications11(1), 105 (2025)

Chevalier, S., Becker, J., Gui, Y ., Noël, V ., Su, C., Jung, S., Calzone, L., Zinovyev, A., Del Sol, A., Pang, J., et al.: Data-driven inference of Boolean networks from transcriptomes to predict cellular differentiation and reprogramming. npj Systems Biology and Applications11(1), 105 (2025)

work page 2025
[8]

In: International Conference on Computational Methods in Systems Biology

Chevalier, S., Boyenval, D., Magaña-López, G., Roncalli, T., Vaginay, A., Paulevé, L.: 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. pp. 71–79. Springer (2024)

work page 2024
[9]

Science376(6594), eabl4896 (2022)

Consortium*, T.T.S., Jones, R.C., Karkanias, J., Krasnow, M.A., Pisco, A.O., Quake, S.R., Salzman, J., Yosef, N., Bulthaup, B., Brown, P., et al.: The tabula sapiens: A multiple-organ, single-cell transcriptomic atlas of humans. Science376(6594), eabl4896 (2022)

work page 2022
[10]

In: International conference on Tools and Algorithms for the Construction and Analysis of Systems

De Moura, L., Bjørner, N.: Z3: An efficient SMT solver. In: International conference on Tools and Algorithms for the Construction and Analysis of Systems. pp. 337–340. Springer (2008)

work page 2008
[11]

Nature595(7868), 554–559 (2021)

Di Bella, D.J., Habibi, E., Stickels, R.R., Scalia, G., Brown, J., Yadollahpour, P., Yang, S.M., Abbate, C., Biancalani, T., Macosko, E.Z., Chen, F., Regev, A., Arlotta, P.: Molecular logic of cellular diversification in the mouse cerebral cortex. Nature595(7868), 554–559 (2021)

work page 2021
[12]

Nature Methods22(9), 1836–1845 (2025) 11 APREPRINT- MAY14, 2026

Ergen, C., Pour Amiri, V .V ., Kim, M., Kronfeld, O., Streets, A., Gayoso, A., Yosef, N.: Scvi-hub: an actionable repository for model-driven single-cell analysis. Nature Methods22(9), 1836–1845 (2025) 11 APREPRINT- MAY14, 2026

work page 2025
[13]

IEEE Transactions on Cybernetics52(5), 2916–2930 (2020)

Gao, S., Sun, C., Xiang, C., Qin, K., Lee, T.H.: Learning asynchronous Boolean networks from single-cell data using multiobjective cooperative genetic programming. IEEE Transactions on Cybernetics52(5), 2916–2930 (2020)

work page 2020
[14]

Nature biotechnology 40(2), 163–166 (2022)

Gayoso, A., Lopez, R., Xing, G., Boyeau, P., Valiollah Pour Amiri, V ., Hong, J., Wu, K., Jayasuriya, M., Mehlman, E., Langevin, M., et al.: A Python library for probabilistic analysis of single-cell omics data. Nature biotechnology 40(2), 163–166 (2022)

work page 2022
[15]

PLOS Computational Biology21(4), e1012735 (2025)

Greene, G., Zonfa, I., Ravasz Regan, E.: A Boolean network model of hypoxia, mechanosensing and TGF- β signaling captures the role of phenotypic plasticity and mutations in tumor metastasis. PLOS Computational Biology21(4), e1012735 (2025)

work page 2025
[16]

Bioinformatics29(18), 2320–2326 (2013)

Guziolowski, C., Videla, S., Eduati, F., Thiele, S., Cokelaer, T., Siegel, A., Saez-Rodriguez, J.: Exhaustively characterizing feasible logic models of a signaling network using answer set programming. Bioinformatics29(18), 2320–2326 (2013)

work page 2013
[17]

Computational and Structural Biotechnology Journal21, 21–33 (2023)

Hérault, L., Poplineau, M., Duprez, E., Remy, É.: A novel Boolean network inference strategy to model early hematopoiesis aging. Computational and Structural Biotechnology Journal21, 21–33 (2023)

work page 2023
[18]

Huvar, O., Beneš, N., Jonáš, M., Šafránek, D., Pastva, S.: Inference of qualitative models from steady-state data via Weighted MaxSMT (2026),https://arxiv.org/abs/2605.07433

work page internal anchor Pith review Pith/arXiv arXiv 2026
[19]

In: The 29th International Conference on Theory and Applications of Satisfiability Testing, SAT 2026, July 20-23, Lisbon, Portugal (2026, to appear)

Huvar, O., Jonáš, M., Pastva, S.: SMT with uninterpreted functions and monotonicity constraints in systems biology. In: The 29th International Conference on Theory and Applications of Satisfiability Testing, SAT 2026, July 20-23, Lisbon, Portugal (2026, to appear)

work page 2026
[20]

Nature224(5215), 177–178 (1969)

Kauffman, S.: Homeostasis and differentiation in random genetic control networks. Nature224(5215), 177–178 (1969)

work page 1969
[21]

Machine learning52(1), 147–167 (2003)

Lähdesmäki, H., Shmulevich, I., Yli-Harja, O.: On learning gene regulatory networks under the Boolean network model. Machine learning52(1), 147–167 (2003)

work page 2003
[22]

PLOS Computational Biology20(7), 1–25 (2024)

Magaña-López, G., Calzone, L., Zinovyev, A., Paulevé, L.: scBoolSeq: Linking scRNA-seq statistics and Boolean dynamics. PLOS Computational Biology20(7), 1–25 (2024)

work page 2024
[23]

Expert Review of Proteomics13(6), 555–569 (2016)

Mayer, G., Marcus, K., Eisenacher, M., Kohl, M.: Boolean modeling techniques for protein co-expression networks in systems medicine. Expert Review of Proteomics13(6), 555–569 (2016)

work page 2016
[24]

Bioinformatics32(3), 465–468 (2016)

Müssel, C., Schmid, F., Blätte, T.J., Hopfensitz, M., Lausser, L., Kestler, H.A.: BiTrinA—multiscale binarization and trinarization with quality analysis. Bioinformatics32(3), 465–468 (2016)

work page 2016
[25]

Biosystems97(2), 134–139 (2009)

Naldi, A., et al.: Logical modelling of regulatory networks with GINsim 2.3. Biosystems97(2), 134–139 (2009)

work page 2009
[26]

Heliyon8(8) (2022)

Pušnik, Ž., Mraz, M., Zimic, N., Moškon, M.: Review and assessment of Boolean approaches for inference of gene regulatory networks. Heliyon8(8) (2022)

work page 2022
[27]

BMC systems biology1(1), 4 (2007)

Schaub, M.A., Henzinger, T.A., Fisher, J.: Qualitative networks: a symbolic approach to analyze biological signaling networks. BMC systems biology1(1), 4 (2007)

work page 2007
[28]

Sebastiani, R., Trentin, P.: OptiMathSAT: A tool for optimization modulo theories. J. Autom. Reason.64(3), 423–460 (2020). https://doi.org/10.1007/S10817-018-09508-6

work page doi:10.1007/s10817-018-09508-6 2020
[29]

Bioinformatics28(18), i495–i501 (2012)

Singh, A., Nascimento, J.M., Kowar, S., Busch, H., Boerries, M.: Boolean approach to signalling pathway modelling in HGF-induced keratinocyte migration. Bioinformatics28(18), i495–i501 (2012)

work page 2012
[30]

In: 37th International Symposium on Multiple-Valued Logic (ISMVL’07)

Sofronie-Stokkermans, V ., Ihlemann, C.: Automated reasoning in some local extensions of ordered structures. In: 37th International Symposium on Multiple-Valued Logic (ISMVL’07). pp. 1–1. IEEE (2007)

work page 2007
[31]

BMC bioinformatics14(1), 91 (2013)

Soneson, C., Delorenzi, M.: A comparison of methods for differential expression analysis of RNA-seq data. BMC bioinformatics14(1), 91 (2013)

work page 2013
[32]

Journal of theoretical biology153(1), 1–23 (1991)

Thomas, R.: Regulatory networks seen as asynchronous automata: a logical description. Journal of theoretical biology153(1), 1–23 (1991)

work page 1991
[33]

Nucleic Acids Research54(D1), D652–D660 (2025)

Türei, D., Schaul, J., Palacio-Escat, N., Bohár, B., Bai, Y ., Ceccarelli, F., Çevrim, E., Daley, M., Darcan, M., Dimitrov, D., Do ˘gan, T., Domingo-Fernández, D., Dugourd, A., Gábor, A., Gul, L., Hall, B.A., Hoyt, C.T., Ivanova, O., Klein, M., Lawrence, T., Mañanes, D., Módos, D., Müller-Dott, S., Ölbei, M., Schmidt, C., ¸ Sen, B., Theis, F.J., Ünlü, A.,...

work page 2025
[34]

Journal of Computational Biology30(9), 1046–1058 (2023) 12 APREPRINT- MAY14, 2026

Yordanov, B., Dunn, S.j., Gravill, C., Arora, H., Kugler, H., Wintersteiger, C.M.: The reasoning engine: a satisfia- bility modulo theories-based framework for reasoning about discrete biological models. Journal of Computational Biology30(9), 1046–1058 (2023) 12 APREPRINT- MAY14, 2026

work page 2023
[35]

In: International Symposium on Bioinformatics Research and Applications

Yordanov, B., Dunn, S.J., Gravill, C., Kugler, H., Wintersteiger, C.M.: An SMT-based framework for reasoning about discrete biological models. In: International Symposium on Bioinformatics Research and Applications. pp. 114–125. Springer (2022)

work page 2022
[36]

Yordanov, B., Dunn, S.J., Kugler, H., Smith, A., Martello, G., Emmott, S.: A method to identify and analyze biological programs through automated reasoning. NPJ systems biology and applications2(1), 16010 (2016) 13 APREPRINT- MAY14, 2026 A Example – More Details There are 393 030 optimal solutions for Scenario I of Example 1, all of which have the same va...

work page 2016