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.
[1] FORMAL-LANGUAGE-CONSTRAINED PATH PROBLEMS∗ CHRIS BARRETT† , RIKO JACOB‡ , AND MADHAV MARATHE†
EDIT: Simple read twice BDD on x,y. The concatenation of edge labels give the palindrome word: "+x -y -y +x"
The graph is at: https://ll0x.wdfiles.com/local--files/admin%3Amanage/aa.png
(the graph may need copy/paste of the link)