Abstract: Satisfiability problem is a basic problem in logic,and also is NP-hard. Survey propagation(SP) is a very effective algorithm for this problem. However, SP tends not to converge in hard region, or gives wrong assignments to the variables. An algorithm combined with SP and ant colony optimization(ACO) was proposed. The messages calculated in SP were used in ACO as guidance to help ACO find a solution. And local search was conducted in the new algorithm.The new algorithm can quickly find solutions for some instances that SP doesn't work.

Key words: Survey propagation, Hard region, Ant colony optimization, Local search