MAX-SAT Problem using Hybrid Harmony Search Algorithm

Maximum Satisfiability problem is an optimization variant of the Satisfiability problem (SAT) denoted as MAX-SAT. The aim of this problem is to find Boolean variable assignment that maximizes the number of satisfied clauses in the Boolean formula. In case the number of variables per clause is equal...

Full description

Bibliographic Details
Main Authors: Abu Doush Iyad, Quran Amal Lutfi, Al-Betar Mohammed Azmi, Awadallah Mohammed A.
Format: Article
Language:English
Published: De Gruyter 2018-10-01
Series:Journal of Intelligent Systems
Subjects:
Online Access:https://doi.org/10.1515/jisys-2016-0129
_version_ 1819007281616912384
author Abu Doush Iyad
Quran Amal Lutfi
Al-Betar Mohammed Azmi
Awadallah Mohammed A.
author_facet Abu Doush Iyad
Quran Amal Lutfi
Al-Betar Mohammed Azmi
Awadallah Mohammed A.
author_sort Abu Doush Iyad
collection DOAJ
description Maximum Satisfiability problem is an optimization variant of the Satisfiability problem (SAT) denoted as MAX-SAT. The aim of this problem is to find Boolean variable assignment that maximizes the number of satisfied clauses in the Boolean formula. In case the number of variables per clause is equal or greater than three, then this problem is considered NP-complete. Hence, many researchers have developed techniques to deal with MAX-SAT. In this paper, we investigate the impact of different hybrid versions of binary harmony search (HS) algorithm on solving MAX 3-SAT problem. Therefore, we propose two novel hybrid binary HS algorithms. The first hybridizes Flip heuristic with HS, and the second uses Tabu search combined with Flip heuristic. Furthermore, a distinguished feature of our proposed approaches is using an objective function that is updated dynamically based on the stepwise adaptation of weights (SAW) mechanism to evaluate the MAX-SAT solution using the proposed hybrid versions. The performance of the proposed approaches is evaluated over standard MAX-SAT benchmarks, and the results are compared with six evolutionary algorithms and three stochastic local search algorithms. The obtained results are competitive and show that the proposed novel approaches are effective.
first_indexed 2024-12-21T00:22:05Z
format Article
id doaj.art-f5165b87acc8457fb0e037462516ffae
institution Directory Open Access Journal
issn 0334-1860
2191-026X
language English
last_indexed 2024-12-21T00:22:05Z
publishDate 2018-10-01
publisher De Gruyter
record_format Article
series Journal of Intelligent Systems
spelling doaj.art-f5165b87acc8457fb0e037462516ffae2022-12-21T19:22:04ZengDe GruyterJournal of Intelligent Systems0334-18602191-026X2018-10-0127464365810.1515/jisys-2016-0129MAX-SAT Problem using Hybrid Harmony Search AlgorithmAbu Doush Iyad0Quran Amal Lutfi1Al-Betar Mohammed Azmi2Awadallah Mohammed A.3Computer Science Department, Yarmouk University, Irbid, JordanComputer Science Department, Yarmouk University, Irbid, JordanDepartment of Information Technology, Al-Huson University College, Al-Balqa Applied University, P.O. Box 50, Al-Huson, Irbid, JordanDepartment of Computer Science, Al-Aqsa University, P. O. Box 4051, Gaza, PalestineMaximum Satisfiability problem is an optimization variant of the Satisfiability problem (SAT) denoted as MAX-SAT. The aim of this problem is to find Boolean variable assignment that maximizes the number of satisfied clauses in the Boolean formula. In case the number of variables per clause is equal or greater than three, then this problem is considered NP-complete. Hence, many researchers have developed techniques to deal with MAX-SAT. In this paper, we investigate the impact of different hybrid versions of binary harmony search (HS) algorithm on solving MAX 3-SAT problem. Therefore, we propose two novel hybrid binary HS algorithms. The first hybridizes Flip heuristic with HS, and the second uses Tabu search combined with Flip heuristic. Furthermore, a distinguished feature of our proposed approaches is using an objective function that is updated dynamically based on the stepwise adaptation of weights (SAW) mechanism to evaluate the MAX-SAT solution using the proposed hybrid versions. The performance of the proposed approaches is evaluated over standard MAX-SAT benchmarks, and the results are compared with six evolutionary algorithms and three stochastic local search algorithms. The obtained results are competitive and show that the proposed novel approaches are effective.https://doi.org/10.1515/jisys-2016-0129maximum satisfiability problemharmony searchlocal searchoptimization3sat problemevolutionary algorithmsmax-sat problemmetaheuristic
spellingShingle Abu Doush Iyad
Quran Amal Lutfi
Al-Betar Mohammed Azmi
Awadallah Mohammed A.
MAX-SAT Problem using Hybrid Harmony Search Algorithm
Journal of Intelligent Systems
maximum satisfiability problem
harmony search
local search
optimization
3sat problem
evolutionary algorithms
max-sat problem
metaheuristic
title MAX-SAT Problem using Hybrid Harmony Search Algorithm
title_full MAX-SAT Problem using Hybrid Harmony Search Algorithm
title_fullStr MAX-SAT Problem using Hybrid Harmony Search Algorithm
title_full_unstemmed MAX-SAT Problem using Hybrid Harmony Search Algorithm
title_short MAX-SAT Problem using Hybrid Harmony Search Algorithm
title_sort max sat problem using hybrid harmony search algorithm
topic maximum satisfiability problem
harmony search
local search
optimization
3sat problem
evolutionary algorithms
max-sat problem
metaheuristic
url https://doi.org/10.1515/jisys-2016-0129
work_keys_str_mv AT abudoushiyad maxsatproblemusinghybridharmonysearchalgorithm
AT quranamallutfi maxsatproblemusinghybridharmonysearchalgorithm
AT albetarmohammedazmi maxsatproblemusinghybridharmonysearchalgorithm
AT awadallahmohammeda maxsatproblemusinghybridharmonysearchalgorithm