# Step by step of a modification of the Beame-Pitassi Algorithm

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.

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?

• 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. – Yuval Filmus Oct 15 '15 at 20:03
• @YuvalFilmus I'm reading background area for one week and still I have this question. – juaninf Oct 22 '15 at 1:46
• LaTeX hint: \langle ... \rangle. – Raphael Dec 12 '15 at 10:19
• 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. – D.W. Jan 20 '16 at 5:21
• I'm confused by the not very descriptive title. Can you formulate a question in English? – Raphael Jan 20 '16 at 11:01