5
$\begingroup$

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)

$\endgroup$
  • 1
    $\begingroup$ To find identical clauses, you can use a hash table. $\endgroup$ – Yuval Filmus Jan 18 '13 at 5:12
  • 1
    $\begingroup$ 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? $\endgroup$ – usul Jan 18 '13 at 5:47
  • $\begingroup$ 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. $\endgroup$ – usul Jan 18 '13 at 5:48
  • $\begingroup$ @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. $\endgroup$ – Salil Jan 18 '13 at 17:03
  • $\begingroup$ @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. $\endgroup$ – Salil Jan 18 '13 at 17:12
9
$\begingroup$

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

"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.

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."

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

$\endgroup$
  • $\begingroup$ Thank you for pointing this nice paper. As you have mentioned in the snippet, the paper is more focused on finding the redundancies from within a single formula, but I feel that I will be able to make use of this concept in order to finding redundancies across two or more formulae. Also, the techniques and references discussed here seem useful. Thank you. $\endgroup$ – Salil Jan 18 '13 at 17:22
  • $\begingroup$ Since two formulae can be viewed as a single formula by conjunction, or just taking the union of the sets of clauses, I thought the paper wil be useful. I think it will be difficult to find work on two different formulae. If you edit your question to give more context on how mutiple formulae arise, it would be helpful. $\endgroup$ – Vijay D Jan 18 '13 at 19:30
  • $\begingroup$ Whether the clauses are part of the same formula or different, should not make much difference. I am not sure about your latest suggestion though. What do you want to know about the generation of these formulae? Consider, that I am provided several CNF formulae by a black box. Will I be able to use the above mentioned paper for my benefit? I feel so. May be I will have to go deeper to find out how, but for now, this paper seems promising. Thanks again. $\endgroup$ – Salil Jan 19 '13 at 15:00

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.