<p>I wanted to post this as a comment, but since I cannot quite figure out the way to do so I guess it will have to be an "answer" instead. </p>

<p>I agree that the question is nice. Of course, the same question can also be asked about the length of resolution refutations (i.e., the number of clauses occurring in the refutation, counted with repetitions) and the width of refutation (i.e., the size of, or number of literals occurring in, the largest clause in the refutation).</p>

<p>In all of these cases there are "obvious" upper bounds, but it is not clear to me whether one should expect matching lower bounds or not. Therefore, I wanted to add one question and one comment.</p>

<p>The question concerns refutation length. It seems reasonable to believe that the bound for length stated in the comment by Massimo is tight, but do we know this? </p>

<p>And the comment concerns width. Note that for this measure, a moment of thought reveals that a direct sum lower bound does <em>not</em> hold. For width, one instead refutes the whole $A$-formula for each clause $B_i$, in width $w_A$, say, plus the width of the $B$-formula, and then one refutes the $B$-formula in width $w_B$. Assuming that both formulas have constant initial width, the width of the refutation of the direct sum will be essentially $\max (w_A, w_B)$.</p>

<p>This is of course an easy observation, but the point is that it might indicate that the question for space could be tricky. This is so since almost all lower bounds on space in refutation we know of go via width lower bounds. (That is, the space lower bounds were derived independently, but with hindsight they all follow as a corollary from the beautiful paper "A Combinatorial Characterization of Resolution Width" by Atserias and Dalmau.) But if there is a direct sum theorem for resolution clause space, it will not follow from width lower bounds but has to be argued directly, which at least so far has seemed to be much harder. But of course there might be some easy argument that I am missing.</p>

CC BY-SA 2.5
2011-01-17T08:04:29.050Z
Welcome, Jakob!
arnab
CC BY-SA 2.5
2011-01-17T08:07:28.390Z
Comments are unfortunately limited to people with a reputation of at least 50 - this is an oddity of the software and relates to spam-prevention. I'm sure you'll cross that threshold rapidly.
Suresh Venkat
CC BY-SA 2.5
2011-01-17T09:29:16.563Z
Hi Jakob, it is nice to see you here. (ps: I think you have passed the threshold.)
Kaveh
CC BY-SA 2.5
2011-01-17T09:49:19.040Z
Hi Jakob, I wonder if this kind of statement has some consequences regarding trade-offs.  As a lower bound technique that would not be a very powerful tool: the formula length squares while space increases linearly.  Anyway this property could lead to formula with small width and large space (notice that also the width grows if a non constant number of repetition are done).
MassimoLauria
CC BY-SA 2.5
2011-01-17T07:47:30.483Z
2011-01-17T07:47:30.483Z
Jakob Nordstrom
<p>Resolution is a scheme to prove unsatisfiability of CNFs.  A proof in resolution is a logical deduction of the empty clause for the initial clauses in of the CNF.  In particular any initial clause can be inferred, and from two clauses $A \lor x$ and $B \lor \neg{x}$ the clause $A \lor B$ can be deduced as well.  A refutation is a sequence of deductions which ends with an empty clause.</p>

<p>If such refutation is implemented, we can consider a procedure that keeps some clauses in memory.  In case a non-initial clause must be used again and it is not in memory anymore, the algorithm should must it again from scratch or from the ones in memory.</p>

<p>Let $Sp(F)$ the smallest number of clauses to be kept in memory to reach the empty clauses. This is called the <em>clause space</em> complexity of $F$. We say say that $Sp(F)=\infty$ is $F$ is satisfiable.</p>

<p>The problem I'm suggesting is this: consider two CNFs $A=\bigwedge_{i=1}^m A_i$ and $B=\bigwedge_{j=1}^n B_j$, and let the CNF</p>

<p>$$A \lor B = \bigwedge_{i=1}^m \bigwedge_{j=1}^n A_i \lor B_j$$
</p>

<p>What is the relation of $Sp(A \lor B)$ with $Sp(A)$ and $Sp(B)$? </p>

<p>The obvious upper bound is $Sp(A \lor B) \leq Sp(A) + Sp(B) -1$. Is this tight?</p>

CC BY-SA 2.5
2010-11-18T17:11:10.330Z
Nice question! Do you know the answer for the *size* of the direct sum? I guess the worst case is when the A and B do not have shared variables. An interesting case might be when A and B are the same up to renaming of the variable. Btw, I don't see how you get that upper bound, it feels like it can be much worse.
Kaveh
CC BY-SA 2.5
2010-11-18T17:14:08.253Z
I now see the upper bound, you can copy the refutation for $B$ for $A_i \lor B_j$ for $1 \leq j \leq n$ to get $A_i$ one by one for each $1 \leq i \leq m$ and then do the refutation for $A$. The size will be around $m.(Size(B)+O(1))+Size(A)$.
Kaveh
CC BY-SA 2.5
2010-11-18T17:36:06.047Z
You are right. I forgot to mention that, but of course the most interesting case in term of a lower bound is when A and B do not share variables. That is exactly the case I am actually interested in. Considering different A and B is better to inductively obtain a result for $F_1 \lor F_2 \lor \ldots F_k$ where $F_i$ are disjoint variable copies of the same $F$.
MassimoLauria
CC BY-SA 2.5
2010-11-18T17:37:13.813Z
Notice that regarding refutation length you easily have $$Length(A \lor B) \leq Length(B)|A|+Length(A)$$
MassimoLauria
CC BY-SA 2.5
2010-11-19T13:19:55.417Z
The trivial space upper bound actually requires one less clause in memory. I edited accordingly.
MassimoLauria
<cc.complexity-theory><lo.logic><proof-complexity><proof-search>
A direct sum theorem for Resolution clause space complexity?
MassimoLauria
# A direct sum theorem for Resolution clause space complexity?

(Asked by: username_0 on 2010-11-18)

Resolution is a scheme to prove unsatisfiability of CNFs. A proof in resolution is a logical deduction of the empty clause for the initial clauses in of the CNF. In particular any initial clause can be inferred, and from two clauses $A \lor x$ and $B \lor \neg{x}$ the clause $A \lor B$ can be deduced as well. A refutation is a sequence of deductions which ends with an empty clause.

If such refutation is implemented, we can consider a procedure that keeps some clauses in memory. In case a non-initial clause must be used again and it is not in memory anymore, the algorithm should must it again from scratch or from the ones in memory.

Let $Sp(F)$ the smallest number of clauses to be kept in memory to reach the empty clauses. This is called the *clause space* complexity of $F$. We say say that $Sp(F)=\infty$ is $F$ is satisfiable.

The problem I'm suggesting is this: consider two CNFs $A=\bigwedge\_{i=1}^m A\_i$ and $B=\bigwedge\_{j=1}^n B\_j$, and let the CNF

$$A \lor B = \bigwedge\_{i=1}^m \bigwedge\_{j=1}^n A\_i \lor B\_j$$

What is the relation of $Sp(A \lor B)$ with $Sp(A)$ and $Sp(B)$?

The obvious upper bound is $Sp(A \lor B) \leq Sp(A) + Sp(B) -1$. Is this tight?

**Tags:** cc.complexity-theory, lo.logic, proof-complexity, proof-search

> **Comments:**
> **username_1**: Nice question! Do you know the answer for the *size* of the direct sum? I guess the worst case is when the A and B do not have shared variables. An interesting case might be when A and B are the same up to renaming of the variable. Btw, I don't see how you get that upper bound, it feels like it can be much worse.  
> **username_1**: I now see the upper bound, you can copy the refutation for $B$ for $A_i \lor B_j$ for $1 \leq j \leq n$ to get $A_i$ one by one for each $1 \leq i \leq m$ and then do the refutation for $A$. The size will be around $m.(Size(B)+O(1))+Size(A)$.  
> **username_0**: You are right. I forgot to mention that, but of course the most interesting case in term of a lower bound is when A and B do not share variables. That is exactly the case I am actually interested in. Considering different A and B is better to inductively obtain a result for $F_1 \lor F_2 \lor \ldots F_k$ where $F_i$ are disjoint variable copies of the same $F$.  
> **username_0**: Notice that regarding refutation length you easily have $$Length(A \lor B) \leq Length(B)|A|+Length(A)$$  
> **username_0**: The trivial space upper bound actually requires one less clause in memory. I edited accordingly.  

---

## 1 answers

### Answer by username_2 on 2011-01-17. Score: 7

I wanted to post this as a comment, but since I cannot quite figure out the way to do so I guess it will have to be an "answer" instead.

I agree that the question is nice. Of course, the same question can also be asked about the length of resolution refutations (i.e., the number of clauses occurring in the refutation, counted with repetitions) and the width of refutation (i.e., the size of, or number of literals occurring in, the largest clause in the refutation).

In all of these cases there are "obvious" upper bounds, but it is not clear to me whether one should expect matching lower bounds or not. Therefore, I wanted to add one question and one comment.

The question concerns refutation length. It seems reasonable to believe that the bound for length stated in the comment by Massimo is tight, but do we know this?

And the comment concerns width. Note that for this measure, a moment of thought reveals that a direct sum lower bound does *not* hold. For width, one instead refutes the whole $A$-formula for each clause $B\_i$, in width $w\_A$, say, plus the width of the $B$-formula, and then one refutes the $B$-formula in width $w\_B$. Assuming that both formulas have constant initial width, the width of the refutation of the direct sum will be essentially $\max (w\_A, w\_B)$.

This is of course an easy observation, but the point is that it might indicate that the question for space could be tricky. This is so since almost all lower bounds on space in refutation we know of go via width lower bounds. (That is, the space lower bounds were derived independently, but with hindsight they all follow as a corollary from the beautiful paper "A Combinatorial Characterization of Resolution Width" by Atserias and Dalmau.) But if there is a direct sum theorem for resolution clause space, it will not follow from width lower bounds but has to be argued directly, which at least so far has seemed to be much harder. But of course there might be some easy argument that I am missing.

> **Comments:**
> **username_3**: Welcome, Jakob!  
> **username_4**: Comments are unfortunately limited to people with a reputation of at least 50 - this is an oddity of the software and relates to spam-prevention. I'm sure you'll cross that threshold rapidly.  
> **username_1**: Hi Jakob, it is nice to see you here. (ps: I think you have passed the threshold.)  
> **username_0**: Hi Jakob, I wonder if this kind of statement has some consequences regarding trade-offs.  As a lower bound technique that would not be a very powerful tool: the formula length squares while space increases linearly.  Anyway this property could lead to formula with small width and large space (notice that also the width grows if a non constant number of repetition are done).  

---

