Empirical analysis of landscapes created by k-SAT instances to support a mathematical derivation of the number of local maxima and upper bounds. A k-SAT instance is a boolean formula in Conjunctive Normal Form (consisting of ANDs of clauses, clauses are ORs of literals) where each clause has exactly k literals.

A ‘landscape’ is generated by considering all permutations of input values and counting the number of individual clauses that are true: the expression is satisfied if every clause is true.

My role in this project was to create a program to compute the exact number of local maxima for a range of k-SAT instances. These numbers were used in conjunction with the mathematical analysis of Dr. Andreas Albrecht.

Main publication:

  • A.A. Albrecht, P.C.R. Lane and K. Steinhöfel, ‘Analysis of local search landscapes for k-SAT instances,’ Mathematics in Computer Science, 3:465-488, 2010. Web page.