code: def _compute(self):
          
  
          # unless clause D checks are used, test one literal at a time
          # and add it either to satisfied of backbone assumptions
          i = 0
          while i < len(self.setd):
              if self.ucld:
                  self.do_cld_check(self.setd[i:])
                  i = 0
  
              if self.setd:  # if may be empty after the clause D check
                  if self.oracle.solve(assumptions=self.ss_assumps + self.bb_assumps + [self.setd[i]]):
                      # filtering satisfied clauses
                      self._filter_satisfied()
                  else:
                      # current literal is backbone
                      self.bb_assumps.append(-self.setd[i])
  
              i += 1
docs: The main method of the class, which computes an MCS given its
              over-approximation. The over-approximation is defined by a model
              for the hard part of the formula obtained in :func:`compute`.
  
              The method is essentially a simple loop going over all literals
              unsatisfied by the previous model, i.e. the literals of
              ``self.setd`` and checking which literals can be satisfied. This
              process can be seen a refinement of the over-approximation of the
              MCS. The algorithm follows the pseudo-code of the LBX algorithm
              presented in [1]_.
  
              Additionally, if :class:`LBX` was constructed with the requirement
              to make "clause :math:`D`" calls, the method calls
              :func:`do_cld_check` at every iteration of the loop using the
              literals of ``self.setd`` not yet checked, as the contents of
              "clause :math:`D`".