Consistent Neighborhood for the Satisfiability Problem

Most of the local search methods for the satisfiability problem deal with a complete and inconsistent truth assignment of the problem variables, and try to repair it by switching the truth value of some variables until reaching a model. We propose a new local search algorithm which works on partial truth assignments, but always consistent, instead of complete and inconsistent ones. This method attempts to extend a current partial assignment as a complete method would do. However, instead of backtracking when a conflict arises, it frees at least one variable involved in each falsified clause to restore consistency. Thus, the explored neighborhood is always consistent whereas it is not the case for classical local search algorithms. Experimental results show the competitiveness of our method towards other local search methods.