带不可置换函数和单调性约束的 SMT 方法在系统生物学中的应用
计算机科学中的逻辑
2026-04-10 v1
摘要
不可置换函数理论是建模具有未知或抽象组件的系统的关键工具。某些领域如系统生物学对这些组件施加进一步的单调性限制，要求特定输入对输出产生持续的正或负影响。在本文中，我们通过应用不可置换函数理论并加入单调性约束来解决生物系统的模型推断问题。我们比较了对问题进行惯性量化编码与现有基于惰性量子化实例化方法的性能——后者基于有限集的量子无单调性引理足以编码不可置换函数的单调性。此外，我们考虑一种惰性变体，该方法按需引入单调性引理。我们使用大量系统生物学基准测试评估了基于 SMT 的模型推断方法。结果表明，实例化编码显著优于量子化编码，后者通常在大函数仪参数和复杂实例方面难以应对。作为关键结果，我们表明，基于 SMT 的不可置换函数和单调性约束方法显著优于系统生物学中使用的基于 ASP 的 Bonesis 和基于 BDD 的 AEON 等领域专用工具。
引用
@article{arxiv.2604.07496,
title = {SMT with Uninterpreted Functions and Monotonicity Constraints in Systems Biology},
author = {Ondřej Huvar and Martin Jonáš and Samuel Pastva},
journal= {arXiv preprint arXiv:2604.07496},
year = {2026}
}
备注
Submitted to SAT 2026 (under review)