CNF Rule hierarchy discovery

Question

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)

Answer 1

This question has received an answer on CSTheory.SE by Vijay D, which I include below. Primary intent of this post is to remove this question from the Unanswered queue.

---

Efficient CNF Simplification based on Binary Implication Graphs, Marijn Heule, Matti Jarvisalo, and Armin Biere, 2011

<p>"This paper develops techniques for efficiently detecting and removing redundancies from CNF (conjunctive normal form) formulas based on the underlying binary clause structure (i.e., the binary implication graph) of the formulas. </p>

<p>In addition to considering known simplification techniques (hidden tautology elim- ination (HTE), hyper binary resolution (HBR), failed literal elimination over binary clauses, equivalent literal substitution, and transitive reduction  of the binary implication graph), we introduce the novel technique of hidden literal elimination (HLE) that removes so-called hidden literals from clauses without affecting the set of satisfying assignments."</p>

I recommend Section 2.1 of the paper which reviews known simplification techniques.