Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

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

share|cite|improve this question
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
   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
            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.

share|cite|improve this answer

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.