---
title: "Read-Once Resolution for Unsatisfiability-Based Max-SAT Algorithms"
authors:
  - "Federico Heras"
  - "João P. Marques Silva"
doi: "10.5591/978-1-57735-516-8/IJCAI11-103"
url: "https://ijcai.org/proceedings/2011/103"
pdf: "https://ijcai.org/proceedings/2011/0103.pdf"
venue: "Proceedings of the Twenty-Second International Joint Conference on Artificial Intelligence"
year: 2011
pages: "572-576"
track: ""
keywords:
---

# Read-Once Resolution for Unsatisfiability-Based Max-SAT Algorithms

Federico Heras, João P. Marques Silva

*Proceedings of the Twenty-Second International Joint Conference on Artificial Intelligence*, pages 572-576. DOI: [10.5591/978-1-57735-516-8/IJCAI11-103](https://doi.org/10.5591/978-1-57735-516-8/IJCAI11-103)

## Abstract

This paper proposes the integration of the resolution rule for Max-SAT with unsatisfiability-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 subparts of a general proof. Finally, we perform an empirical investigation on structured instances from recent Max-SAT evaluations. Preliminary results show that the use of read-once resolution substantially improves the performance of the solver.