Discrete Lagrangian-Based Search for Solving MAX-SAT Problems

Abstract

Weighted maximum satisfiability problems (MAX-SAT) are difficult to solve due to the large number of local minima in their search space. In this paper we propose a new discrete Lagrangian based search method (DLM) for solving these problems. Instead of restarting from a new point when the search reaches a local minimum, the Lagrange multipliers in DLM provide a force to lead the search out of the local minimum and move it in a direction provided by the multipliers. Since DLM has very few parameters to be tuned, it can be made deterministic and the results, reproducible. We compare DLM with GRASP in solving a large set of test problems, and show that it finds better solutions and is substantially faster. DLM has a solid theoretical foundation that can be used as a systematic approach for solving general discrete optimization problems. 1 Introduction The satisfiability (SAT) problem is defined as follows. Given a set of n clauses fC 1 , C 2 , \\Delta \\Delta \\Delta, Cn g on m variables x...