# Restricted read twice BDDs and context free grammars

Several papers give poly-time algorithms for constrained paths on labelled graphs, e.g. [1]

## Quote:

Given an alphabet Σ, a (directed) graph G whose edges are weighted and Σ-labeled, and a formal language L ⊆ Σ∗ , the formal-language-constrained shortest/simple path problem con- sists of finding a shortest (simple) path p in G complying with the additional constraint that l(p) ∈ L. Here l(p) denotes the unique word obtained by concatenating the Σ-labels of the edges along the path p. (1) We show that the formal-language-constrained shortest path problem is solvable efficiently in polynomial time when L is restricted to be a context-free language (CFL).

Can this be used for restricted read twice BDDs (Binary Decision Diagram)?

Consider BDD where every variables occurs twice and the order of all paths root->T is restricted to:

1 .. n n .. 1 (this is palindrome)

Treat the BDD as edge labelled digraph where the true edge of variable is labelled as +variable and the false edge as -variable.

Some paths in the digraph are "BDD inconsistent" - if a variable takes both values.

Looks like CFG constraint can help to find "consistent" paths.

It is possible to construct CFG that accepts all palindromes and only palindromes (over the alphabet U {+variable,-variable}.

Finding a path from the root to "true" constrained by the above CFG will give a consistent satisfying assignment - the first half of the path is correct because a variable occurs only once and the second part is the reverse.

Is this correct (computer experiments suggest it is)?

A different grammar may give different restriction.

Is this published somewhere?

To my humble knowledge this is one of the very few examples of read twice BDD supporting polytime SAT query.

EDIT: The problem I am trying to solve is to find types of read twice BDDs which allow polytime SAT query with the help of CFGs. The above construction gives example for the case when the order of the variables is restricted to a palindrome, hence the (possibly incorrect) description "restricted" (because of the restriction of the order). I am not familiar with CFGs.

EDIT: Simple read twice BDD on x,y. The concatenation of edge labels give the palindrome word: "+x -y -y +x"

(the graph may need copy/paste of the link)

-
Do you think that you should ask this at cs theory ? –  Graviton Dec 29 '10 at 15:00
I asked there and wait to be booted just for asking... –  Leon Leon Dec 29 '10 at 16:28
If you're not familiar with CFGs then you should read about them somewhere. It's a standard undergraduate topic so there must be lots of good textbooks covering it. –  Yuval Filmus Dec 29 '10 at 22:08
Can you recommend introduction to CFGs for dummies? –  Leon Leon Dec 30 '10 at 8:26

I think there may be a simpler algorithm, which uses straightforward dynamic programming.

If I understand you correctly, you're interested in a BDD with $2n+1$ levels, the first and last containing the root and sink, respectively (we just delete all vertices from which $T$ is unreachable). Edges only go between adjacent levels, with the correct annotation.

Let's concentrate on the middle three levels $A,B,C$. Thus all $A \rightarrow B$ and $B \rightarrow C$ are labelled by $\pm x_n$.

When is a node $c \in C$ reachable from a node $a \in A$? There must be some path going through $B$ with edges labeled by the same polarity of $x_n$. We can delete level $B$ and replace it by arrows going directly from $A$ to $C$; we label each arrow by the allowable assignments for $x_n$.

Suppose there is some path from the root to a vertex $c \in C$. What is its provenance? It must have passed through some vertex $a \in A$ via some edge $e$ going into $a$. We can shortcut the edge $e$ so that it goes directly to $c$, carrying both its original label and the new descriptive label concerning $x_n$. In this way, we can erase level $A$ as well.

Having eliminated both levels $A,B$, we have removed $x_n$ from the BDD, and we can iterate our steps; having done this $n$ times, we will end up with a parametrization of all solutions to the BDD.

Edit: Here is a run of the algorithm on your example. The graph is composed of five levels: $$L_0 = \{x_0\},\; L_1 = \{y_0,y_1\},\; L_2 = \{y_2\},\; L_3 = \{x_2,x_3\},\; L_4 = \{T\}.$$ There are 10 edges, which we list as tuples of from/to/label: $$(x_0,y_0,+x),(x_0,y_1,-x),(y_0,y_2,+y),(y_0,y_2,-y),(y_1,y_2,+y),$$ $$(y_2,x_2,+y),(y_2,x_3,-y),(x_2,T,-x),(x_3,T,-x),(x_3,T,+x).$$

First iteration: the three middle levels are $L_1,L_2,L_3$. We start by eliminating $L_2$. Edges involving $y_2$ are removed, and the following edges are added: $$(y_0,x_2,+y),(y_0,x_3,-y),(y_1,x_2,+y).$$ Next we eliminate $L_1$. Edges involving $y_0,y_1$ are removed, and the following edges are added: $$(x_0,x_2,+x+y),(x_0,x_3,+x-y),(x_0,x_2,-x+y).$$ We are left with levels $L_0,L_3,L_4$ and the following 6 edges: $$(x_0,x_2,+x+y),(x_0,x_3,+x-y),(x_0,x_2,-x+y),(x_2,T,-x),(x_3,T,-x),(x_3,T,+x).$$

Second iteration: the three middle levels are $L_0,L_3,L_4$. We eliminate $L_3$. Edges involving $x_2,x_3$ are removed, and the following edges are added: $$(x_0,T,-x+y),(x_0,T,+x-y).$$ This gives us the answer.

Naively following the algorithm might give too many edges. However, notice that upon eliminating a variable $x_i$, we need only retain one assignment of the variables $x_{i+1},\ldots,x_n$ for each polarity of $x_i$. This way we won't get all solutions, but we can decide whether there is a solution.

However, it is easy to change the algorithm so that it maintains a succinct representation of all solutions. I leave that as an exercise for the reader.

-
Thank you. Sorry but I don't understand your construction. My constructions uses even length palindromes though I can use $2n+1$ levels by just duplicating a variable. Since you comment on CFGs can you find a better CFG instead of a palindromic one ? –  Leon Leon Dec 29 '10 at 14:41
Presumably this DP algorithm is better than the one in the paper, since this one is more specialized. I think it is $O(N^2)$, where $N$ is the number of edges. –  Yuval Filmus Dec 29 '10 at 22:06