A Tractable Walsh Analysis of SAT and Its Implications for Genetic Algorithms

Abstract

Walsh Transforms measure all sources of nonlinear interactions for functions that have a bit representation. There can be exponentially many nonlinear interactions and exactly computing all Walsh coefficients is usually intractable for non-trivial functions. In this paper we will show that SAT problems evaluated as MAXSAT functions have a highly restricted set of nonzero Walsh coefficients and those coefficients can be computed in linear time with respect to the number of clauses. This analysis suggests why standard simple genetic algorithms should perform poorly on MAXSAT problems. Introduction Boolean Satisfiability (SAT) was the first problem proven to be NP-Complete. SAT problems consist of literals, defined as variables or negated variables, that are combined together using and () and or (). Typically, SAT problems are presented in conjunctive normal form which groups literals together into disjunctive clauses. A SAT problem is considered solved when an instantiation of variables...