rw3sat.coffee

rw3sat.coffee

random_walk_3_sat = (f, n, rr) ->
  ff = (x) -> f.every (fn) -> fn x
  for r in [1..rr]
    x = sample [false, true] for i in [1..n]
    for k in [1..3*n]
      return "充足可能である" if ff x                    # W7,8,9
      c = sample (fn for fn in f when not fn x)        # W10
      idx = parseInt sample c.toString().match(/\d+/g) # W11
      x[idx] = not x[idx]                              # W12
  "おそらく充足不可能である"
sample = (arr) -> arr[Math.floor Math.random() * arr.length]

p1 = (x) ->     x[0] or     x[1] or     x[2]
p2 = (x) ->     x[3] or     x[1] or not x[2]
p3 = (x) -> not x[0] or     x[3] or     x[2]
p4 = (x) -> not x[0] or not x[3] or     x[1]
p5 = (x) -> not x[3] or not x[1] or     x[2]
p6 = (x) -> not x[0] or not x[1] or not x[2]
p7 = (x) ->     x[0] or not x[3] or not x[2]
p8 = (x) ->     x[0] or     x[3] or not x[1]
f = [p1, p2, p3, p4, p5, p6, p7, p8]

console.log random_walk_3_sat f, 4, 3