Tabu-Sat and Walksat for Level Graph Formulas

Porschen, Stefan and Speckenmeyer, Ewald and Randerath, Bert and Gärtner, Mattias (2004) Tabu-Sat and Walksat for Level Graph Formulas.
Technical Report , 20 p.


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.

Download: [img] Postscript
Download (1MB) | Preview
Editorial actions: View Item View Item (Login required)
Deposit Information:
ZAIK Number: zaik2004-476
Depositing User: Stefan Porschen
Date Deposited: 01 Mar 2005 00:00
Last Modified: 12 Jan 2012 10:56