Computing minimal representations with binary decision diagrams

Two-level logic minimization is a complex problem, but can lead to multiple advantages. Having the ability of reducing a boolean function can lead to better performances from applications using those. Olivier Coudert developed a state-of-the-art algorithm called SCHERZO being more powerful than any other algorithm created before. This work aims to develop SCHERZO in PyNuSMV, a python framework working on SMV files. The development of the algorithm made use of ZDD from CUDD imported through SWIG.