# 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: I posted this earlier on math.SE, but could not get any ideas, and was instead suggested to post this problem here)

• To find identical clauses, you can use a hash table. – Yuval Filmus Jan 18 '13 at 5:12
• Why does memoization fail? I think the straightforward approach would be to find some canonical encoding of formulae (e.g. sort clauses by length, then alphabetically by variable, ...) and memoize both clauses and entire formulae. Would this work? – usul Jan 18 '13 at 5:47
• Also, is it necessary to use any advanced tricks? It seems like in the time (and space) you use to determine if you've seen a formula before, which requires at least one pass over it, you could simply evaluate it. – usul Jan 18 '13 at 5:48
• @Yuval: Yes, a hashtable would be useful as I mentioned in the question (memoization). However, the problem would be to efficiently track the identical clauses. – Salil Jan 18 '13 at 17:03
• @usul: Thank you for the suggestions. I wanted to know if there are techniques which would optimize this process. Regarding the point of evaluating instead of memorizing, I feel that once the hierarchy is constructed, it can be used for all future evaluations (since the literal values might change over time) and that would save time. – Salil Jan 18 '13 at 17:12