Computing Properties of Thermodynamic Binding Networks: An Integer Programming Approach
Computing Properties of Thermodynamic Binding Networks: An Integer Programming Approach
复制标题
DOI：
10.4230/lipics.dna.27.2
复制
发表时间：
2020-11
期刊：
影响因子：
--
通讯作者：
David Haley;David Doty
中科院分区：
文献类型：
--
作者：
David Haley;David Doty
热力学结合网络（TBN）模型最近被开发为研究工程分子系统的工具。 TBN模型允许一个人通过简化的抽象来推理其行为，该抽象忽略了有关分子组成的细节，重点是任何化学基质共有的系统能量学的两个关键决定因素：形成了多少个分子键，以及中存在多少个分离的复合物中，并且系统。我们以整数程序的形式制定了计算TBN稳定配置的NP-硬化问题（又称最小能量：最大化债券和复合物数量的能量）。我们提供了解决这些配方的开源软件，并提供了经验证据，表明这种方法可以比基于SAT求解器的以前的方法对TBN稳定配置进行明显更快的计算。我们的设置还可以推理一些TBN，其中一些分子的计数无限。这些改进反过来又使我们能够有效地自动化对实用TBN所需属性的验证。最后，我们表明，TBN的刻板基础（整数编程中的最佳证书）具有自然的解释，因为其中构成了本地最小的能量配置的“基本组件”。这种表征有助于验证稳定配置的正确性，而且还有助于验证TBN中的整个“动力学途径”。
The thermodynamic binding networks (TBN) model was recently developed as 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 configurations of a TBN (a.k.a., minimum energy: those that maximize the number of bonds and complexes). We provide open-source software that solves these formulations, and give empirical evidence that this approach enables dramatically faster computation of TBN stable configurations than previous approaches based on SAT solvers. Our setup can also 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's Graver basis (a kind of certificate of optimality in integer programming) has a natural interpretation as 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.