Wrong Answer Computing Graph Dominators

I'm using the Data.Graph.Inductive.Query.Dominators library (http://haskell.org/ghc/docs/latest/html/libraries/fgl/Data-Graph-Inductive-Q...). The library is a bit spare on comments, so I may or may not be using it correctly. My goal is to compute the set of nodes that dominate two different nodes of a DAG, with respect to one initial node. My approach is: import qualified Data.Graph.Inductive.Graph as Graph import qualified Data.Graph.Inductive.Query.Dominators as Dom uips = intersect domConfl domAssigned :: [Graph.Node] -- my goal domConfl = fromJust $ lookup conflNode domFromLastd -- dominators of first node domAssigned = fromJust $ lookup (negate conflNode) domFromLastd -- dominators of second node domFromLastd = Dom.dom conflGraph lastd -- source node I compute the dominators individually and my answer is their intersection. When I call the dom function, my assumption is that I need to pass it the source node, and it tells me, for any node x to which there is a path from the source, the list of nodes for which *any path* from source to x must touch, i.e., the list of dominators of x. The DAG in question is attached as a postscript file, which is generated by `dot -Tps` using the output of the Graphviz module directly from the graph object. The nodes for which I'm computing dominators are labeled -2 and 2 (that is, conflNode = 2). The problem is that I think the answer is wrong. In particular I think the set of dominators for -2 is {20, -2}, and the set for 2 is {20, 2}. Their intersection is {20}, which is what I expect. But what I am getting is: --> uips = [-9,20] --> domConfl = [2,-9,20] --> domAssigned = [-2,-9,-12,20] --> lastd = 20 But -9 is not a dominator for 2, since 20,-7,8,6,2 is a path from 20 to 2 that does not touch 9. -9 is also not a dominator for -2, since 20,-7,8,6,-2 is a path from 20 to -2 not touching 9. Am I missing something? I've simplified the code above slightly from the original code in order to ignore some irrelevancies. The original code is for computing a learned clause in a SAT solver. The code in the state that will reproduce the error above is available via a git clone: git clone http://fid.stygian.net/dpllsat Build via cabal, using the --disable-optimization option to configure in order to enable assertions, then run: ./dist/build/dsat/dsat ./tests/problems/uf20/uf20-0226.cnf The graph should be saved in conflict.dot and with `dot -Tps -o conflict.ps conflict.dot` you should be able to turn it into the ps file attached. The problematic code referenced above starts on line 759. -- Denis
participants (1)
-
Denis Bueno