docs: def compute(self):
          """
              Compute a MaxSAT solution. First, the method checks whether or
              not the set of hard clauses is satisfiable. If not, the method
              returns ``False``. Otherwise, add soft clauses to the oracle and
              call the MaxSAT algorithm (see :func:`_compute`).
  
              Note that the soft clauses are added to the oracles after being
              augmented with additional *selector* literals. The selectors
              literals are then used as *assumptions* when calling the SAT oracle
              and are needed for extracting unsatisfiable cores.
          """
  
          if self.oracle.solve():
              # hard part is satisfiable
              # create selectors and a mapping from selectors to clause ids
              self.sels, self.vmap = [], {}
              self.scpy = [True for cl in self.soft]
  
              # adding soft clauses to oracle
              for i in range(len(self.soft)):
                  self.topv += 1
  
                  self.soft[i].append(-self.topv)
                  self.sels.append(self.topv)
                  self.oracle.add_clause(self.soft[i])
  
                  self.vmap[self.topv] = i
  
              self._compute()
              return True
          else:
              return False