SMT with Uninterpreted Functions and Monotonicity Constraints in Systems Biology

TL;DR

This paper presents an SMT-based method for modeling biological systems using uninterpreted functions with monotonicity constraints, outperforming existing tools in large-scale benchmarks.

Contribution

It introduces a lazy instantiation approach for monotonicity constraints in SMT, improving efficiency over naive and eager methods in systems biology modeling.

Findings

Lazy SMT approach outperforms naive encodings on large instances.

SMT with monotonicity constraints surpasses domain-specific tools like Bonesis and AEON.

Quantifier instantiation-based encodings are more scalable for complex functions.

Abstract

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.