License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.SAT.2023.29
URN: urn:nbn:de:0030-drops-184912
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2023/18491/
Zhou, Junping ;
Liang, Jiaxin ;
Yin, Minghao ;
He, Bo
LS-DTKMS: A Local Search Algorithm for Diversified Top-k MaxSAT Problem
Abstract
The Maximum Satisfiability (MaxSAT), an important optimization problem, has a range of applications, including network routing, planning and scheduling, and combinatorial auctions. Among these applications, one usually benefits from having not just one single solution, but k diverse solutions. Motivated by this, we study an extension of MaxSAT, named Diversified Top-k MaxSAT (DTKMS) problem, which is to find k feasible assignments of a given formula such that each assignment satisfies all hard clauses and all of them together satisfy the maximum number of soft clauses. This paper presents a local search algorithm, LS-DTKMS, for DTKMS problem, which exploits novel scoring functions to select variables and assignments. Experiments demonstrate that LS-DTKMS outperforms the top-k MaxSAT based DTKMS solvers and state-of-the-art solvers for diversified top-k clique problem.
BibTeX - Entry
@InProceedings{zhou_et_al:LIPIcs.SAT.2023.29,
author = {Zhou, Junping and Liang, Jiaxin and Yin, Minghao and He, Bo},
title = {{LS-DTKMS: A Local Search Algorithm for Diversified Top-k MaxSAT Problem}},
booktitle = {26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
pages = {29:1--29:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-286-0},
ISSN = {1868-8969},
year = {2023},
volume = {271},
editor = {Mahajan, Meena and Slivovsky, Friedrich},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2023/18491},
URN = {urn:nbn:de:0030-drops-184912},
doi = {10.4230/LIPIcs.SAT.2023.29},
annote = {Keywords: Top-k, MaxSAT, local search}
}