satisfiable assignment close to an unsatisfiable assignment

Given a CNF formula $F$ and an unsatisfiable assignment $\alpha_u$ over the variables in $F$, I want to find a satisfiable assignment $\alpha_s$ which is as close as possible to $\alpha_u$, w.r.t. the hamming distance.

Do you have any idea how I could find such an assignment?

I first thought about encoding $\alpha_u$ in $F$ using unit-clauses and then find a maximally satisfying assignment over the new formula, but this won't work for dense formulas.

Thanks, Stefan

-
The worst case complexity of finding such an assignment is definitely non polynomial, since its exist implies satisfiability of $F$. –  Levon Haykazyan Aug 10 '11 at 15:37
Thank you, I am aware of that, but there are still better and worse ways of doing it, I guess –  stefan Aug 10 '11 at 16:25
@Levon: Have you proved P≠NP? :) –  Tsuyoshi Ito Aug 10 '11 at 16:27
@Tsuyoshi: Good catch, I need to be more careful :) –  Levon Haykazyan Aug 10 '11 at 19:07
For those not familiar with complexity, Levon's error is using "definitely" , since we do not know if P is equal to NP or not. –  chazisop Aug 11 '11 at 16:56

Breadth first local search seems the obvious choice. Generate a list of all the variables in the unsatisfied clauses. Try flipping each one in turn and see if you get a satisfying assignment. If they all fail, repeat the process except flipping two variables, and so on. Pseudocode:

function find_nearby_solution(how_nearby)
if how_nearby < 1
error
vars := get_variables_of_unsatisfied_clauses()
for v in vars
flip v
mark v flipped
if how_nearby > 1
if find_nearby_solution(how_nearby - 1)
return true
else
if all_clauses_satisfied()
return true
unflip v
mark v unflipped
return false


Call find_nearby_solution(1), find_nearby_solution(2), ... until one of the calls returns true. At that point you have your satisfying assignment.

-