Transitive closure

Given two implications a → b and b → c using the property of transitivity we can deduce another implication a → c. It is generally good to know many implications because they are used in binary and hyper binary resolutions. If implications are stored as a directed graph we can apply transitive closure on the graph to deduce many more implications. However, transitive closure is very expensive (O(|V|⋅(|V|+|E|)) time), memory hungry and not always gives the expected benefits because the implication might be already very dense.

My idea is to do the transitive closure when the graph is sparse and many new binaries can be found. There are two ways to compute the density of a directed graph:

• log(|E|)/log(|V|) which returns a value in interval (-∞, 2)
• 2*|E|/(|V|⋅(|V|-1)) which returns a value in interval [0, 2]
  

I chose the former, though I plan evaluate the later in the near feature. I tested a few values and figured out that 1.10 is the optimal threshold. If the graph is denser than 1.10 then the transitive closure is too expensive so it is omitted. The next figure shows the results for three thresholds 1.05 (blue), 1.10 (green) and 1.20 (red). Transitive closure has some benefits, but too much of it can slow down the search.