Improved Circuit-to-CNF Conversion

So far, it has been shown how to encode an ATPG problem into a Boolean satisfiability problem and how to convert a circuit into a SAT instance represented in CNF. The use of multiple-valued logic for handling industrial circuits has also been addressed. In this chapter, improvements to the circuit-to-CNF conversion are proposed so that the approach can cope with large circuits very efficiently. In the first section of this chapter,¹ the use of a hybrid logic is proposed. As mentioned above, the use of the four-valued logic L₄ to handle industrial circuits containing tri-state elements and unknown values creates some overhead – especially in circuits that could completely be modeled with the Boolean logic L₂.