Exploiting Circuit Duality to Speed Up SAT

Introduction:

Inspecting the properties of logic circuits is pivotal to logic applications for computers and especially to Electronic Design Automation (EDA). There exists a large variety of properties to be checked in logic circuits, e.g., unateness, linearity, symmetry, balancedness, monotonicity, thresholdness and many others. Basic characteristics are usually verified first to provide grounds for more involved tests. Tautology and contradiction are the most fundamental properties in logic circuits. A check for tautology determines if a logic circuit is true for all possible input patterns. Analogously, a check for contradiction determines if a logic circuit is false for all possible input patterns. While investigating elementary properties, tautology and contradiction check are difficult problems, i.e., co-NP-complete and NP-complete, respectively. Indeed, both tautology and contradiction check are equivalent formulation of the Boolean SATisfiability (SAT) problem.

Contribution:

Tautology and contradiction check are dual problems. One can interchangeably check outputwise for tautology in place of contradiction by inverting all outputs in a logic circuit. In this trivial approach, the two obtained problems are fully complementary and there is no explicit computational advantage in solving one problem instead of the other.

We show that exact logic inversion is not necessary for transforming tautology into contradiction, and vice versa [1]. We give a set of operator switching rules that selectively exchange tautologies with contradictions. A logic circuit modified by these rules is inverted just if true or false for all input combinations. In the other cases, it is not necessarily the complement of the original one.

This approach generates two different, but equisolvable, instances of the same problem. In this scenario, solving both of them in parallel enables a positive computation speed-up. Indeed, the instance solved first stops the other reducing the runtime. This concept can be used on top of any other checking 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 wide-spread and computing resources are inexpensive. As a case study, we investigate the impact of this approach on SAT. There, by using non-trivial and trivial dualities in sequence, we create a dual SAT instance solvable in parallel with the original one.

Experiments:

First, statistical experiments confirmed that solving the dual circuit in place of the regular one generates runtime reductions not of the random variation type.
 

Then, experiments on general benchmarks show 25% speed-up of SAT, on average, in a concurrent execution scenario.
 



Download:

The “DualSAT” benchmarks and experimental setup can be downloaded at:

DualSAT Experimental Setup

All experiments have been performed using the ABC academic tool [2].
 

Contact:

Please contact Luca Amarau for any questions you might have about “DualSAT”,  at luca dot amaru at epfl dot ch.

Related publications:

[1] L. Amarù, P.-E. Gaillardon, A. Mishchenko, M. Ciesielski, G. De Micheli, “Exploiting Circuit Duality to Speed Up SAT“, IEEE Computer Society Annual Symposium on VLSI (ISVLSI), Montpellier, FR, 2015.

[2] ABC Synthesis tool available at http://www.eecs.berkeley.edu/~alanmi/abc/