SAT – a randomized algorithm

As everybody knows, SAT is NP-complete.

Here is a randomized algorithm that (eventually) solves an instance of a SAT-Problem (in polynomial time).

The problem must be given in conjunctive normal form. The algorithm uses the following format for the problem:

Let’s call our boolean variables $v_1, v_2, \dots, v_n$ . I want to show the format for the algorithm with an example. Consider the following CNF: $(v_1 \vee \lnot v_2) \wedge (\lnot v_1 \vee v_3) \wedge (v_2 \vee v_3 \vee \lnot v_4)$ . A satisfiying combination of variables would be: $v_1=1, v_2=1, v_3=1, v_4=0$ (1 corresponds with true, 0 corresponds with false).

The above formula would be translated into the following array of arrays:

[[1,-2],[1,3],[2,3,-4]]

The first element, [1,-2] shows, that $v_1$ is used normal and $v_2$ is negated. The other elements show things correspondingly.

Here’s the source code (Ruby):

# Input format: Array of arrays
# [[+1,+2],[-1,+3]] => (A or B) and (-A or C) 
# i.e. sign indicates, wether variable is beeing neglected (-) or not (+)
# !!! Special: Using 1-indexed subarrays (otherwise problems with sign and 0)


def randomBool()
  return (rand(2)==0)
end

# controls the whole CNF
def validateField(field, belegung)
  result=true
  field.each { |b| 
    result=(result and validateSubField(b, belegung))
  }
  return result
end

# controls a subarray of the CNF
def validateSubField(field,belegung)
  result=false
  field.each { |b|
    zw = belegung[b.abs]
    if (b<0)
      zw = (not zw)
    end
    result = (result or zw) 
  }
  return result
end

# n is the number of variables
def solve(field, n)
  result = Array.new(n+1){ |i| randomBool() }
  timeout=200
  timeout.times{
    # look for corrupt clause
    field.each { |e| 
      if (not validateSubField(e, result))
        zw = rand(e.length)
        result[e[zw]]=(not result[e[zw]])
        break
      end
    }
  }
  result[0]="Result:"
  if (validateField(field, result))
    return result
  end
  return "No solution found in #{timeout} steps found"
end


# Generates a CNF using n variables and l subfields with k elements
def generateRandomCNF(n, l, k)
  result = Array.new(l){ Array.new(k) }
  result.each { |f| 
    f.length.times{ |i|
      a = (rand(n)*((rand(2.0)-0.5)*2)).to_i
      while (a==0)
        a = (rand(n)*((rand(2.0)-0.5)*2)).to_i
      end
      f[i]=a
    }
  }
end

This entry was posted on 4. August 2009 at 2:57 am and is filed under Algorithms, Probability theory. You can follow any responses to this entry through the RSS 2.0 feed. You can leave a response, or trackback from your own site.

phimuemue's Blog