Читать книгу DNA- and RNA-Based Computing Systems - Группа авторов - Страница 22

Sakamoto et al. [5] introduced a hairpin formation model for solving an SAT problem using molecular biology techniques. For a given illustrative SAT problem (x₁ ∨x₂) ∧ (¬x₂ ∨x₃), literal strings (x₁, ¬x₂), (x₁, x₃), (x₂, ¬x₂), and (x₂, x₃) are formed. A literal string is a string used to encode the given formula with conjunctions of the literals selected from each clause. The literal strings are obtained by concatenating of DNA sequences corresponding to each literal in a ligation step. In these literal strings, if a variable is represented in both original and negation form, then it violates the SAT condition of the given SAT problem. The literal strings without such violation in which a variable is represented only and at least in one form (either actual or negation) constitute a satisfiable solution to the given SAT problem. In Sakamoto's model, possible literal strings are first obtained by ligation. A length of the literal string equals to the number of clauses × nucleotides used for each literal. Subsequently, the obtained literal strings are subjected to temperature variation, which leads to a hairpin formation if a variable is represented in its original and negation form. The restriction enzyme destroys all such hairpins. These solutions are readily eliminated in the subsequent gel electrophoresis operation where only the literal strings with the desired length are separated. All the literal strings separated are analyzed using the sequencer, and the solution of the given SAT problem is obtained. It is to be noted that the given procedure eliminates a large number of unsatisfying literal strings, which makes it easier to deduce the correct solution from the analysis of the remaining satisfying literal strings. The procedure is useful for large size problems. However, it also has a risk of missing some literal strings due to experimental errors that may lead to an erroneous solution to the given SAT problem.

For the given illustrative SAT problem [(x₁∨x₂) ∧ (¬x₂∨x₃)], a single‐stranded sequence for all literals is ligated to form the literal strings (x₁, ¬x₂), (x₁, x₃), (x₂, ¬x₂), and (x₂, x₃). The ligated strings are shown in Figure 2.5. These ligated strings will be subjected to restriction enzyme digestion, which eliminates the string (x₂, ¬x₂), and finally, the remaining literal strings are (x₁, ¬x₂), (x₁, x₃), and (x₂, x₃). From these remaining three literal strings, a solution to the given SAT problem is deduced by mathematical analysis. It is to be mentioned that only one literal string is eliminated for the given problem as it has only (2)² [= (number of literals in each clause)^{number of clauses}] equal to four literal strings. Though for the given illustrative example the search space is reduced only by 25% (as it removes only one literal string), for bigger problems the reduction in search space is significant. Sakamoto et al. [5] illustrated the benefit of the method by solving 6‐variable, 10‐clause problem [= (x₁ ∨x₂ ∨¬ x₃) ∧(x₁ ∨x₃ ∨ x₄) ∧(x₁ ∨¬ x₃ ∨¬ x₄) ∧(¬ x₁ ∨¬ x₃ ∨x₄) ∧(x₁ ∨¬ x₃ ∨x₅) ∧(x₁ ∨x₄ ∨¬ x₆) ∧(¬ x₁ ∨x₃ ∨ x₄) ∧(x₁ ∨x₃ ∨¬ x₄) ∧(¬ x₁ ∨¬ x₃ ∨¬ x₄) ∧(¬ x₁ ∨ x₃ ∨¬ x₄)] having three literals in each clause. This example has 3¹⁰ = 59 049 literal strings out of which only 24 literal strings were found to be satisfying the condition. Thus, ∼99.95% of the search space is eliminated using the above methodology to finally obtain the correct solution just by analyzing 24 literal strings. One of the advantages of this methodology is the use of just one step, unlike sequential elimination steps used in earlier models.

Figure 2.5 Illustration of four literal strings for the DNA hairpin formation‐based computation.