A two level local search for MAXSAT problems with hard and soft constraints

Abstract. Local search techniques have attracted considerable interest in the AI community since the development of GSAT for solving large propositional SAT problems. Newer SAT techniques, such as the Dis-crete Lagrangian Method (DLM), have further improved on GSAT and can also be applied to general constraint satisfaction and optimisation. However, little work has applied local search to MAX-SAT problems with hard and soft constraints. As many real-world problems are best represented by hard (mandatory) and soft (desirable) constraints, the development of effective local search heuristics for this domain is of sig-nificant practical importance. This paper extends previous work on dynamic constraint weighting by introducing a two-level heuristic that switches search strategy according to whether a current solution contains unsatisfied hard constraints. Us-ing constraint weighting techniques derived from DLM to satisfy hard constraints, we apply a Tabu search to optimise the soft constraint vio-lations. These two heuristics are further combined with a dynamic hard constraint multiplier that changes the relative importance of the hard constraints during the search. We empirically evaluate this new algo-rithm using a set of randomly generated 3-SAT problems of various sizes and difficulty, and in comparison with various state-of-the-art SAT tech-niques. The results indicate that our dynamic, two-level heuristic offers significant performance benefits over the standard SAT approaches.