2
$\begingroup$

I am study this lecture The Complexity of Propositional Proofs. Here there is a term size of propositional formula (page 2),

Every tautology $\tau$ on $n$ variables has an $F$-proof in which thera are at most $2^{O(n)}$ formulas, each of which has size polynomial in the size of $\tau$

but here doesn't define that term. I have googled this term and I have found something similar length of propositional formula, which is defined as

The function $L(P)$ giving the length of a formula is defined by structural induction as follows:

  • $L(p_i) = 1$, for all atomic formulas $p_i$
  • $L(P ∧ Q)$ = 1 + $L(P ) + L(Q)$,
  • $L(P ∨ Q) = 1 + L(P ) + L(Q)$,
  • $L(¬P) = 1 + L(P)$.

My question is: Is the length and size of a formula the same?

Improve this question
$\endgroup$
5
  • 1
    $\begingroup$ There are several different definitions of the length or size of a formula, but the most popular one is the one you quote. The lecture probably uses the same definition; length and size are synonymous in this case. $\endgroup$
    – Yuval Filmus
    Commented Oct 16, 2015 at 14:18
  • 1
    $\begingroup$ Size never occurs in the context of a formula in the lecture you link to. Can you be more specific and give a slide number? $\endgroup$
    – Yuval Filmus
    Commented Oct 16, 2015 at 14:23
  • 1
    $\begingroup$ Again, a page number would be very useful. The survey is quite long and nobody is going to skim it, looking at all occurrences of the term size. $\endgroup$
    – Yuval Filmus
    Commented Oct 16, 2015 at 14:27
  • 1
    $\begingroup$ Which part of the lecture are you referring to? The string 'size of' does not occur in the document you link. There is a part about the 'refutation resolution width' on slide 15. Is that what you mean? $\endgroup$
    – Lieuwe Vinkhuijzen
    Commented Oct 16, 2015 at 14:38
  • 1
    $\begingroup$ Also, when referencing material you should give the authors in clear text, too. $\endgroup$
    – Raphael
    Commented Oct 16, 2015 at 15:34

1 Answer 1

Reset to default
1
$\begingroup$

There are two possible ways of defining what the length or size of the formula is:

  1. According to the size of a reasonable (and fixed!) binary encoding.

  2. According to the size of a reasonable (and fixed!) encoding over an infinite alphabet which includes symbols for all possible variables.

The definition you mention, for example, is what you get if you apply the second type of definition with respect to the prefix or postfix encoding of a formula.

Note that these two "approaches" don't by themselves defined a concrete measure of size. In cases where it matters, a concrete definition will appear, for example the one you quote. In many cases, however, the exact definition makes no difference since all definitions are "polynomially related", that is, the size of a formula varies at most polynomially between the different definitions. Your quote, for example, cares only about the size of the formulas being polynomial, and so an exact definition isn't important.

In other places, however, it is mentioned that some formula has size $O(n)$. Here the exact encoding still doesn't matter, but there is a real difference between the two options mentioned above. Consider for example the formula $x_1 \lor \cdots \lor x_n$. Under the second option, such a formula has size $\Theta(n)$. However, any reasonable binary encoding of this formula will have size $\Theta(n\log n)$, since storing the indices also takes space. From the author's statement it follows that he uses a definition of the second kind.

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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