Initial Solution Generation and Diversified Variable Picking in Local Search for (Weighted) Partial MaxSAT
The (weighted) partial maximum satisfiability ((W)PMS) problem is an important generalization of the classic problem of propositional (Boolean) satisfiability with a wide range of real-world applications. In this paper, we propose an initialization and a diversification strategy to improve local sea...
Main Authors: | , , , , |
---|---|
Format: | Article |
Language: | English |
Published: |
MDPI AG
2022-12-01
|
Series: | Entropy |
Subjects: | |
Online Access: | https://www.mdpi.com/1099-4300/24/12/1846 |
_version_ | 1827639821943701504 |
---|---|
author | Zaijun Zhang Jincheng Zhou Xiaoxia Wang Heng Yang Yi Fan |
author_facet | Zaijun Zhang Jincheng Zhou Xiaoxia Wang Heng Yang Yi Fan |
author_sort | Zaijun Zhang |
collection | DOAJ |
description | The (weighted) partial maximum satisfiability ((W)PMS) problem is an important generalization of the classic problem of propositional (Boolean) satisfiability with a wide range of real-world applications. In this paper, we propose an initialization and a diversification strategy to improve local search for the (W)PMS problem. Our initialization strategy is based on a novel definition of variables’ structural entropy, and it aims to generate a solution that is close to a high-quality feasible one. Then, our diversification strategy picks a variable in two possible ways, depending on a parameter: continuing to pick variables with the best benefits or focusing on a clause with the greatest penalty and then selecting variables probabilistically. Based on these strategies, we developed a local search solver dubbed <inline-formula><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline"><semantics><mi mathvariant="italic">ImSATLike</mi></semantics></math></inline-formula>, as well as a hybrid solver <inline-formula><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline"><semantics><mrow><mi mathvariant="italic">ImSATLike-TT</mi></mrow></semantics></math></inline-formula>, and experimental results on (weighted) partial MaxSAT instances in recent MaxSAT Evaluations show that they outperform or have nearly the same performances as state-of-the-art local search and hybrid competitors, respectively, in general. Furthermore, we carried out experiments to confirm the individual impacts of each proposed strategy. |
first_indexed | 2024-03-09T16:48:28Z |
format | Article |
id | doaj.art-fd907b93e8cd4112b5beaf211b34d1d2 |
institution | Directory Open Access Journal |
issn | 1099-4300 |
language | English |
last_indexed | 2024-03-09T16:48:28Z |
publishDate | 2022-12-01 |
publisher | MDPI AG |
record_format | Article |
series | Entropy |
spelling | doaj.art-fd907b93e8cd4112b5beaf211b34d1d22023-11-24T14:44:04ZengMDPI AGEntropy1099-43002022-12-012412184610.3390/e24121846Initial Solution Generation and Diversified Variable Picking in Local Search for (Weighted) Partial MaxSATZaijun Zhang0Jincheng Zhou1Xiaoxia Wang2Heng Yang3Yi Fan4School of Mathematics and Statistics, Qiannan Normal University for Nationalities, Duyun 558000, ChinaKey Laboratory of Complex Systems and Intelligent Optimization of Guizhou Province, Duyun 558000, ChinaSchool of Mathematics and Statistics, Qiannan Normal University for Nationalities, Duyun 558000, ChinaSchool of Mathematics and Statistics, Qiannan Normal University for Nationalities, Duyun 558000, ChinaSchool of Mathematics and Statistics, Qiannan Normal University for Nationalities, Duyun 558000, ChinaThe (weighted) partial maximum satisfiability ((W)PMS) problem is an important generalization of the classic problem of propositional (Boolean) satisfiability with a wide range of real-world applications. In this paper, we propose an initialization and a diversification strategy to improve local search for the (W)PMS problem. Our initialization strategy is based on a novel definition of variables’ structural entropy, and it aims to generate a solution that is close to a high-quality feasible one. Then, our diversification strategy picks a variable in two possible ways, depending on a parameter: continuing to pick variables with the best benefits or focusing on a clause with the greatest penalty and then selecting variables probabilistically. Based on these strategies, we developed a local search solver dubbed <inline-formula><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline"><semantics><mi mathvariant="italic">ImSATLike</mi></semantics></math></inline-formula>, as well as a hybrid solver <inline-formula><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline"><semantics><mrow><mi mathvariant="italic">ImSATLike-TT</mi></mrow></semantics></math></inline-formula>, and experimental results on (weighted) partial MaxSAT instances in recent MaxSAT Evaluations show that they outperform or have nearly the same performances as state-of-the-art local search and hybrid competitors, respectively, in general. Furthermore, we carried out experiments to confirm the individual impacts of each proposed strategy.https://www.mdpi.com/1099-4300/24/12/1846maximum satisfiabilitystructural entropylocal searchheuristic search |
spellingShingle | Zaijun Zhang Jincheng Zhou Xiaoxia Wang Heng Yang Yi Fan Initial Solution Generation and Diversified Variable Picking in Local Search for (Weighted) Partial MaxSAT Entropy maximum satisfiability structural entropy local search heuristic search |
title | Initial Solution Generation and Diversified Variable Picking in Local Search for (Weighted) Partial MaxSAT |
title_full | Initial Solution Generation and Diversified Variable Picking in Local Search for (Weighted) Partial MaxSAT |
title_fullStr | Initial Solution Generation and Diversified Variable Picking in Local Search for (Weighted) Partial MaxSAT |
title_full_unstemmed | Initial Solution Generation and Diversified Variable Picking in Local Search for (Weighted) Partial MaxSAT |
title_short | Initial Solution Generation and Diversified Variable Picking in Local Search for (Weighted) Partial MaxSAT |
title_sort | initial solution generation and diversified variable picking in local search for weighted partial maxsat |
topic | maximum satisfiability structural entropy local search heuristic search |
url | https://www.mdpi.com/1099-4300/24/12/1846 |
work_keys_str_mv | AT zaijunzhang initialsolutiongenerationanddiversifiedvariablepickinginlocalsearchforweightedpartialmaxsat AT jinchengzhou initialsolutiongenerationanddiversifiedvariablepickinginlocalsearchforweightedpartialmaxsat AT xiaoxiawang initialsolutiongenerationanddiversifiedvariablepickinginlocalsearchforweightedpartialmaxsat AT hengyang initialsolutiongenerationanddiversifiedvariablepickinginlocalsearchforweightedpartialmaxsat AT yifan initialsolutiongenerationanddiversifiedvariablepickinginlocalsearchforweightedpartialmaxsat |