Weizmann Logo
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style

Reports tagged with OBDDs:
TR98-011 | 29th January 1998
Farid Ablayev, Marek Karpinski

A Lower Bound for Integer Multiplication on Randomized Read-Once Branching Programs

We prove an exponential lower bound ($2^{\Omega(n/\log n)}$) on the
size of any randomized ordered read-once branching program
computing integer multiplication. Our proof depends on proving
a new lower bound on Yao's randomized one-way communication
complexity of certain boolean functions. It generalizes to some
other ... more >>>

TR98-038 | 9th July 1998
Marek Karpinski

On the Computational Power of Randomized Branching Programs

We survey some upper and lower bounds established recently on
the sizes of randomized branching programs computing explicit
boolean functions. In particular, we display boolean
functions on which randomized read-once ordered branching
programs are exponentially more powerful than deterministic
or nondeterministic read-$k$-times branching programs for ... more >>>

TR00-046 | 19th June 2000
Philipp Woelfel

New Bounds on the OBDD-Size of Integer Multiplication via Universal Hashing

Ordered binary decision diagrams (OBDDs) belong to the most important
representation types for Boolean functions. Although they allow
important operations such as satisfiability test and equality test to
be performed efficiently, their limitation lies in the fact, that they
may require exponential size for important functions. Bryant ... more >>>

TR06-004 | 6th January 2006
Jesper Torp Kristensen, Peter Bro Miltersen

Finding small OBDDs for incompletely specified truth tables is hard

We present an efficient reduction mapping undirected graphs
G with n = 2^k vertices for integers k
to tables of partially specified Boolean functions
g: {0,1}^(4k+1) -> {0,1,*} so that for any integer m,
G has a vertex colouring using m colours if and only if g ... more >>>

TR07-009 | 8th January 2007
Nathan Segerlind

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

Revisions: 1 , Comments: 1

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-028 | 12th February 2007
Daniel Sawitzki

Implicit Simulation of FNC Algorithms

Implicit algorithms work on their input's characteristic functions and should solve problems heuristically by as few and as efficient functional operations as possible. Together with an appropriate data structure to represent the characteristic functions they yield heuristics which are successfully applied in numerous areas. It is known that implicit algorithms ... 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 >>>

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

ISSN 1433-8092 | Imprint