Cheap and Secure Web Hosting Provider : See Now

Measuring the hardness of SAT instances Lemma

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

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.