Scatter search for SAT and W-MAX-SAT problems

Author

Habiba, Drias ; Nabila, Azi

Author_Institution

Dept. of Comput. Sci., USTHB, Alger, Algeria

fYear

2001

fDate

36951

Firstpage

105

Lastpage

109

Abstract

SAT, the decision version of the satisfiability problem, which consists in verifying that a conjunction of clauses is satisfied by at least one variables interpretation, has been shown to be the first NP-complete satisfiability problem. In this paper, scatter search is used for the first time to solve the problems SAT and weighted maximum SAT (W-MAX-SAT). We present hereafter this approach and the general algorithm. We describe the issues of the method in the general context and then we propose an implementation for SAT and W-MAX-SAT. A procedure to generate good initial scattered solutions as well as an operator to combine solutions and a classical technique to improve the solutions quality are presented. We compare our empirical results with those obtained by GRASP

Keywords

computability; computational complexity; formal logic; optimisation; search problems; NP-complete satisfiability problem; W-MAX-SAT problems; clause conjunction; decision version; scatter search; scattered solutions; weighted maximum SAT; Algorithm design and analysis; Artificial intelligence; Bridges; Computational complexity; Computer science; Genetic algorithms; Logic; NP-complete problem; Scattering; Simulated annealing;

fLanguage

English

Publisher

ieee

Conference_Titel

System Theory, 2001. Proceedings of the 33rd Southeastern Symposium on

Conference_Location

Athens, OH

Print_ISBN

0-7803-6661-1

Type

conf

DOI

10.1109/SSST.2001.918500

Filename

918500