Efficient exact spare allocation via Boolean satisfiability

Fabricating large memory and processor arrays is subject to physical failures resulting in yield degradation. The strategy of incorporating spare rows and columns to obtain reasonable production yields was first proposed in the 1970s, and continues to play an important role in recent VLSI developments. The spare allocation problem (SAP) in general is known to be intractable, an efficient exact spare allocation algorithm has great value. We propose a new Boolean encoding of SAP and a new SAT-based exact algorithm SATRepair. We used a realistic fault distribution model to compare SATRepair's performances against those of BDDRepair and several algorithms found in the literature. We found that a) our Boolean encoding of SAP facilitates the development of efficient exact SAP algorithms, and b) our SA T-based algorithm outperforms previous algorithms, especially for large problems.