docs: def do_cld_check(self, cld):
          """
              Do the "clause :math:`D`" check. This method receives a list of
              literals, which serves a "clause :math:`D`" [1]_, and checks
              whether the formula conjoined with :math:`D` is satisfiable.
  
              If clause :math:`D` cannot be satisfied together with the formula,
              then negations of all of its literals are backbones of the formula
              and the MCSls algorithm can stop. Otherwise, the literals satisfied
              by the new model refine the MCS further.
  
              Every time the method is called, a new fresh selector variable
              :math:`s` is introduced, which augments the current clause
              :math:`D`. The SAT oracle then checks if clause :math:`(D \\vee
              \\neg{s})` can be satisfied together with the internal formula.
              The :math:`D` clause is then disabled by adding a hard clause
              :math:`(\\neg{s})`.
  
              :param cld: clause :math:`D` to check
              :type cld: list(int)
          """
  
          # adding a selector literal to clause D
          # selector literals for clauses D currently
          # cannot be reused, but this may change later
          self.topv += 1
          sel = self.topv
          cld.append(-sel)
  
          # adding clause D
          self.oracle.add_clause(cld)
          self.ss_assumps.append(sel)
  
          self.setd = []
          self.oracle.solve(assumptions=self.ss_assumps + self.bb_assumps)
  
          self.ss_assumps.pop()  # removing clause D assumption
          if self.oracle.get_status() == True:
              model = self.oracle.get_model()
  
              for l in cld[:-1]:
                  # filtering all satisfied literals
                  if model[abs(l) - 1] > 0:
                      self.ss_assumps.append(l)
                  else:
                      self.setd.append(l)
          else:
              # clause D is unsatisfiable => all literals are backbones
              self.bb_assumps.extend([-l for l in cld[:-1]])
  
          # deactivating clause D
          self.oracle.add_clause([-sel])