Given a set of logical sentences together with nonnegative weights assigned to each of them, the Maximum Weight Satisfiability problem (MAX-WEIGHT SAT) consists in assigning a truth value to the literals of the sentences which maximizes the sum of weights of the satisfied (or true) sentences. In this paper, we explore how to solve this problem using the Variable Neighborhood Search (VNS) metaheuristic. We consider the DIMACS challenge test problems (with weights added) but also much larger instances, with far apart mountains. In order to study the geometry of local optima, a new tool called mountain profiles, is introduced. Moreover, exploiting insights it provides, a generalization of the basic VNS scheme, called Skewed VNS (SVNS), is proposed (together with other variants) and proves to be very efficient in solving large instances. Comparisons are made with a Greedy Randomized Search Procedure (GRASP) and a Tabu Search heuristic. For the larger test problems, which contain up to 7200 clauses and 800 variables, SVNS outperforms the other heuristics with respect to the quality of the solutions obtained.
Published November 2000 , 30 pages
G0062.ps (700 KB)