PARTIAL MAX-SAT of Level Graph (Mixed-Horn) Formulas
Ewald Speckenmeyer, Stefan Porschen · 2010
This paper provides an empirical study of stochastic local search procedures for solving the MAXSAT problem on a specific class of mixed Horn formulas [13, 14], namely level graph formulas [15]. 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.