alt="images"/>) … an (xn or ) an+1 as shown in Figure 2.2a. It is to be noted that a1 – an+1 are the additional vertices included in the graph to commonly connect x1 and – xn and , respectively, and facilitate in representing all possible combinations for the string x1 x2 x3 … xn. The graphical form a1 (x1 or ) a2 (x2 or ) a3 (x3 or ) … an (xn or ) an+1 is represented in the DNA world by using the sequences for each vertex and edge in the same manner as that explained in Adleman's model. These DNA solutions can be amplified and separated easily based on the specific sequence represented for each variable using the biochemical steps of PCR, gel electrophoresis, and affinity separation described earlier.
Figure 2.2 Lipton's graph [3] for constructing a binary number for a general variable string (x1 x2 x3 … xn).
The objective is to extract a binary sequence for x1 x2 x3 … xn from all possible combinations that satisfy all the clauses C1, C2, C3, …, Cm. To solve this problem, the ssDNA sequences of x1, , x2, , x3, , …, xn and along with sequences of a1 – an+1 are added in the first test tube. Here all the sequences are selected such that the ligation represents the path between the vertices like Adleman's model. All feasible paths are represented in the first test tube. These paths are constituted by the edges from ak to both xk and and from both xk and to ak+1 for any kth variable. If the vertex takes the xk label, it encodes the value “1,” and if it takes the label, it encodes the value “0.” For example, the path a1a2x2a3x3a4 encodes binary number 011. The next operation is the extraction in which the solution that satisfies the Boolean formula has to be extracted from all feasible solutions present in the first test tube. For this, the DNA solutions are operated by an extraction operator E (t, i, v) in several sequential steps in which t represents the sequences of the tube where an ith bit of variable string x1 x2 x3 … xn is equal to v {0, 1}. Here the extraction operator E (t, i, v) is selected sequentially such that clauses C1, C2, C3, …., Cm are satisfied one after another. Thus, the first extraction operation is selected to make C1 satisfiable. All DNA solutions satisfying C1 are then subjected to the next extraction operation, which makes C2 satisfiable and so on. If any solution is left in the tube after sequentially satisfying C1, C2, C3, …., Cm clauses, then it implies that the given Boolean formula is satisfiable for the sequence remained in the tube. If no solution is left, then it implies that the given Boolean formula is not satisfiable.
Consider a simple example of (x1∨x2) ∧ (¬x2∨x3) for illustration. In this formula, variables x1, x2, and x3 are present. The objective is to find a binary string for x1 x2 x3, which satisfies the clauses C1 = (x1∨x2) and C2 = (¬x2∨x3). Boolean formula (x1∨x2) ∧ (¬x2∨x3) will be solved by making the test tubes for all possibilities, as given in Table 2.1. There are three variables, x1, x2, and x3, represented by “0” or “1,” which leads to total eight possibilities (23 = 8). These eight possible ways are encoded in the form of DNA molecules just by pouring all individual sequences of vertices and edges into the test tube t0 and performing the ligation. Next, the extraction operation is performed on this tube t0. The first extraction operator is E (t0, 1, 1), which extract values having the first bit as “1” since this makes first clause C1 = (x1∨x2) true. Also, the second bit corresponding to x2 can make C1 = (x1∨x2) true. Therefore, all remaining solutions that do not satisfy the E (t0, 1, 1) are extracted in the tube t1′. These solutions from t1′ are then subjected to the second condition where x2 becomes 1. Thus, the next extraction operation, t2, is . The solutions extracted by t1 and t2 represent the solutions that satisfy C1 = (x1∨x2). These solutions are stored in tube t3 and subjected to the next extraction operation, which makes C2 = (¬x2∨x3) satisfiable. In the next operation, E(t3, 2, 0) is performed to extract the solution having ¬x2 equal to 1, which satisfies C2 = (¬x2∨x3). Further, the SAT of C2 = (¬x2∨x3) depends on x3. Therefore, all the remaining solutions stored in are subjected to . This extracts the solutions having x3 equal to 1. These extracted solutions are stored in t5. Finally, the solutions left in t4 and t5 are the solutions that make the given Boolean formula satisfiable. Similarly, the sequence of extraction steps for evaluating the SAT of any Boolean formula can be designed efficiently, as illustrated in the above example.
Table 2.1 The sequence of extraction
