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

  • 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.