Ant colony optimization with adaptive fitness function for satisfiability testing

Ant Colony Optimization (ACO) is a metaheuristic inspired by the foraging behavior of ant colonies that has been successful in the resolution of hard combinatorial optimization problems. This work proposes MaxMin-SAT, an ACO alternative for the satisfiability problem (SAT). MaxMin-SAT is the first ACO algorithm for SAT that implements an Adaptive Fitness Function, which is a technique used for Genetic Algorithms to escape local optima. To show effectiveness of this technique, three different adaptive fitness functions are compared: Stepwise Adaptation of Weights, Refining Functions, and a mix of the previous two. To experimentally test MaxMin-SAT, a comparison with Walksat (a successful local search algorithm) is presented. Even though MaxMin-SAT cannot beat Walksat when dealing with phase transition instances, experimental results show that it can be competitive with the local search heuristic for overconstrained instances.