Salvato in:
Dettagli Bibliografici
Autori principali: Zhang, Jialu, Li, Chu-Min, Cherif, Sami, Li, Shuolin, Zheng, Zhifei
Natura: Preprint
Pubblicazione: 2025
Soggetti:
Accesso online:https://arxiv.org/abs/2506.06216
Tags: Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
_version_ 1866914279004831744
author Zhang, Jialu
Li, Chu-Min
Cherif, Sami
Li, Shuolin
Zheng, Zhifei
author_facet Zhang, Jialu
Li, Chu-Min
Cherif, Sami
Li, Shuolin
Zheng, Zhifei
contents The Maximum Satisfiability problem (MaxSAT) is a major optimization challenge with numerous practical applications. In recent MaxSAT evaluations, most MaxSAT solvers have incorporated an Integer Linear Programming (ILP) solver into their portfolios. However, a good portfolio strategy requires a lot of tuning work and is limited to the profiling benchmark. This paper proposes a methodology to fully integrate ILP preprocessing techniques into the MaxSAT solving pipeline and investigates the impact on the top-performing MaxSAT solvers. Experimental results show that our approach helps to improve 5 out of 6 state-of-the-art MaxSAT solvers, especially for WMaxCDCL-OpenWbo1200, the winner of the MaxSAT evaluation 2024 on the unweighted track, which is able to solve 15 additional instances using our methodology.
format Preprint
id arxiv_https___arxiv_org_abs_2506_06216
institution arXiv
publishDate 2025
record_format arxiv
spellingShingle Integer Linear Programming Preprocessing for Maximum Satisfiability
Zhang, Jialu
Li, Chu-Min
Cherif, Sami
Li, Shuolin
Zheng, Zhifei
Artificial Intelligence
The Maximum Satisfiability problem (MaxSAT) is a major optimization challenge with numerous practical applications. In recent MaxSAT evaluations, most MaxSAT solvers have incorporated an Integer Linear Programming (ILP) solver into their portfolios. However, a good portfolio strategy requires a lot of tuning work and is limited to the profiling benchmark. This paper proposes a methodology to fully integrate ILP preprocessing techniques into the MaxSAT solving pipeline and investigates the impact on the top-performing MaxSAT solvers. Experimental results show that our approach helps to improve 5 out of 6 state-of-the-art MaxSAT solvers, especially for WMaxCDCL-OpenWbo1200, the winner of the MaxSAT evaluation 2024 on the unweighted track, which is able to solve 15 additional instances using our methodology.
title Integer Linear Programming Preprocessing for Maximum Satisfiability
topic Artificial Intelligence
url https://arxiv.org/abs/2506.06216