based Max-SAT solvers. First, we show that the resolution rule for Max-SAT can be safely
applied as dictated by the resolution proof associated with an unsatisfiable core when such
proof is read-once, that is, each clause is used at most once in the resolution process.
Second, we study how this property can be integrated in an unsatisfiability-based solver. In
particular, the resolution rule for Max-SAT is applied to read-once proofs or to read-once …