[Haskell-cafe] Wrong Answer Computing Graph Dominators

[Denis Bueno]

I'm using the Data.Graph.Inductive.Query.Dominators library
(http://haskell.org/ghc/docs/latest/html/libraries/fgl/Data-Graph-Inductive-Query-Dominators.html)
with GHC 6.8.2.
 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, configuring with --disable-optimization
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
-------------- next part --------------
A non-text attachment was scrubbed...
Name: bad-dominators.ps
Type: application/postscript
Size: 12697 bytes
Desc: not available
Url : http://www.haskell.org/pipermail/haskell-cafe/attachments/20080415/746ed57b/bad-dominators-0001.ps