Measuring the hardness of SAT instances Lemma I am reading the paper Measuring the hardness of SAT instances by Ans&oacute;tegui, Bonet, Levy and Many&agrave; (Proc. 23rd AAAI Conf. on AI, pp.&nbsp;222&ndash;228, 2008) (PDF).I have two questions the first one is I would like to undersatnd the demonstration for the last claim. Specifically I need an example of the proof tree of $[x\rightarrow b](\Gamma)\vdash \{\Box\}$. And the second one is I would like an example of the last part of the Lemma 3, that is an example of the definition $s(\Gamma)$.


  Lemma 3 The space satisfies the following three properties:
  
  
  $s(\Gamma \cup \{\Box\})$ = 0
  For any unsatisfiable formula $\Gamma$, and any partial truth assignment $\phi$, we have $s(\phi(\Gamma))\leq s(\Gamma)$.
  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$.
  
  
  
  3 Note that, since $\Gamma$ is unsatisfiable, it either contains $\Box$ or it contains a variable with both signs.


I trying to understand the proof of that Lemma using this UNSAT formula: $\Gamma = (a+b)(a+b')(a'+c)(a'+c')$. Specifically, in this point:  "From the proof tree of
$[x \rightarrow b](\Gamma) \vdash\{\Box\}$ , adding the literal $x'$ in the clauses where
$[x \rightarrow b]$ has removed it, but preserving the structure of the
proof tree, we get a proof of $\Gamma \vdash x'$". I consider $x=a=1$ then replacing $a'$ in the formula $[a\rightarrow 1](\Gamma)$ I get $(a'+b)(a'+b')(a+c)(a+c')$ that also by resolution is $\{\Box\}$. What is wrong in my example How Do I get $\Gamma \vdash x'$?

*$\{\Box\}$ means the empty clause
First, $[a\to 1]\Gamma = (1)(1)(c)(c')$. A refutation of this consists of resolving $c$ and $c'$. Following the proof, we reinstate $a'$ to get the CNF $(1)(1)(a'+c)(a'+c')$, and then resolve $a'+c$ and $a'+c'$ to get $a'$.

Similarly, $[a\to 0]\Gamma = (b)(b')(1)(1)$, which can be refuted by resolving $b$ and $b'$. Reinstating $a$, we get $(a+b)(a+b')(1)(1)$, and resolving $a+b$ and $a+b'$ we get $a$.

Note that your notation, which is different from the paper's, is confusing you. For example, $x'$ is not the negation of $x$ but rather a new variable symbol.