code: private void minimisationWithBinaryResolution(final LNGIntVector outLearnt) {
      long lbd = computeLBD(outLearnt, -1);
      int p = not(outLearnt.get(0));
      if (lbd <= lbLBDMinimizingClause) {
        myflag++;
        for (int i = 1; i < outLearnt.size(); i++)
          permDiff.set(var(outLearnt.get(i)), myflag);
        int nb = 0;
        for (final MSWatcher wbin : watchesBin.get(p)) {
          int imp = wbin.blocker();
          if (permDiff.get(var(imp)) == myflag && value(imp) == Tristate.TRUE) {
            nb++;
            permDiff.set(var(imp), myflag - 1);
          }
        }
        int l = outLearnt.size() - 1;
        if (nb > 0) {
          for (int i = 1; i < outLearnt.size() - nb; i++) {
            if (permDiff.get(var(outLearnt.get(i))) != myflag) {
              p = outLearnt.get(l);
              outLearnt.set(l, outLearnt.get(i));
              outLearnt.set(i, p);
              l--;
              i--;
            }
          }
          outLearnt.removeElements(nb);
        }
      }
    }
docs: A special clause minimization by binary resolution for small clauses.
  @param outLearnt the vector where the new learnt 1-UIP clause is stored