MAX-SAT Problem using Hybrid Harmony Search Algorithm

被引:5
作者
Abu Doush, Iyad [1 ,2 ]
Quran, Amal Lutfi [1 ]
Al-Betar, Mohammed Azmi [3 ]
Awadallah, Mohammed A. [4 ]
机构
[1] Yarmouk Univ, Comp Sci Dept, Irbid, Jordan
[2] Amer Univ Kuwait, Dept Comp Sci & Informat Syst, Salmiya, Kuwait
[3] Al Balqa Appl Univ, Al Huson Univ Coll, Dept Informat Technol, POB 50, Irbid, Jordan
[4] Al Aqsa Univ, Dept Comp Sci, POB 4051, Gaza, Palestine
关键词
Maximum satisfiability problem; harmony search; local search; optimization; 3SAT problem; evolutionary algorithms; MAX-SAT problem; metaheuristic;
D O I
10.1515/jisys-2016-0129
中图分类号
TP18 [人工智能理论];
学科分类号
081104 ; 0812 ; 0835 ; 1405 ;
摘要
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.
引用
收藏
页码:643 / 658
页数:16
相关论文
共 58 条
[31]  
Kroc L, 2009, 21ST INTERNATIONAL JOINT CONFERENCE ON ARTIFICIAL INTELLIGENCE (IJCAI-09), PROCEEDINGS, P544
[32]   GASAT: A genetic local search algorithm for the satisfiability problem [J].
Lardeux, Frederic ;
Saubion, Frederic ;
Hao, Jin-Kao .
EVOLUTIONARY COMPUTATION, 2006, 14 (02) :223-253
[33]  
Layeb Abdesslem, 2012, Journal of Advances in Information Technology, V3, P138, DOI 10.4304/jait.3.2.138-146
[34]  
Layeb A., 2011, 12 INT AR C INF TECH, P175
[35]  
Layeb A, 2008, LECT NOTES ARTIF INT, V5271, P172, DOI 10.1007/978-3-540-87656-4_22
[36]  
Layeb A, 2010, LECT NOTES ARTIF INT, V6097, P136, DOI 10.1007/978-3-642-13025-0_15
[37]   A new structural optimization method based on the harmony search algorithm [J].
Lee, KS ;
Geem, ZW .
COMPUTERS & STRUCTURES, 2004, 82 (9-10) :781-798
[38]  
Li CM, 2005, LECT NOTES COMPUT SC, V3709, P403
[39]  
Marchiori E, 1999, GECCO-99: PROCEEDINGS OF THE GENETIC AND EVOLUTIONARY COMPUTATION CONFERENCE, P393
[40]   Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL [J].
Maric, Filip .
THEORETICAL COMPUTER SCIENCE, 2010, 411 (50) :4333-4356