Abstract
Rationally designed molecular circuits describable by well-mixed chemical reaction kinetics can realize arbitrary Boolean function computation yet differ significantly from their electronic counterparts. The design, preparation, and purification of new molecular components poses significant barriers. Consequently, it is desirable to synthesize circuits from an existing “fridge” inventory of distinguishable parts, while satisfying constraints such as component compatibility. Heuristic synthesis techniques intended for large electronic circuits often result in non-optimal molecular circuits, invalid circuits that violate domain-specific constraints, or circuits that cannot be built with the current inventory. Existing “exact” synthesis techniques are able to find minimal feedforward Boolean circuits with complex constraints, but do not map to distinguishable inventory components.
We present the Fridge Compiler, an SMT-based approach to find optimal Boolean circuits within a given molecular inventory. Empirical results demonstrate the Fridge Compiler’s versatility in synthesizing arbitrary Boolean functions using three different molecular architectures, while satisfying user-specified constraints. We showcase the successful synthesis of all 256 three-bit and 65,536 four-bit predicate functions using a large custom inventory, with worst-case completion times of only seconds on a modern laptop. In addition, we introduce a unique class of cyclic molecular circuits that cover a larger number of Boolean functions than their conventional counterparts over a common inventory, often with significantly smaller implementations. Importantly, and absent in previous approaches specific to molecular circuits, the Fridge Compiler is logically sound, complete, and optimal for the user-specified cost function and component inventory.
Supported by an NSF grant (CCF 2106695) and a Faculty Early Career Development Award from NSF (CCF 2143227).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Backes, J.D., Riedel, M.D.: The synthesis of cyclic dependencies with Boolean satisfiability. ACM Trans. Design Autom. Electr. Syst. 17, 44:1–44:24 (2012)
Badelt, S., Shin, S.W., Johnson, R.F., Dong, Q., Thachuk, C., Winfree, E.: A general-purpose CRN-to-DSD compiler with formal verification, optimization, and simulation capabilities. In: Brijder, R., Qian, L. (eds.) DNA 2017. LNCS, vol. 10467, pp. 232–248. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-66799-7_15
Brayton, R.K., Mishchenko, A.: ABC: an academic industrial-strength verification tool. In: International Conference on Computer Aided Verification (2010)
Cardelli, L.: Two-domain DNA strand displacement. Math. Struct. Comput. Sci. 23, 247–271 (2010)
Chen, H.L., Doty, D., Soloveichik, D.: Rate-independent computation in continuous chemical reaction networks. In: Proceedings of the 5th Conference on Innovations in Theoretical Computer Science, ITCS 2014, pp. 313–326. Association for Computing Machinery (2014)
Chen, J.H., Chen, Y.C., Weng, W.C., Huang, C.Y., Wang, C.Y.: Synthesis and verification of cyclic combinational circuits. 2015 28th IEEE International System-on-Chip Conference (SOCC), pp. 257–262 (2015)
Chen, Y.J., et al.: Programmable chemical controllers made from DNA. Nat. Nanotechnol. 8(10), 755–762 (2013). https://doi.org/10.1038/nnano.2013.189
Eshra, A., Shah, S., Song, T., Reif, J.H.: Renewable DNA hairpin-based logic circuits. IEEE Trans. Nanotechnol. 18, 252–259 (2019)
Haaswijk, W., Soeken, M., Mishchenko, A., Micheli, G.D.: SAT-based exact synthesis: encodings, topology families, and parallelism. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 39, 871–884 (2020)
Jha, S., Gulwani, S., Seshia, S.A., Tiwari, A.: Oracle-guided component-based program synthesis. In: 2010 ACM/IEEE 32nd International Conference on Software Engineering, vol. 1, pp. 215–224 (2010)
Jones, T.S., Oliveira, S.M.D., Myers, C.J., Voigt, C.A., Densmore, D.M.: Genetic circuit design automation with Cello 2.0. Nat. Protocols 17, 1097–1113 (2022)
Lakin, M.R., Youssef, S., Polo, F., Emmott, S., Phillips, A.: Visual DSD: a design and analysis tool for DNA strand displacement systems. Bioinformatics 27, 3211–3213 (2011)
de Moura, L.M., Bjørner, N.S.: Z3: An efficient SMT solver. In: International Conference on Tools and Algorithms for Construction and Analysis of Systems (2008)
Nielsen, A.A.K., et al.: Genetic circuit design automation. Science 352 (2016)
Qian, L., Winfree, E.: Scaling up digital circuit computation with DNA strand displacement cascades. Science 332, 1196–1201 (2011)
Riedel, M.D.: Cyclic combinational circuits. California Institute of Technology (2004)
Shannon, C.E.: Realization of All 16 Switching Functions of Two Variables Requires 18 Contacts: Bell Laboratories Memorandum, pp. 711–714. Wiley-IEEE Press (1953)
Soeken, M., et al.: Practical exact synthesis. In: 2018 Design, Automation & Test in Europe Conference & Exhibition (DATE), pp. 309–314 (2018)
Soeken, M., Riener, H., Haaswijk, W., Micheli, G.D.: The EPFL logic synthesis libraries. ArXiv abs/1805.05121 (2018)
Solar-Lezama, A., Tancau, L., Bodik, R., Seshia, S., Saraswat, V.: Combinatorial sketching for finite programs. In: Proceedings of the 12th international conference on Architectural support for programming languages and operating systems, pp. 404–415 (2006)
Soloveichik, D., Seelig, G., Winfree, E.: DNA as a universal substrate for chemical kinetics. Proc. Natl. Acad. Sci. 107, 5393–5398 (2009)
Testa, E., et al.: Inverter propagation and fan-out constraints for beyond-CMOS majority-based technologies. 2017 IEEE Computer Society Annual Symposium on VLSI (ISVLSI), pp. 164–169 (2017)
Thachuk, C., Winfree, E.: A fast, robust, and reconfigurable molecular circuit breadboard. In: 15th Annual Conference on Foundations of Nanoscience (2018). https://thachuk.com/talk/2018-fnano-invited/2018-FNANO-invited.pdf, invited Talk
Torlak, E., Bodík, R.: Growing solver-aided languages with Rosette. In: SIGPLAN Symposium On New Ideas, New Paradigms, and Reflections on Programming and Software (2013)
Wolf, C.: Yosys open synthesis suite (2016)
Yordanov, B., Hamadi, Y., Kugler, H., Wintersteiger, C.M.: Z34Bio: an SMT-based framework for analyzing biological computation. In: SMT Workshop 2013 11th International Workshop on Satisfiability Modulo Theories (2013)
Author information
Authors and Affiliations
Corresponding authors
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2023 The Author(s), under exclusive license to Springer Nature Switzerland AG
About this paper
Cite this paper
Wathieu, L., Smith, G., Ceze, L., Thachuk, C. (2023). Fridge Compiler: Optimal Circuits from Molecular Inventories. In: Pang, J., Niehren, J. (eds) Computational Methods in Systems Biology. CMSB 2023. Lecture Notes in Computer Science(), vol 14137. Springer, Cham. https://doi.org/10.1007/978-3-031-42697-1_16
Download citation
DOI: https://doi.org/10.1007/978-3-031-42697-1_16
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-031-42696-4
Online ISBN: 978-3-031-42697-1
eBook Packages: Computer ScienceComputer Science (R0)