A New Population-Based Method for Satisfiability Problems

Abstract

. This paper presents the mask method (MASK), a new population-based, evolutionary search procedure for finding models for satisfiability problems (SAT). In this method, a partial truth assignment for a given boolean expression containing N variables is represented by a partially instantiated 0/1 string with N positions (called mask), with each position coding one variable. The mask method begins with a population of masks. An iteration process follows to evaluate each mask in the population using an evaluation mechanism, then to discard half of them, and finally to divide each remaining mask into two new ones by fixing a free position in the mask to 0 and 1 respectively. This process continues until all the positions in the mask have a fixed value. The method is compared with a class of genetic algorithms (GAs) on a set of SAT instances and proves to be much more efficient. 1 INTRODUCTION The satisfiability problem or SAT [5] is of great importance in Artificial Intelligence both in...