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...

Full description

Bibliographic Details
Main Authors: Zaijun Zhang, Jincheng Zhou, Xiaoxia Wang, Heng Yang, Yi Fan
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