Exact one-pass synthesis of digital microfluidic biochips

With the advances of the microfluidic technology, the design of digital microfluidic biochips recently received significant attention. But thus far, the corresponding design tasks such as binding, scheduling, placement, and routing have usually been considered separately. Furthermore, often just heuristic results have been obtained. In this work, we present a one-pass synthesis scheme which directly realizes the desired functionality onto the chip and, at the same time, guarantees minimality with respect to area and/or timing. For this purpose, the deductive power of solvers for Boolean satisfiability is exploited. Experiments show how the approach leverages the design of the respective devices.