An official website of the United States government
Starting in the early 2000s, sophisticated technologies have been developed for the rational construction of synthetic genetic networks that implement specified logical functionalities. Despite impressive progress, however, the scaling necessary in order to achieve greater computational power has been hampered by many constraints, including repressor toxicity and the lack of large sets of mutually orthogonal repressors. As a consequence, a typical circuit contains no more than roughly seven repressor-based gates per cell. A possible way around this scalability problem is to distribute the computation among multiple cell types, each of which implements a small subcircuit, which communicate among themselves using diffusible small molecules (DSMs). Examples of DSMs are those employed by quorum sensing systems in bacteria. This paper focuses on systematic ways to implement this distributed approach, in the context of the evaluation of arbitrary Boolean functions. The unique characteristics of genetic circuits and the properties of DSMs require the development of new Boolean synthesis methods, distinct from those classically used in electronic circuit design. In this work, we propose a fast algorithm to synthesize distributed realizations for any Boolean function, under constraints on the number of gates per cell and the number of orthogonal DSMs. The method is based on an exact synthesis algorithm to find the minimal circuit per cell, which in turn allows us to build an extensive database of Boolean functions up to a given number of inputs. For concreteness, we will specifically focus on circuits of up to 4 inputs, which might represent, for example, two chemical inducers and two light inputs at different frequencies. Our method shows that, with a constraint of no more than seven gates per cell, the use of a single DSM increases the total number of realizable circuits by at least 7.58-fold compared to centralized computation. Moreover, when allowing two DSM’s, one can realize 99.995% of all possible 4-input Boolean functions, still with at most 7 gates per cell. The methodology introduced here can be readily adapted to complement recent genetic circuit design automation software. A toolbox that uses the proposed algorithm was created and made available at https://github. com/sontaglab/DBC/.
more »
« less
Fridge Compiler: Optimal Circuits from Molecular Inventories
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.
more »
« less
- PAR ID:
- 10498682
- Editor(s):
- Pang, J.
- Publisher / Repository:
- Lecture Notes in Computer Science, Springer.
- Date Published:
- Journal Name:
- Proceedings of Computational Methods in Systems Biology. CMSB 2023.
- Volume:
- 14137
- Page Range / eLocation ID:
- 236–252
- Format(s):
- Medium: X
- Sponsoring Org:
- National Science Foundation
More Like this
-
-
A functionally complete Boolean operator is sufficient for computational circuits of arbitrary complexity. We connected YES (buffer) with NOT (inverter) and two NOT four-way junction (4J) DNA gates to obtain IMPLY and NAND Boolean functions, respectively, each of which represents a functionally complete gate. The results show a technological path towards creating a DNA computational circuit of arbitrary complexity based on singleton NOT or a combination of NOT and YES gates, which is not possible in electronic computers. We, therefore, concluded that DNA-based circuits and molecular computation may offer opportunities unforeseen in electronics.more » « less
-
Fully Homomorphic Encryption (FHE) is a cryptographic technique that enables privacy-preserving computation. State-of-the-art Boolean FHE implementations provide a very low-level interface, usually exposing a limited set of Boolean gates that programmers must use to write their FHE applications. This programming model is unnecessarily restrictive: many Boolean FHE schemes supportprogrammable bootstrapping, an operation that allows evaluation of an arbitrary fixed-size lookup table. However, most modern FHE compilers are only capable of reasoning about traditional Boolean circuits, and therefore struggle to take full advantage of programmable bootstrapping. We present COATL, an FHE compiler that makes use of programmable bootstrapping to produce circuits that are smaller and more efficient than their traditional Boolean counterparts. COATL generates circuits usingarithmetic lookup tables, a novel abstraction we introduce for reasoning about computations in Boolean FHE programs. We demonstrate on a variety of benchmarks that COATL can generate circuits that run up to 1.5× faster than those generated by other state-of-the-art compilation strategies.more » « less
-
Ivrii, Alexander; Strichman, Ofer (Ed.)Systems mixing Boolean logic and arithmetic have been a long-standing challenge for verification tools such as SAT-based bit-vector solvers. Though SAT solvers can be highly efficient for Boolean reasoning, they scale poorly once multiplication is involved. Algebraic methods using Gröbner basis reduction have recently been used to efficiently verify multiplier circuits in isolation, but generally do not perform well on problems involving bit-level reasoning. We propose that pseudo-Boolean solvers equipped with cutting planes reasoning have the potential to combine the complementary strengths of the existing SAT and algebraic approaches while avoiding their weaknesses. Theoretically, we show that there are optimal-length cutting planes proofs for a large class of bit-level properties of some well known multiplier circuits. This scaling is significantly better than the smallest proofs known for SAT and, in some instances, for algebraic methods. We also show that cutting planes reasoning can extract bit-level consequences of word-level equations in exponentially fewer steps than methods based on Gröbner bases. Experimentally, we demonstrate that pseudo-Boolean solvers can verify the word-level equivalence of adder-based multiplier architectures, as well as commutativity of bit-vector multiplication, in times comparable to the best algebraic methods. We then go further than previous approaches and also verify these properties at the bit-level. Finally, we find examples of simple nonlinear bit-vector inequalities that are intractable for current bit-vector and SAT solvers but easy for pseudo-Boolean solvers.more » « less
-
null (Ed.)We provide a modified version of the Ligero sublinear zero knowledge proof system for arithmetic circuits provided by Ames et. al. (CCS ‘17). Our modification "BooLigero" tailors Ligero for use in Boolean circuits to achieve a significant improvement in proof size. Although the original Ligero system could be used for Boolean circuits, Ligero generally requires allocating an entire field element to represent a single bit on a wire in a Boolean circuit. In contrast, our system performs operations over words of bits, allowing a proof size savings of between O(log(|F|)^1/4) and O(log(|F|)^1/2) compared to Ligero, where F is the field that leads to the optimal proof size in original Ligero. We achieve improvements in proof size of approximately 1.1-1.6x for SHA-2 and 1.7-2.8x for SHA-3. In addition to checking constraints of standard Boolean operations such as AND, XOR, and NOT over words, BooLigero also supports several other constraints such as multiplication in GF(2^w), bit masking, bit rearrangement within and across words, and bitwise outer product. Like Ligero, construction requires no trusted setup and no computational assumptions, which is ideal for blockchain applications. It is plausibly post-quantum secure in the standard model. Furthermore, it is public-coin, perfect honest-verifier zero knowledge, and can be made non-interactive in the random oracle model using the Fiat-Shamir transform.more » « less
- Free Publicly Accessible Full Text
-
Accepted Manuscript1.0
- Conference Paper:
- https://doi.org/10.1007/978-3-031-42697-1_16
