Francesco Bergadano, Nader Bshouty, Christino Tamon, Stefano Varricchio

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 >>>

Detlef Sieling

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 >>>

Matthias Krause, Petr Savicky, Ingo Wegener

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 >>>

Nathan Segerlind

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 >>>

Beate Bollig, Niko Range, Ingo Wegener

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 >>>

Nathan Segerlind

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 >>>

Beate Bollig

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 >>>

Olga Tveretina, Carsten Sinz, Hans Zantema

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 >>>

Luke Friedman, Yixin Xu

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 >>>

Beate Bollig

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 >>>