code: def solve(self):
          
  
          is_sat = False
  
          while self.oracle.solve():
              is_sat = True
              self.model = self.oracle.get_model()
              self.cost = self._get_model_cost(self.formula, self.model)
              if self.verbose:
                  print('o {0}'.format(self.cost))
                  sys.stdout.flush()
              if self.cost == 0:      # if cost is 0, then model is an optimum solution
                  break
              self._assert_lt(self.cost)
              self.oracle.set_phases(self.model)  # solution-based phase saving
  
          if is_sat:
              self.model = filter(lambda l: abs(l) <= self.formula.nv, self.model)
              if self.verbose:
                  print('s OPTIMUM FOUND')
          elif self.verbose:
              print('s UNSATISFIABLE')
  
          return is_sat
docs: Computes a solution to the MaxSAT problem. The method implements
              the LSU/LSUS algorithm, i.e. it represents a loop, each iteration
              of which calls a SAT oracle on the working MaxSAT formula and
              refines the upper bound on the MaxSAT cost until the formula
              becomes unsatisfiable.
  
              Returns ``True`` if the hard part of the MaxSAT formula is
              satisfiable, i.e. if there is a MaxSAT solution, and ``False``
              otherwise.
  
              :rtype: bool