A Satisfiability-Based Approximate Algorithm for Logic Synthesis Using Switching Lattices

In recent years the realization of a logic function on two-dimensional arrays of four-terminal switches, called switching lattices, has attracted considerable interest. Exact and approximate methods have been proposed for the problem of synthesizing Boolean functions on switching lattices with minimum size, called lattice synthesis (LS) problem. However, the exact method can only handle relatively small instances and the approximate methods may find solutions that are far from the optimum. This paper introduces an approximate algorithm, called JANUS, that formalizes the problem of realizing a logic function on a given lattice, called lattice mapping (LM) problem, as a satisfiability problem and explores the search space of the LS problem in a dichotomic search manner, solving LM problems for possible lattice candidates. This paper also presents three methods to improve the initial upper bound and an efficient way to realize multiple logic functions on a single lattice. Experimental results show that JANUS can find solutions very close to the minimum in a reasonable time and obtain better results than the existing approximate methods. The solutions of JANUS can also be better than those of the exact method, which cannot be determined to be optimal due to the given time limit, where the maximum gain on the number of switches reaches up to 25%.