<blockquote>
  <p><a href="http://fmv.jku.at/papers/HeuleJarvisaloBiere-SAT11.pdf">Efficient CNF Simplification based on Binary Implication Graphs</a>, Marijn Heule, Matti Jarvisalo, and Armin Biere, 2011</p>
  
  <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>
</blockquote>

<p>I recommend Section 2.1 of the paper which reviews known simplification techniques.</p>

CC BY-SA 3.0
2013-01-18T17:22:22.833Z
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.
Salil
CC BY-SA 3.0
2013-01-18T19:30:25.743Z
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.
Vijay D
CC BY-SA 3.0
2013-01-19T15:00:00.610Z
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.
Salil
CC BY-SA 3.0
2013-01-18T05:54:36.040Z
2013-01-18T05:54:36.040Z
Vijay D
<p>This is bothering me for some time. Consider that I have a set of CNF formulae:</p>

<p>$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)$</p>

<p>$F_2 = \left( B \lor F \lor G \right)$</p>

<p>$F_3 = \left( A \lor B \lor D \right)$</p>

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

<p>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.</p>

<p>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...)</p>

<p>Is anyone aware of such problems? I know concepts such as <a href="http://en.wikipedia.org/wiki/Tree_decomposition">Junction Trees</a> in machine learning, <a href="http://en.wikipedia.org/wiki/Memoization">Memoization</a> 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.</p>

<p>Thanks,</p>

<p>Salil</p>

<p>(PS: I posted this earlier on math.SE, but could not get any ideas, and was instead suggested to post this problem here)</p>

CC BY-SA 3.0
2013-01-18T05:12:57.813Z
To find identical clauses, you can use a hash table.
Yuval Filmus
CC BY-SA 3.0
2013-01-18T05:47:26.113Z
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
CC BY-SA 3.0
2013-01-18T05:48:38.173Z
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
CC BY-SA 3.0
2013-01-18T17:03:52.403Z
@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
CC BY-SA 3.0
2013-01-18T17:12:14.443Z
@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
<lo.logic><lattice>
CNF Rule hierarchy discovery
Salil
# CNF Rule hierarchy discovery

(Asked by: username_0 on 2013-01-18)

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](http://en.wikipedia.org/wiki/Tree_decomposition) in machine learning, [Memoization](http://en.wikipedia.org/wiki/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,

username_0

(PS: I posted this earlier on math.SE, but could not get any ideas, and was instead suggested to post this problem here)

**Tags:** lo.logic, lattice

> **Comments:**
> **username_1**: To find identical clauses, you can use a hash table.  
> **username_2**: 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?  
> **username_2**: 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.  
> **username_0**: @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.  
> **username_0**: @username_2: 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.  

---

## 1 answers

### Answer by username_3 on 2013-01-18. Score: 9 | Accepted answer

> [Efficient CNF Simplification based on Binary Implication Graphs](http://fmv.jku.at/papers/HeuleJarvisaloBiere-SAT11.pdf), 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.

> **Comments:**
> **username_0**: 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.  
> **username_3**: 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.  
> **username_0**: 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.  

---

