# The Space of an Unsatisfiable Formula

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

• I can't understand your question. First, you don't have anything in your post that ends with a question mark. Second, I'm struggling to parse/understand the sentence "The natural question, I think so, How it is posible that the tree-like refutation of ...". How about breaking that sentence down into multiple smaller pieces, and make explicit what your question is, and what your thoughts are? – D.W. Sep 29 '15 at 20:24

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

• when you write "since the only difference between $\Gamma$ and $\Gamma'$ is the adition of $b'$", Do you want to say the difference between $\Gamma$ and $\Gamma'$ when $b\rightarrow 1$? – juaninf Oct 12 '15 at 1:01
• @juaninf I am using your notation. – Yuval Filmus Oct 12 '15 at 6:31
• what book you recommend for learn concepts as "admissible rule" – juaninf Oct 12 '15 at 12:50
• @juaninf I read about it in Structural Proof Theory by Negri and von Plato, but I'm not sure that's the best introduction (especially not in this context). There are lecture notes by Jakob Nordström on proof complexity that you can find on his homepage. – Yuval Filmus Oct 12 '15 at 13:00