"Tabu-Sat and Walksat for Level Graph Formulas"
Technical report by Stefan Porschen, Ewald Speckenmeyer, Bert Randerath, Mattias Gärtner, available as BibTeX Source, postscript file and compressed postscript file.
Zentrum für Angewandte Informatik Köln, Lehrstuhl Speckenmeyer
Preprint Key:	zaik2004-476
Keywords:	level graph formula, propositional satisfiability, stochastic local search algorithm
MSC codes:	03B05, 68Q25
This technical report has 20 pages, was written in October 2004, it has not been published.
Abstract:	This paper provides an empirical study of stochastic local search procedures for solving the MAXSAT problem on propositional formulas. Concretely, we first compare Walksat and (variants of) Tabu-Sat for MAX2SAT and MAX3SAT on arbitrary random CNF formulas. Second, we compare conveniently adapted versions of these procedures on level graph formulas encoding the arc crossing minimization problem for randomly generated level graphs. The Tabu-Sat procedure introduced here, dynamically modifies the tabulength parameter when a cycle in the search space is detected. Another variant called Vector-Tabu-Sat manages a tabulength parameter for every Boolean variable independently. Several numerical experiments indicate that our variants of Tabu-Sat are superior to Walksat when the number of clauses increases.