Computing properties of thermodynamic binding networks: An integer programming approach

TL;DR

This paper introduces an integer programming method to efficiently compute stable configurations of thermodynamic binding networks, enabling faster analysis and verification of molecular systems compared to previous SAT-based approaches.

Contribution

The authors develop an integer programming formulation for TBN stability analysis, providing open-source software and demonstrating significant computational improvements over prior methods.

Findings

Faster computation of TBN stable configurations than SAT solvers.

Ability to handle molecules with unbounded counts.

Verification of entire kinetic pathways in TBNs.

Abstract

The thermodynamic binding networks (TBN) model is a tool for studying engineered molecular systems. The TBN model allows one to reason about their behavior through a simplified abstraction that ignores details about molecular composition, focusing on two key determinants of a system's energetics common to any chemical substrate: how many molecular bonds are formed, and how many separate complexes exist in the system. We formulate as an integer program the NP-hard problem of computing stable (a.k.a., minimum energy) configurations of a TBN: those configurations that maximize the number of bonds and complexes. We provide open-source software solving this integer program. We give empirical evidence that this approach enables dramatically faster computation of TBN stable configurations than previous approaches based on SAT solvers. Furthermore, unlike SAT-based approaches, our integer programming formulation can reason about TBNs in which some molecules have unbounded counts. These improvements in turn allow us to efficiently automate verification of desired properties of practical TBNs. Finally, we show that the TBN has a natural representation with a unique Hilbert basis describing the "fundamental components" out of which locally minimal energy configurations are composed. This characterization helps verify correctness of not only stable configurations, but entire "kinetic pathways" in a TBN.