rw3sat.py

rw3sat.py

#!/usr/bin/env python
# -*- coding: utf-8 -*-
import random
import re

def random_walk_3_sat(f, n, rr):
  ff = re.split(r'\s*and\s*', f)
  for r in xrange(rr):
    x = [random.choice([False, True]) for i in xrange(n)] # W4
    for k in xrange(3 * n):
      if (eval(f)):
        return u'充足可能である'                          # W7,8
      c = random.choice([c for c in ff if not eval(c)])   # W10
      idx = int(random.choice(re.findall(r'\d+', c)))     # W11
      x[idx] = not x[idx]                                 # W12
  return u'おそらく充足不可能である'

p1 = "(    x[0] or     x[1] or     x[2])"
p2 = "(    x[3] or     x[1] or not x[2])"
p3 = "(not x[0] or     x[3] or     x[2])"
p4 = "(not x[0] or not x[3] or     x[1])"
p5 = "(not x[3] or not x[1] or     x[2])"
p6 = "(not x[0] or not x[1] or not x[2])"
p7 = "(    x[0] or not x[3] or not x[2])"
p8 = "(    x[0] or     x[3] or not x[1])"
f = ' and '.join([p1, p2, p3, p4, p5, p6, p7, p8])

print random_walk_3_sat(f, 4, 3)