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 decision algorithm beame_pitassi described in the Figure 1 in paper and showed below. This algorithm searches for the space of an UNSAT formula.

enter image description here

I am studying that algorithm using the following formula $\Gamma = (a\vee b)(a\vee \lnot b)(\lnot a \vee c)(\lnot a \vee \lnot c)$. Below, the steps using this $\Gamma$.

  • function beame_pitassi
  • $proved := false$
  • $s:= 1$
  • while $s \leq 3$ and $\lnot proved$

    • $s = 1$
    • $<false,-> =$ try_strahler($\Gamma$, $1$, $[\,]$)

      • foreach $x \notin [\,]$ and $b \in\{true, false\}$

        • $<false,->=$try_strahler($\Gamma$, $0$, $[a\rightarrow 0]$)
        • $<false,->=$try_strahler($\Gamma$, $0$, $[a\rightarrow 0, b\rightarrow 0]$)
        • $<false,->=$try_strahler($\Gamma$, $0$, $[a\rightarrow 0, b\rightarrow 0, c\rightarrow 0]$)
    • $s = 2$

    • $<true,cut(b,t_1?,t_2?)> =$ try_strahler($\Gamma$, $2$, $[\,]$)

      • foreach $x \notin [\,]$ and $b \in\{true, false\}$

        • $<false,->=$try_strahler($\Gamma$, $1$, $[a\rightarrow 0]$)
        • $<true,hypothesis((a+b))>=$try_strahler($\Gamma$, $1$, $[a\rightarrow 0, b\rightarrow 0]$)
    • $s:=s+1$

I know that the steps of my example could be hard but these say that the algorithm stops when happens the next assignment $[a\rightarrow 0, b\rightarrow 0]$ for $\Gamma$. Specifically, when $[a\rightarrow 0, b\rightarrow 0]$ falsifies the clause $(a\vee b)$ of $\Gamma$.

For me the output of this example is

$\langle$ unsat, cut(hypothesis($a\vee b$), hypothesis($a\vee\neg b$))$\rangle$.

In other words two clauses ,$(\lnot a \vee c)$ and $(\lnot a \vee \lnot c)$, of $\Gamma$ are losses in the proof, please Is correct the steps that I make in that example? and Could you help to understand why these clauses are losses?

  • 2
    $\begingroup$ This is already your fifth question on this paper. You can't expect us to guide you step-by-step in understanding the paper. Make some effort yourself. A good starting point would be getting a thorough background in the area, say by reading lecture notes. $\endgroup$ – Yuval Filmus Oct 15 '15 at 20:03
  • $\begingroup$ @YuvalFilmus I'm reading background area for one week and still I have this question. $\endgroup$ – juaninf Oct 22 '15 at 1:46
  • 1
    $\begingroup$ LaTeX hint: \langle ... \rangle. $\endgroup$ – Raphael Dec 12 '15 at 10:19
  • 1
    $\begingroup$ Please don't write "stuff EDIT: more stuff". Instead, edit the question to be what it should have been from the start, and to read as a single cohesive whole for someone who encounters it for the first time. You don't need to mark edits by adding "EDIT" -- we have revision history for that. Thank you. $\endgroup$ – D.W. Jan 20 '16 at 5:21
  • 1
    $\begingroup$ I'm confused by the not very descriptive title. Can you formulate a question in English? $\endgroup$ – Raphael Jan 20 '16 at 11:01

Your Answer

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

Browse other questions tagged or ask your own question.