Another Complete Local Search Method for SAT

Local search algorithms are one of the effective methods for solving hard combinatorial problems. However, a serious problem of this approach is that the search often traps at local optima. At AAAI 2004, Fang and Ruml proposed a novel approach which makes local optima disappeared. The basic idea is that, at each local optimal point during the search, the value of the objective function (a local gradient function) at that point is changed by adding some information into the database. Once no more local optima exist, the local search can always find a global optimal. In this paper, along the same approach of Fang and Ruml, we propose a different objective function based on an ordering of propositional variables. Based on this ordering, ordered resolution is performed at each local optimal point and the resolvent is added into the database. This resolvent always increases the value of the objective function so that the local optimal point disappears after a finite number of steps. Preli...

• Type: Conference
• Year: 2005
• Where: LPAR
• Authors: Haiou Shen, Hantao Zhang
• Keywords: Local Optimal Point, Local Search, LPAR 2005, Objective Function