2D DNA self-assembly for satisfiability
DNA self-assembly has been proposed as a way to cope with huge combinatorial NP-HARD problems, such as satis ability. However, the algorithmic designs for DNA self-assembly proposed so far are highly dependent on the instance to be solved. The required work (DNA synthesis, tile construction, encoding, etc.) can be done only after the instance is given. This paper presents an algorithmic design for solving satis ability problems using two-dimensional DNA self-assembly (tiling). The main driving factor in this work was the design and encoding of the algorithm in a general way that minimizes the dependency on particular instances. In e ect, a large amount of work and preparation can be done in advance as a batch process in the absence of any particular instance. In practice, it is likely that the total time (from the time an instance is given, to the time a solution is returned) will be decreased signi cantly and laboratory procedures will be simpli ed. 1 The Satis ability (SAT) Problem The Boolean Satis ability (SAT) problem is the most known representative of the NP-HARD class of problems. The non-polynomial (usually exponential) time required for optimal solutions to these problems, implies that solution of large instances becomes intractably di cult, if not practically impossible. A SAT instance consists of a number of Boolean variables x1; x2; :::; xm and a number of clauses C1; C2; :::; Cn. Each clause is a disjunction of distinct literals, whereby a literal is a single variable xi itself or its complement xi. A solution (satisfying assignment) is an assignment of binary values to the variables xi, such that the conjunction of all clauses is satis ed. Boolean formulas represented in this format are said to be in Conjunction Normal Form (CNF); a conjunction of disjunctions. An example with 5 variables and 8 clauses is given below: (x1 + x2 + x3)( x2 + x4)( x1 + x5)( x1 + x2 + x3 + x4 + x5)( x3)(x2 + x5)( x5)(x1) In this case, the assignment (x1; x2; x3; x4; x5) = (1; 1; 0; 1; 0) is satisfying. So far, there is no restriction on the number of literals that a single clause can contain. However, even if we require that each clause has exactly k literals (k 3), the problem (known as kCNF-SAT) is still intractable. Moreover, it is proven that any SAT instance can be turned into an equivalent kCNFSAT instance [GaJo79]. From these variations, most notable is the 3CNF-SAT variation, because of the small-sized clauses. Notice that for a given number of m variables, there can be m k 2