Clarification on "clause learning" in DPLL algorithm
All the literals in a conflict clause are set false by definition, else there would be no conflict.  So if the clause $\overline{b_1}\lor\overline{b_2}$ existed, one of those false literals would have caused that clause to go unit before we reached the current level, which in turn would have forced one of the $\overline{b_1}$ or $\overline{b_2}$ literals true.  But we already know that those literals must be false, so we have a contradiction.  This contradiction shows that the clause $\overline{b_1}\lor\overline{b_2}$ cannot exist.  The reasoning is the same for all clauses that are subsets of the conflict clause.