# CNF Rule hierarchy discovery

This is bothering me for some time. Consider that I have a set of CNF formulae:

$F_1 = \left( A \lor B \lor C \right) \land \left( C \lor D \lor E \right) \land \left( B \lor F \lor G \right)$

$F_2 = \left( B \lor F \lor G \right)$

$F_3 = \left( A \lor B \lor D \right)$

Now, given the values (T/F) of the literals ($A$, $B$, $\cdots$), I wish to evaluate these formulae.

However, the point is that, if we observe closely, we can see that formula $F_1$ subsumes formula $F_2$ (i.e., while evaluating $F_1$, I will be automatically evaluating $F_2$). If I evaluate $F_1$ first followed by $F_2$, I will be unnecessarily repeating the efforts (since I already evaluated the $3^{rd}$ clause in $F_1$, I could have used that result for $F_2$, if I had some way of knowing it). Again, in case of $F_1$ and $F_3$, they do share some parts of the $1^{st}$ clause.

So, the question is, whether I can re-use the work done while performing this evaluation, by discovering the relationships (or hierarchy) of these CNF rules. I would like some scheme which tells me to evaluate $\left(A \lor B \right)$, use that for $F_1$ and $F_3$, tells me to evaluate $F_2$ before $F_1$ and directly use that result while evaluating $F_1$ (and so on...)

Is anyone aware of such problems? I know concepts such as Junction Trees in machine learning, Memoization in DP, or data structures like Trie which loosely achieve the same, but I am not able to fit my problem to these formulations. Any help would be greatly appreciated.

Thanks,

Salil

(PS: hoping that I did not post this on the wrong forum on SE)

-
There is a theoretical computer science stack exchange: cstheory.stackexchange.com I don't know if that works better or not. – Henry B. Jan 17 '13 at 4:52
@HenryB., Thank you for your suggestion. If I do not receive any inputs here, I will definitely try this question there. – Salil Jan 17 '13 at 6:02
I case if someone wants to follow this up, I have created a new question on CSTheory: cstheory.stackexchange.com/questions/16133/… – Salil Jan 20 '13 at 14:08