Trap Escaping Strategies in Discrete Lagrangian Methods for Solving Hard Satisfiability and Maximum Satisfiability Problems

Proceedings of the AAAI Conference on Artificial Intelligence, 16

Volume

Proceedings of the AAAI Conference on Artificial Intelligence, 16

Satisfiability

In this paper, we present an improved local-search method based on discrete Lagrange multipliers for solving difficult SAT problems. Although a basic discrete Lagrangian method (DLM) can solve most of the DIMACS SAT benchmarks efficiently, a few of the large SAT benchmarks have eluded solutions by any local-search methods today. Thesedifficult benchmarks generally have many traps that attract local-search trajectories. To this end, we propose to identify their existence when any change to a variable will cause the resulting Lagrangian value to increase. Using the hanoi4 and par-16-1 benchmarks, we illustrate that some unsatisfied clauses are trapped more often than others. Since it is too difficult to remember explicitly all the traps encountered during a search, we propose a new strategy to remember these traps implicitly by giving larger increases to Lagrange multipliers of unsatisfied clauses that are trapped more often. We illustrate the benefit of this new update strategy by solving some of most difficult SAT benchmarks in the DIMACS archive (hanoi4, hanoi4-simple, par16-1 to par16-5, f2000, and par32-1-c).