3sat_solver.rb

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

require 'pp'

formula =
  ["(  x[0] or  x[2] or !x[4] )",
   "( !x[3] or !x[4] or !x[5] )",
   "( !x[2] or !x[4] or  x[5] )",
   "( !x[1] or  x[3] or !x[5] )",
   "( !x[0] or !x[3] or  x[1] )",
   "( !x[3] or !x[4] or  x[5] )",
   "( !x[0] or !x[2] or !x[3] )",
   "(  x[1] or !x[3] or !x[4] )",
   "(  x[1] or  x[3] or !x[5] )"
]

n_variables = 10

try_steps = 11

class ThreeSatError < StandardError ; end
def markov_chain_3sat(f,n,k)
  x = Array.new(n){[true, false].sample}
  k.times do
    if f.all?{|c| eval(c)}
      return x
    else
      i = f.keep_if{|c| eval(c) }.sample.scan('\d+').sample.to_i
      x[i] = !x[i]
    end
  end
  raise ThreeSatError, 'There seems to be no solution.'
end

begin
  pp markov_chain_3sat(formula,n_variables,try_steps)
rescue ThreeSatError => e
  puts e.message
end