A direct sum theorem for Resolution clause space complexity?

Question

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?

Answer 1

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.