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 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:

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

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

  • 1
    $\begingroup$ We can't help you read the paper line by line. Try to find more introductory material on the topic, for example by following some references, say the ones introducing the space complexity measure. Another option is looking for relevant course material, for example Jakob Nordström's csc.kth.se/~jakobn/teaching/proofcplx11/lectures/Lecture04.pdf. More generally, you should try being more independent. Reading papers is a skill you have to develop. $\endgroup$ Sep 27, 2015 at 12:25
  • $\begingroup$ @YuvalFilmus I have edited my question $\endgroup$
    – juaninf
    Sep 27, 2015 at 15:13
  • 1
    $\begingroup$ Note that after someone answers this question you won't be able to add another one to this post, but rather you will have to ask a new question. $\endgroup$ Sep 27, 2015 at 15:17
  • $\begingroup$ the questioner is not asking for help to read line by line the whole paper, but only a very tricky section, & personally think this is an excellent use of stackexchange/CS site as far as questions, but presume that experts with the knowledge to answer such questions could be rare. it would also be better if this paper talked about SAT resolution proof trees earlier in the paper, of which there is a lot of literature & it is studying in particular. try also Computer Science Chat for this type of query. $\endgroup$
    – vzn
    Sep 28, 2015 at 22:56

1 Answer 1


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.

  • $\begingroup$ understand @YuvalFilmus, only a one doubt more please. Is the choose of $x=a$ the minimum of the tree-like refutations among all the Strahlers of tree-like refutations of the formula? $\endgroup$
    – juaninf
    Sep 27, 2015 at 17:20
  • $\begingroup$ @juaninf I don't know, you tell me. $\endgroup$ Sep 27, 2015 at 19:31
  • $\begingroup$ according my tree it is yes. $\endgroup$
    – juaninf
    Sep 27, 2015 at 23:39
  • $\begingroup$ sorry by my questions, but according to the paper $(1)(1)(a'+c)(a'+c')$ is proof of $\Gamma \vdash a'$ but, is it possible? I make this last question because the first two clauses were replace with ones. $\endgroup$
    – juaninf
    Sep 27, 2015 at 23:43
  • $\begingroup$ No, $(1)(1)(a'+c)(a'+c')$ is not a proof of anything. It's a formula. It implies $a'$, though, which you can prove by resolving the last two clauses. $\endgroup$ Sep 28, 2015 at 3:26

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.