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...
Main Authors: | , , , |
---|---|
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 |