SMT with Uninterpreted Functions and Monotonicity Constraints in Systems Biology
This addresses the model inference problem in systems biology, offering a more efficient method compared to existing tools, though it appears incremental as it builds on existing SMT techniques with specific constraints.
The paper tackles model inference for biological systems by applying SMT with uninterpreted functions and monotonicity constraints, showing that instantiation-based encodings outperform quantified encodings and significantly outperform state-of-the-art domain-specific tools like Bonesis and AEON.
The theory of uninterpreted functions is a key modeling tool for systems with unknown or abstracted components. Some domains such as systems biology impose further restrictions regarding monotonicity 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.