# Wrong Answer Computing Graph Dominators

Denis Bueno dbueno at gmail.com
Sat Apr 12 11:03:18 EDT 2008

I'm using the Data.Graph.Inductive.Query.Dominators library
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
-------------- next part --------------
A non-text attachment was scrubbed...