2
$\begingroup$

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

  • 1
    The worst case complexity of finding such an assignment is definitely non polynomial, since its exist implies satisfiability of $F$.2011-08-10
  • 0
    Thank you, I am aware of that, but there are still better and worse ways of doing it, I guess2011-08-10
  • 2
    @Levon: Have you proved P≠NP? :)2011-08-10
  • 1
    @Tsuyoshi: Good catch, I need to be more careful :)2011-08-10
  • 0
    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.2011-08-11
  • 0
    It is $\mathsf{NP\text{-}hard}$ and solvable in $\mathsf{P}^\mathsf{NP}$. Is there a simple many-one reduction to SAT? I don't know.2011-08-12
  • 0
    We might ask the same question as a promise problem: we know that the given CNF is satisfiable, and given an assignment, want to find a satisfying assignment close to it. This sounds like the decoding problem of binary codes.2011-08-12

1 Answers 1

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.