zbMATH — the first resource for mathematics

Heuristic NPN classification for large functions using AIGs and LEXSAT. (English) Zbl 06623514
Creignou, Nadia (ed.) et al., Theory and applications of satisfiability testing – SAT 2016. 19th international conference, Bordeaux, France, July 5–8, 2016. Proceedings. Cham: Springer (ISBN 978-3-319-40969-6/pbk; 978-3-319-40970-2/ebook). Lecture Notes in Computer Science 9710, 212-227 (2016).
Summary: Two Boolean functions are NPN equivalent if one can be obtained from the other by negating inputs, permuting inputs, or negating the output. NPN equivalence is an equivalence relation and the number of equivalence classes is significantly smaller than the number of all Boolean functions. This property has been exploited successfully to increase the efficiency of various logic synthesis algorithms. Since computing the NPN representative of a Boolean function is not scalable, heuristics have been proposed that are not guaranteed to find the representative for all functions. So far, these heuristics have been implemented using the function’s truth table representation, and therefore do not scale for functions exceeding 16 variables.
In this paper, we present a symbolic heuristic NPN classification using and-inverter graphs and Boolean satisfiability techniques. This allows us to heuristically compute NPN representatives for functions with much larger number of variables; our experiments contain benchmarks with up to 194 variables. A key technique of the symbolic implementation is SAT-based procedure LEXSAT, which finds the lexicographically smallest satisfiable assignment. To our knowledge, LEXSAT has never been used before in logic synthesis algorithms.
For the entire collection see [Zbl 1337.68009].

68Q25 Analysis of algorithms and problem complexity
68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
ABC; MiniSat
Full Text: DOI
[1] Benini, L., Micheli, G.D.: A survey of Boolean matching techniques for library binding. ACM Trans. Design Autom. Electr. Syst. 2(3), 193–226 (1997) · doi:10.1145/264995.264996
[2] Brand, D.: Verification of large synthesized designs. In: Proceedings of the International Conference on Computer Aided Design, pp. 534–537 (1993) · doi:10.1109/ICCAD.1993.580110
[3] Brayton, R., Mishchenko, A.: ABC: an academic industrial-strength verification tool. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 24–40. Springer, Heidelberg (2010) · Zbl 05772618 · doi:10.1007/978-3-642-14295-6_5
[4] Chatterjee, S., Mishchenko, A., Brayton, R.K., Wang, X., Kam, T.: Reducing structural bias in technology mapping. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 25(12), 2894–2903 (2006) · Zbl 05450327 · doi:10.1109/TCAD.2006.882484
[5] Debnath, D., Sasao, T.: Efficient computation of canonical form for Boolean matching in large libraries. In: Proceedings of the Asia and South Pacific Design Automation Conference, pp. 591–96 (2004) · doi:10.1109/ASPDAC.2004.1337660
[6] Eén, N., Mishchenko, A., Sörensson, N.: Applying logic synthesis for speeding up SAT. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol. 4501, pp. 272–286. Springer, Heidelberg (2007) · Zbl 1214.68351 · doi:10.1007/978-3-540-72788-0_26
[7] Goto, E., Takahasi, H.: Some theorems useful in threshold logic for enumerating Boolean functions. In: International Federation for Information Processing Congress, pp. 747–52 (1962) · Zbl 0143.39505
[8] Harrison, M.A.: Introduction to Switching and Automata Theory. McGraw-Hill, New York (1965) · Zbl 0196.51702
[9] Hellerman, L.: A catalog of three-variable Or-inverter and And-inverter logical circuits. IEEE Trans. Electr. Comput. 12, 198–223 (1963) · doi:10.1109/PGEC.1963.263531
[10] Huang, Z., Wang, L., Nasikovskiy, Y., Mishchenko, A.: Fast Boolean matching based on NPN classification. In: Proceedings of the 2013 International Conference on Field Programmable Technology, pp. 310–313 (2013) · doi:10.1109/FPT.2013.6718374
[11] Katebi, H., Markov, I.L.: Large-scale Boolean matching. In: Proceedings of the Design, Automation and Test in Europe Conference and Exhibition, pp. 771–76 (2010) · doi:10.1109/DATE.2010.5456949
[12] Knuth, D.E.: The Art of Computer Programming, vol. 4A. Addison-Wesley, Reading, Massachusetts (2011) · Zbl 1354.68001
[13] Knuth, D.E.: The Art of Computer Programming, vol. 4, Fascicle 6: Satisfiability. Addison-Wesley, Reading, Massachusetts (2015)
[14] Krentel, M.W.: The complexity of optimization problems. J. Comput. Syst. Sci. 36(3), 490–509 (1988) · Zbl 0652.68040 · doi:10.1016/0022-0000(88)90039-6
[15] Kuehlmann, A., Paruthi, V., Krohm, F., Ganai, M.K.: Robust Boolean reasoning for equivalence checking and functional property verification. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 21(12), 1377–1394 (2002) · Zbl 05448668 · doi:10.1109/TCAD.2002.804386
[16] Mailhot, F., Micheli, G.D.: Algorithms for technology mapping based on binary decision diagrams and on Boolean operations. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 12(5), 599–620 (1993) · Zbl 05448924 · doi:10.1109/43.277607
[17] Mishchenko, A., Chatterjee, S., Brayton, R.: DAG-aware AIG rewriting: a fresh look at combinational logic synthesis. In: Proceedings of the 43rd Design Automation Conference, pp. 532–536 (2006) · doi:10.1109/DAC.2006.229287
[18] Muroga, S.: Logic Design and Switching Theory. Wiley, New York (1979) · Zbl 0473.94018
[19] Rudell, R.: Dynamic variable ordering for ordered binary decision diagrams. In: Proceedings of the International Conference on Computer Aided Design, pp. 42–47 (1993) · doi:10.1109/ICCAD.1993.580029
[20] Soeken, M., Amarù, L.G., Gaillardon, P., De Micheli, G.: Optimizing majority-inverter graphs with functional hashing. In: Proceedings of the Design, Automation and Test in Europe Conference and Exhibition, pp. 1030–1035 (2016) · doi:10.3850/9783981537079_0281
[21] Tseytin, G.S.: On the complexity of derivation in propositional calculus. In: Slisenko, A.P. (ed.) Studies in Constructive Mathematics and Mathematical Logic, Part II, Seminars in Mathematics, pp. 115–125. Springer, NewYork (1970) · doi:10.1007/978-1-4899-5327-8_25
[22] Warren, H.S.: Hacker’s Delight, 2nd edn. Addison-Wesley, Reading (2012)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.