code: private void backward(final CLClause c, final int ignore) {
          int minlit = 0;
          int minoccs = Integer.MAX_VALUE;
          int litoccs;
          this.stats.steps++;
          for (int i = 0; i < c.lits().size(); i++) {
              final int lit = c.lits().get(i);
              if (lit == ignore) { continue; }
              if (val(lit) < 0) { continue; }
              litoccs = occs(lit).count();
              if (minlit != 0 && minoccs >= litoccs) { continue; }
              minlit = lit;
              minoccs = litoccs;
          }
          if (minoccs >= this.config.bwocclim) { return; }
          assert minlit != 0;
          for (int i = 0; i < c.lits().size(); i++) { mark(c.lits().get(i)); }
          final CLOccs os = occs(minlit);
          for (final CLClause d : os) {
              if (d == c) { continue; }
              int lit;
              int count = this.seen.size();
              int negated = 0;
              this.stats.steps++;
              for (int p = 0; count != 0 && p < d.lits().size(); p++) {
                  lit = d.lits().get(p);
                  final int m = marked(lit);
                  if (m == 0) { continue; }
                  assert count > 0;
                  count--;
                  if (m > 0) { continue; }
                  assert m < 0;
                  if (negated != 0) {
                      count = Integer.MAX_VALUE;
                      break;
                  }
                  negated = lit;
              }
              if (count != 0) { continue; }
              if (negated != 0) {
                  this.tostrengthen.push(new Pair<>(d, negated));
                  this.stats.backwardStrengthened++;
              } else {
                  this.stats.backwardSubsumed++;
                  dumpClause(d);
              }
          }
          unmark();
      }
docs: Backward subsumes from clause.
  @param c      the clause
  @param ignore the literal to ignore