Amaru, LucaGaillardon, Pierre-EmmanuelMishchenko, AlanCiesielski, MaciejDe Micheli, Giovanni2015-04-232015-04-232015-04-23201510.1109/ISVLSI.2015.18https://infoscience.epfl.ch/handle/20.500.14299/113477In this paper, we establish a <i>non-trivial</i> duality between tautology and contradiction check to speed up circuit SAT. Tautology check determines if a logic circuit is <i>true</i> in every possible interpretation. Analogously, contradiction check determines if a logic circuit is <i>false</i> in every possible interpretation. A <i>trivial</I> transformation of a (tautology, contradiction) check problem into a (contradiction, tautology) check problem is the <i>inversion</i> of all outputs in a logic circuit. In this work, we show that <i>exact</i> logic <i>inversion</i> is not necessary. We give operator switching rules that selectively exchange tautologies with contradictions, and <i>vice versa</i>. Our approach collapses into logic <i>inversion</i> just for tautology and contradiction extreme points but generates <i>non-complementary</i> logic circuits in the other cases. This property enables computing benefits when an alternative, but equisolvable, instance of a problem is easier to solve than the original one. As a case study, we investigate the impact on SAT. There, our methodology generates a dual SAT instance solvable in parallel with the original one. This concept can be used on top of any other SAT approach and does not impose much overhead, except having to run two solvers instead of one, which is typically not a problem because multi-cores are widespread and computing resources are inexpensive. Experimental results show a 25% speed-up of SAT in a concurrent execution scenario. Also, statistical experiments confirmed that our runtime reduction is not of the random variation type.text::conference output::conference proceedings::conference paper