Cheap and Secure Web Hosting Provider : See Now

# The Space of an Unsatisfiable Formula

, ,
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 demonstration of the last part 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, $[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'$. The natural question, I think so, How it is posible that the tree-like refutation of $\Gamma'$ be a proof for $\Gamma \vdash b'$ if $\Gamma \neq \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$.

###### Answered By : Yuval Filmus

Here is the original refutation:

1. From $a'+c$ and $a'+c'$ deduce $a'$.
2. From $a$ and $a'$ deduce $\square$.

When you add $b'$ back, you get:

1. From $a'+c$ and $a'+c'$ deduce $a'$.
2. From $a+b'$ and $a'$ deduce $b'$.

More generally, since the only difference between $\Gamma$ and $\Gamma'$ is the addition of $b'$, it is not hard to prove by induction that for every line $\ell$ proved in the refutation of $\Gamma$, the corresponding line in the corresponding $\Gamma'$ proof is either $\ell$ or $\ell+b'$. Hence the $\Gamma'$ proof proves either $\square$ or $b'$. It can happen that it indeed proves $\square$, in which case we can deduce $b'$ by weakening, which is an admissible rule for resolution space (we can get rid of it without increasing the space).