Under the auspices of the Computational Complexity Foundation (CCF)

REPORTS > KEYWORD > ORDERED BINARY DECISION DIAGRAMS:
Reports tagged with Ordered Binary Decision Diagrams:
TR96-009 | 17th January 1996

#### On Learning Branching Programs and Small Depth Circuits

This paper studies the learnability of branching programs and small depth
circuits with modular and threshold gates in both the exact and PAC learning
models with and without membership queries. Some of the results extend earlier
works in [GG95,ERR95,BTW95]. The main results are as follows. For
branching programs we ... more >>>

TR98-001 | 17th December 1997
Detlef Sieling

#### On the Existence of Polynomial Time Approximation Schemes for OBDD Minimization

Revisions: 1

The size of Ordered Binary Decision Diagrams (OBDDs) is
determined by the chosen variable ordering. A poor choice may cause an
OBDD to be too large to fit into the available memory. The decision
variant of the variable ordering problem is known to be
NP-complete. We strengthen this result by ... more >>>

TR99-011 | 14th April 1999
Matthias Krause, Petr Savicky, Ingo Wegener

#### Approximations by OBDDs and the variable ordering problem

Ordered binary decision diagrams (OBDDs) and their variants
are motivated by the need to represent Boolean functions
in applications. Research concerning these applications leads
also to problems and results interesting from theoretical
point of view. In this paper, methods from communication
complexity and ... more >>>

TR07-009 | 8th January 2007
Nathan Segerlind

#### Nearly-Exponential Size Lower Bounds for Symbolic Quantifier Elimination Algorithms and OBDD-Based Proofs of Unsatisfiability

We demonstrate a family of propositional formulas in conjunctive normal form
so that a formula of size $N$ requires size $2^{\Omega(\sqrt[7]{N/logN})}$
to refute using the tree-like OBDD refutation system of
Atserias, Kolaitis and Vardi
with respect to all variable orderings.
All known symbolic quantifier elimination algorithms for satisfiability
generate ... more >>>

TR07-049 | 1st June 2007
Beate Bollig, Niko Range, Ingo Wegener

#### Exact OBDD Bounds for some Fundamental Functions

Ordered binary decision diagrams (OBDDs) are nowadays the most common
dynamic data structure or representation type for Boolean functions.
Among the many areas of application are verification, model checking,
computer aided design, relational algebra, and symbolic graph algorithms.
Although many even exponential lower bounds on the OBDD size of Boolean ... more >>>

TR07-126 | 5th November 2007
Nathan Segerlind

#### On the relative efficiency of resolution-like proofs and ordered binary decision diagram proofs

We show that tree-like OBDD proofs of unsatisfiability require an exponential increase ($s \mapsto 2^{s^{\Omega(1)}}$) in proof size to simulate unrestricted resolution, and that unrestricted OBDD proofs of unsatisfiability require an almost-exponential increase ($s \mapsto 2^{ 2^{\left( \log s \right)^{\Omega(1)}}}$) in proof size to simulate $\Res{O(\log n)}$. The OBDD proof ... more >>>

TR08-056 | 22nd April 2008
Beate Bollig

#### On the OBDD complexity of the most significant bit of integer multiplication

Integer multiplication as one of the basic arithmetic functions has been
in the focus of several complexity theoretical investigations.
Ordered binary decision diagrams (OBDDs) are one of the most common
dynamic data structures for boolean functions.
Among the many areas of application are verification, model checking,
computer-aided design, relational algebra, ... more >>>

TR09-087 | 1st October 2009
Olga Tveretina, Carsten Sinz, Hans Zantema

#### Ordered Binary Decision Diagrams, Pigeonhole Formulas and Beyond

Groote and Zantema proved that a particular OBDD computation of the pigeonhole formula has an exponential
size and that limited OBDD derivations cannot simulate resolution polynomially. Here we show that any arbitrary OBDD Apply refutation of the pigeonhole formula has an exponential
size: we prove that the size of one ... more >>>

TR13-018 | 29th January 2013
Luke Friedman, Yixin Xu

#### Exponential Lower Bounds for Refuting Random Formulas Using Ordered Binary Decision Diagrams

A propositional proof system based on ordered binary decision diagrams (OBDDs) was introduced by Atserias et al. Krajicek proved exponential lower bounds for a strong variant of this system using feasible interpolation, and Tveretina et al. proved exponential lower bounds for restricted versions of this system for refuting formulas derived ... more >>>

TR14-167 | 11th November 2014
Beate Bollig

#### On the Minimization of (Complete) Ordered Binary Decision Diagrams

Ordered binary decision diagrams (OBDDs) are a popular data structure for Boolean functions.
Some applications work with a restricted variant called complete OBDDs
which is strongly related to nonuniform deterministic finite automata.
One of its complexity measures is the width which has been investigated
in several areas in computer science ... more >>>

ISSN 1433-8092 | Imprint