rw3sat.rb

gistfile1.rb

#!/usr/bin/env ruby
# -*- coding: utf-8 -*-

def random_walk_3_sat(f, n, rr) # W1: R を rr に変更
  ff = f.split(/\s*and\s*/)
  rr.times do
    x = Array.new(n) { [true, false].sample } # W4: a を x に変更
    (3*n).times do
      return "充足可能である" if ff.all? { |c| eval(c) } # W7,8,9
      c = ff.find { |cc| !eval(cc) }                     # W10
      idx = c.scan(/\d+/).sample.to_i                    # W11
      x[idx] = !x[idx]                                   # W12
    end
  end
  "おそらく充足不可能である"
end

P1 = "( x[0] or  x[1] or  x[2])"
P2 = "( x[3] or  x[1] or !x[2])"
P3 = "(!x[0] or  x[3] or  x[2])"
P4 = "(!x[0] or !x[3] or  x[1])"
P5 = "(!x[3] or !x[1] or  x[2])"
P6 = "(!x[0] or !x[1] or !x[2])"
P7 = "( x[0] or !x[3] or !x[2])"
P8 = "( x[0] or  x[3] or !x[1])"
f = [P1, P2, P3, P4, P5, P6, P7, P8].join(' and ')
     
puts random_walk_3_sat(f, 4, 3)