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

In this paper, wepresent efficient trap-escapingstrategies in a search based on discrete Lagrangemultipliers to solve difficult SAT problems. Althougha basic discrete Lagrangian method(DLM) can solve most the satisfiable DIMACS SAT benchmarksefficiently, a few of the large benchmarkshave eluded solutions by any local-search methodstoday. Thesedifficult benchmarks generally have manytraps that attract localsearch trajectories. Tothis end, we identify the existence of traps whenany change to a variable wilt cause the resulting Lagrangianvalue to increase. Using the hanoi4and par16-1benchmarks, weillustrate that someunsatisfied clauses are trapped moreoften than others. Since it is too difficult to remember explicitly all the traps encountered, we proposeto remember these traps implicitly by giving larger increases to Lagrange multipliers of unsatisfied clauses that are trapped moreoften. Weillustrate the merit of this new update strategy by solving someof mostdifficult but satisfiable SATbenchmarks in the DIMACS archive (hanoi4, hanoi4-simple ~ par16-1to par16-5, ]2000, and par32-1-c to par32-3-c). Finally, weapply the same algorithm to improveon the solutions of somebenchmark MAX-SAT problems that we solved before.

Authors

• Zhe Wu Department of Computer Science and Technology, Tsinghua University
• Benjamin W. Wah
• University of Illinois
• Urbana Champaign

Keywords

No keywords are indexed for this paper.