# k-SAT Landscape Analysis

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.