The (unweighted) Maximum Satisfiability problem (MaxSat) is: given a boolean formula in conjunctive normal form, find a truth assignment that satisfies the most number of clauses. This paper describes exact algorithms that provide new upper bounds for MaxSat.