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 LBX
              algorithm.
  
              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.satc = [False for cl in self.soft]  # satisfied clauses
          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._filter_satisfied(update_setd=True)
              self._compute()
  
              self.solution = list(map(lambda i: i + 1, filter(lambda i: not self.satc[i], range(len(self.soft)))))
  
          return self.solution