Satisfiability problem - SAT

Problem Definition

The satisfiability problem (SAT) has received many attention by the scientific community since any NP problem can be translated into an equivalent SAT problem in polynomial time (Cooke theorem) [Cook71]; while the inverse transformation may not always exists in polynomial time. The SAT problem was the first which was demonstrated to belong to the NP class of problems.

The SAT problem consists in assigning values to a set of n boolean variables such that they
satisfy a given set of clauses , where is a disjunction of literals, and a literal is a variable or its negation. Hence, we can define SAT as a function , like:

An instance of SAT, , is called satisfiable if , and unsatisfiable otherwise. A k-SAT instance is composed of clauses with length k, and when the problem is NP-complete [Garey79].

The Algorithm

Folino et al. developed in [FPS01] a parallel method for solving the SAT problem. They used a cellular genetic algorithm hybridized with local search, called CGWSAT. WSAT [BKC94] is an extension of GSAT [SLM92] that combines a random walk strategy with greedy local search.

The basic GSAT algorithm starts with a randomly generated truth assignment. It then changes (flips) the assignment of the variable that leads to the largest decrease in the total number of unsatisfied clauses. Such flips are repeated until either a satisfying assignment is found or a preset of maximum number of flips (Maxflips) is reached. This process is repeated as needed up to a maximum of Maxtries times.

WSAT differs from GSAT in the selection of the variable to flip. It restricts the choice of a randomly flipped variable to the set of variables that appear in unsatisfied clauses.

CGWSAT is a parallel implementation of a cGA which has been realized using the parallel computation environment provided by the CAMEL system [CGRS95]. CAMEL is an interactive parallel environment based on cellular automata model that allows to develop and execute cellular programs in parallel machines.

Results

The authors solved the problem in a Meiko CS-2 parallel machine running the Solaris OS. CGWSAT has been tested on hard randomly generated 3-SAT problems, and the results were compared to those of WSAT and PWSAT (a parallel implementation of WSAT). Tests with 256 to 2048 variables were been considered and on some problems of the DIMACS [JT96] test suite and the SATLIB library. The results of Table 1 were obtained with a population size of 320, a probability between 0.01 and 0.5 for crossover, depending on the difficulty ofthe problem, and between 0.9 and 1.0 for mutation and a length approximately equal to 10% the number of variables for two-point crossover.

Table 1. Results of Folino et al. for hard random 3-SAT problems, DIMACS, and SATLIB test suite