An Efficient Global-Search Strategy in Discrete Lagrangian Methods for Solving Hard Satisfiability Problems

Knowledge Representation and Reasoning

Volume

Proceedings of the AAAI Conference on Artificial Intelligence, 17

Boolean Satisfiability

In this paper, we present an efficient global search strategy in a search based on the theory of discrete Lagrange multipliers to solve difficult SAT problems. Although a basic discrete Lagrangian method (DLM) can solve most of the satisfiable DIMACS SAT benchmarks efficiently, a few of the large benchmarks have eluded solutions by any local-search methods today. These difficult benchmarks generally have many traps or deep valleys that attract local-search trajectories. In contrast to the implicit trap-escaping strategies, we use an explict global search strategy that can force a search leave traps more efficiently by adding penalty related to Hamming distance between the current search point and past points in the search trajectory. This new global search strategy significantly improves over other results.