satisfiable assignment close to an unsatisfiable assignment

Question

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

Answer 1

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
      if v not already flipped
         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.