1
$\begingroup$

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 last part of the demonstration 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:

enter image description here

Following the demonstration of the last part of the Lemma 3 (in bold), $[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'$. According to the paper, similarly, for $[b\rightarrow 0]$, $[b\rightarrow 0]\Gamma = (a)(a'+c)(a'+c')$, and adding the literal $b$ where $[b\rightarrow 0]$ has removed it, we get $(a+b)(a'+c)(a'+c')$. My questions are,

1) Is there any difference between these Strahlers? for me there is not any difference, but why the author consider the function $\max$?

2) From the demonstration,

Adding a cut of $x$ to these two proofs, we get a proof of $\Gamma \vdash \Box$.

Is it a rule of sequente calculus, if yes, following wikipedia Could you help to identify who are $\Sigma$, $\Pi$, $\Delta$ and $\Sigma$?

What means cut of $x$?

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

$\endgroup$
  • 1
    $\begingroup$ It would really be better if you first read some lecture notes on resolution. Cut is a very basic notion in resolution, being the only inference rule in the system. $\endgroup$ – Yuval Filmus Oct 12 '15 at 20:33
1
$\begingroup$

You have asked (at least) two questions. The answer to your first question is that sometimes it is much easier to refute a formula given that $x=0$ compared to given $x=1$. Hence the $\max$. In other cases, $x=1$ is easier. That's why we need to go over both possible values of $b$. Finally, the reason why the formula in part 3 of the lemma also maximizes over the variable $x$ is that $x$ represents the last variable which is cut (the one at the root of the tree).

The answer to your second question is as follows. The cut rule allows deriving $a \lor b$ given $a \lor x$ and $b \lor \bar{x}$. Here $a,b$ are arbitrary formulas, in this context clauses. In particular, from $x$ and $\bar{x}$ you can conclude contradiction. The cut rule is the only rule in the resolution proof system.

$\endgroup$
  • $\begingroup$ Thanks, @Yuval Filmus, Could you give please some example of any formula where there are difference between their Strahlers, please? $\endgroup$ – juaninf Oct 12 '15 at 21:55
  • $\begingroup$ Take any formula, add $\lnot x$ to all its clauses, and add the clauses $x \lor y$ and $\lnot y$ (here $x,y$ are new variables). If $x=0$ then the resulting formula is easy to refute, but when $x=1$ you need to refute the original formula. $\endgroup$ – Yuval Filmus Oct 12 '15 at 22:02
  • $\begingroup$ @YuvalFilums I am reading the links that you sent in the other question math.ucla.edu/~asl/bsl/1304/1304-001.ps, according that, your example if for a DAG-resolution, is not? $\endgroup$ – juaninf Oct 13 '15 at 0:59
  • $\begingroup$ No, not necessarily. Tree-like refutations can also be imbalanced. I suggest that you continue reading and only after thoroughly understanding the material, if you still have any questions, you ask them. $\endgroup$ – Yuval Filmus Oct 13 '15 at 3:48
  • $\begingroup$ from your comment I construct the formula $(x+y)(\lnot y)(a+b+\lnot x)(a+\lnot b+\lnot x)(\lnot a + c + \lnot x)(\lnot a + \lnot c + \lnot x)$. And really when $x=0$ then it is easy to refute, but when $x=1$ I get $((\lnot y)(a+b+\lnot x)(a+\lnot b+\lnot x)(\lnot a + c + \lnot x)(\lnot a + \lnot c + \lnot x)$, which using resolution is imposible to refute. $\endgroup$ – juaninf Oct 14 '15 at 10:21

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.