10
$\begingroup$

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?

$\endgroup$
  • $\begingroup$ 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. $\endgroup$ – Kaveh Nov 18 '10 at 17:11
  • $\begingroup$ 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)$. $\endgroup$ – Kaveh Nov 18 '10 at 17:14
  • $\begingroup$ 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$. $\endgroup$ – MassimoLauria Nov 18 '10 at 17:36
  • 1
    $\begingroup$ Notice that regarding refutation length you easily have $$Length(A \lor B) \leq Length(B)|A|+Length(A)$$ $\endgroup$ – MassimoLauria Nov 18 '10 at 17:37
  • $\begingroup$ The trivial space upper bound actually requires one less clause in memory. I edited accordingly. $\endgroup$ – MassimoLauria Nov 19 '10 at 13:19
7
$\begingroup$

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.

$\endgroup$
  • 2
    $\begingroup$ Welcome, Jakob! $\endgroup$ – arnab Jan 17 '11 at 8:04
  • 1
    $\begingroup$ 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. $\endgroup$ – Suresh Venkat Jan 17 '11 at 8:07
  • $\begingroup$ Hi Jakob, it is nice to see you here. (ps: I think you have passed the threshold.) $\endgroup$ – Kaveh Jan 17 '11 at 9:29
  • $\begingroup$ 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). $\endgroup$ – MassimoLauria Jan 17 '11 at 9:49

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.