Farid Ablayev, Marek Karpinski

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

Marek Karpinski

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

Philipp Woelfel

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

Jesper Torp Kristensen, Peter Bro Miltersen

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

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

Daniel Sawitzki

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

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

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