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