def compute(self):
        """
            This is the main method of the :class:`MUSX` class. It computes a
            set of soft clauses belonging to an MUS of the input formula.
            First, the method checks whether the formula is satisfiable. If it
            is, nothing else is done. Otherwise, an *unsatisfiable core* of the
            formula is extracted, which is later used as an over-approximation
            of an MUS refined in :func:`_compute`.
        """

        # cheking whether or not the formula is unsatisfiable
        if not self.oracle.solve(assumptions=self.sels):
            # get an overapproximation of an MUS
            approx = sorted(self.oracle.get_core())

            if self.verbose:
                print('c MUS approx:', ' '.join([str(self.vmap[sel] + 1) for sel in approx]), '0')

            # iterate over clauses in the approximation and try to delete them
            self._compute(approx)

            # return an MUS
            return list(map(lambda x: self.vmap[x] + 1, approx))