docs: def compute(self):
          """
              Compute and return one solution. This method checks whether the
              hard part of the formula is satisfiable, i.e. an MCS can be
              extracted. If the formula is satisfiable, the model computed by the
              SAT call is used as an *over-approximation* of the MCS in the
              method :func:`_compute` invoked here, which implements the BLS
              algorithm augmented with CLD oracle calls.
  
              An MCS is reported as a list of integers, each representing a soft
              clause index (the smallest index is ``1``).
  
              :rtype: list(int)
          """
  
          self.setd = []
          self.solution = None
          self.bb_assumps = []  # backbone assumptions
          self.ss_assumps = []  # satisfied soft clause assumptions
  
          if self.oracle.solve():
              # hard part is satisfiable => there is a solution
              self._overapprox()
              self._compute()
  
              self.solution = [self.smap[-l] for l in self.bb_assumps]
  
          return self.solution