World's most popular travel blog for travel bloggers.

# Strahler of tree like refutations

, ,
Problem Detail:

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$.

###### Answered By : Yuval Filmus

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.