Charles Explorer logo
🇨🇿

Compiling SL representations of Boolean functions into OBDDs

Publikace na Matematicko-fyzikální fakulta |
2020

Tento text není v aktuálním jazyce dostupný. Zobrazuje se verze "en".Abstrakt

Given a truth table representation of a Boolean function f theswitch-list (SL) representation of f consists of the function value f(0) at the all-zero vector and the list of all Boolean vectors from the truth table off which have a different function value then the preceding vector. The main result of this paper is a polynomial time compilation algorithm from a SL representation of a given function f to an Ordered Binary Decision Diagram (OBDD) representation of f where the output OBDD respects some prescribed order of variables possibly different than the input order used by the SL representation of f.

Furthermore we provide a lower bound construction which shows that the presented compilation algorithm yields an asymptotically optimal size OBDD of f respecting the prescribed output order of variables.