# Strahler of tree like refutations

I am reading the paper Measuring the hardness of SAT instances by Ansótegui, Bonet, Levy and Manyà (Proc. 23rd AAAI Conf. on AI, pp. 222–228, 2008) (PDF). I am trying to understand the last part of the demonstration of the Lemma 3 (in bold). For this, I get an example. Let be $\Gamma = (a+b)(a+b')(a'+c)(a'+c')$ then its tree-like refutation is:

Following the demonstration of the last part of the Lemma 3 (in bold), $[b\rightarrow 1]\Gamma=(1)(a)(a'+c)(a'+c')$, and adding the literal $b'$ where $[b\rightarrow 1]$ has removed it, we get $\Gamma' = (1)(a+b')(a'+c)(a'+c')$. In accordance the paper the tree-like refutation of $\Gamma'$ is a proof for $\Gamma \vdash b'$. According to the paper, similarly, for $[b\rightarrow 0]$, $[b\rightarrow 0]\Gamma = (a)(a'+c)(a'+c')$, and adding the literal $b$ where $[b\rightarrow 0]$ has removed it, we get $(a+b)(a'+c)(a'+c')$. My questions are,

1) Is there any difference between these Strahlers? for me there is not any difference, but why the author consider the function $\max$?

2) From the demonstration,

Adding a cut of $x$ to these two proofs, we get a proof of $\Gamma \vdash \Box$.

Is it a rule of sequente calculus, if yes, following wikipedia Could you help to identify who are $\Sigma$, $\Pi$, $\Delta$ and $\Sigma$?

What means cut of $x$?

Lemma 3 The space satisfies the following three properties:

1. $s(\Gamma \cup \{\Box\})$ = 0
2. For any unsatisfiable formula $\Gamma$, and any partial truth assignment $\phi$, we have $s(\phi(\Gamma))\leq s(\Gamma)$.
3. For any unsatisfiable formula $\Gamma$, if $\Box\notin\Gamma$, then there exists a variable $x$ and an assignment $\phi\colon\{x\}\to\{0,1\}$, such that $s(\phi(\Gamma))\leq s(\Gamma)-1$.

The space of a formula is the minimum measure on formulas that satisfy (1), (2) and (3). In other words, we could define the space as:3

$$s(\Gamma) = \min_{x, \overline{x}\in\Gamma, b\in\{0,1\}} \big\{ \max\{s([x\mapsto b](\Gamma))+1, s([x\mapsto\overline{b}](\Gamma))\}\;\big\}$$ when $\Box\notin\Gamma$, and $s(\Gamma\cup\{\Box\}) = 0$.

• It would really be better if you first read some lecture notes on resolution. Cut is a very basic notion in resolution, being the only inference rule in the system. Commented Oct 12, 2015 at 20:33

You have asked (at least) two questions. The answer to your first question is that sometimes it is much easier to refute a formula given that $x=0$ compared to given $x=1$. Hence the $\max$. In other cases, $x=1$ is easier. That's why we need to go over both possible values of $b$. Finally, the reason why the formula in part 3 of the lemma also maximizes over the variable $x$ is that $x$ represents the last variable which is cut (the one at the root of the tree).

The answer to your second question is as follows. The cut rule allows deriving $a \lor b$ given $a \lor x$ and $b \lor \bar{x}$. Here $a,b$ are arbitrary formulas, in this context clauses. In particular, from $x$ and $\bar{x}$ you can conclude contradiction. The cut rule is the only rule in the resolution proof system.

• Thanks, @Yuval Filmus, Could you give please some example of any formula where there are difference between their Strahlers, please? Commented Oct 12, 2015 at 21:55
• Take any formula, add $\lnot x$ to all its clauses, and add the clauses $x \lor y$ and $\lnot y$ (here $x,y$ are new variables). If $x=0$ then the resulting formula is easy to refute, but when $x=1$ you need to refute the original formula. Commented Oct 12, 2015 at 22:02
• @YuvalFilums I am reading the links that you sent in the other question math.ucla.edu/~asl/bsl/1304/1304-001.ps, according that, your example if for a DAG-resolution, is not? Commented Oct 13, 2015 at 0:59
• No, not necessarily. Tree-like refutations can also be imbalanced. I suggest that you continue reading and only after thoroughly understanding the material, if you still have any questions, you ask them. Commented Oct 13, 2015 at 3:48
• from your comment I construct the formula $(x+y)(\lnot y)(a+b+\lnot x)(a+\lnot b+\lnot x)(\lnot a + c + \lnot x)(\lnot a + \lnot c + \lnot x)$. And really when $x=0$ then it is easy to refute, but when $x=1$ I get $((\lnot y)(a+b+\lnot x)(a+\lnot b+\lnot x)(\lnot a + c + \lnot x)(\lnot a + \lnot c + \lnot x)$, which using resolution is imposible to refute. Commented Oct 14, 2015 at 10:21