# rw3sat.ex
# http://i...content-available-to-author-only...e.com/3PzRUG
 
defmodule RW3SAT do
  :random.seed :os.timestamp
 
  defp sample(xs) do
    # ref: http://c...content-available-to-author-only...g.com/entry/2015/04/20/101926
    Enum.at(xs, :random.uniform(Enum.count xs) - 1)
  end
 
  defmodule Literal do
    defstruct index: 0, flag: false
  end
  defp literal(index, flag), do: %Literal{index: index, flag: flag}
 
  defmodule Clause do
    defstruct literals: []
  end
  defp clause(literals), do: %Clause{literals: literals}
 
  defmodule CNF do
    defstruct clauses: []
  end
  defp cnf(clauses), do: %CNF{clauses: clauses}
 
  defp satisfied?(l = %Literal{}, x) do
    if l.flag, do: !Enum.at(x, l.index), else: Enum.at(x, l.index)
    # l.flag xor Enum.at(x, l.index)
  end
 
  defp satisfied?(c = %Clause{}, x) do
    Enum.any?(c.literals, &(satisfied?(&1, x)))
  end
 
  defp satisfied?(f = %CNF{}, x) do
    Enum.all?(f.clauses, &(satisfied?(&1, x)))
  end
 
  defp w4(n) do                                                       # W4
    for _ <- 1..n, do: sample([false, true])
  end
 
  defp rw3sat_loop(_, _, _, _, _, true) do                            # W7
    "充足可能である"                                                  # W8
  end
 
  defp rw3sat_loop(_, _, 0, 0, _, _) do
    "おそらく充足不可能である"                                        # W17
  end
 
  defp rw3sat_loop(f, n, 0, r, _, _) do
    x = w4(n)
    rw3sat_loop(f, n, n * 3, r - 1, x, satisfied?(f, x))          # W15,W16
  end
 
  defp rw3sat_loop(f, n, k, r, x, _) do
    c = f.clauses |> Enum.filter(&(!satisfied?(&1, x))) |> sample     # W10
    %{index: i} = sample(c.literals)                                  # W11
    x2 = for j <- 0..n-1 do                                           # W12
      if i == j, do: !Enum.at(x, j), else: Enum.at(x, j)
    end
    rw3sat_loop(f, n, k - 1, r, x2, satisfied?(f, x2))            # W13,W14
  end
 
  def rw3sat(f, n, r) do
    x = w4(n)
    rw3sat_loop(f, n, n * 3, r, x, satisfied?(f, x))          # W2,W3,W5,W6
  end
 
  def main do
    p1 = clause([literal(0, false), literal(1, false), literal(2, false)])
    p2 = clause([literal(3, false), literal(1, false), literal(2, true )])
    p3 = clause([literal(0, true ), literal(3, false), literal(2, false)])
    p4 = clause([literal(0, true ), literal(3, true ), literal(1, false)])
    p5 = clause([literal(3, true ), literal(1, true ), literal(2, false)])
    p6 = clause([literal(0, true ), literal(1, true ), literal(2, true )])
    p7 = clause([literal(0, false), literal(3, true ), literal(2, true )])
    p8 = clause([literal(0, false), literal(3, false), literal(1, true )])
 
    f = cnf([p1, p2, p3, p4, p5, p6, p7, p8])
    # f = cnf([p1, p2, p3, p4, p5, p6, p8])
    rw3sat(f, 4, 3) |> IO.puts
    # => おそらく充足不可能である
  end
 
end
 
RW3SAT.main

IyBydzNzYXQuZXgKIyBodHRwOi8vaS4uLmNvbnRlbnQtYXZhaWxhYmxlLXRvLWF1dGhvci1vbmx5Li4uZS5jb20vM1B6UlVHCgpkZWZtb2R1bGUgUlczU0FUIGRvCiAgOnJhbmRvbS5zZWVkIDpvcy50aW1lc3RhbXAKCiAgZGVmcCBzYW1wbGUoeHMpIGRvCiAgICAjIHJlZjogaHR0cDovL2MuLi5jb250ZW50LWF2YWlsYWJsZS10by1hdXRob3Itb25seS4uLmcuY29tL2VudHJ5LzIwMTUvMDQvMjAvMTAxOTI2CiAgICBFbnVtLmF0KHhzLCA6cmFuZG9tLnVuaWZvcm0oRW51bS5jb3VudCB4cykgLSAxKQogIGVuZAoKICBkZWZtb2R1bGUgTGl0ZXJhbCBkbwogICAgZGVmc3RydWN0IGluZGV4OiAwLCBmbGFnOiBmYWxzZQogIGVuZAogIGRlZnAgbGl0ZXJhbChpbmRleCwgZmxhZyksIGRvOiAlTGl0ZXJhbHtpbmRleDogaW5kZXgsIGZsYWc6IGZsYWd9CgogIGRlZm1vZHVsZSBDbGF1c2UgZG8KICAgIGRlZnN0cnVjdCBsaXRlcmFsczogW10KICBlbmQKICBkZWZwIGNsYXVzZShsaXRlcmFscyksIGRvOiAlQ2xhdXNle2xpdGVyYWxzOiBsaXRlcmFsc30KCiAgZGVmbW9kdWxlIENORiBkbwogICAgZGVmc3RydWN0IGNsYXVzZXM6IFtdCiAgZW5kCiAgZGVmcCBjbmYoY2xhdXNlcyksIGRvOiAlQ05Ge2NsYXVzZXM6IGNsYXVzZXN9CgogIGRlZnAgc2F0aXNmaWVkPyhsID0gJUxpdGVyYWx7fSwgeCkgZG8KICAgIGlmIGwuZmxhZywgZG86ICFFbnVtLmF0KHgsIGwuaW5kZXgpLCBlbHNlOiBFbnVtLmF0KHgsIGwuaW5kZXgpCiAgICAjIGwuZmxhZyB4b3IgRW51bS5hdCh4LCBsLmluZGV4KQogIGVuZAoKICBkZWZwIHNhdGlzZmllZD8oYyA9ICVDbGF1c2V7fSwgeCkgZG8KICAgIEVudW0uYW55PyhjLmxpdGVyYWxzLCAmKHNhdGlzZmllZD8oJjEsIHgpKSkKICBlbmQKCiAgZGVmcCBzYXRpc2ZpZWQ/KGYgPSAlQ05Ge30sIHgpIGRvCiAgICBFbnVtLmFsbD8oZi5jbGF1c2VzLCAmKHNhdGlzZmllZD8oJjEsIHgpKSkKICBlbmQKCiAgZGVmcCB3NChuKSBkbyAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAjIFc0CiAgICBmb3IgXyA8LSAxLi5uLCBkbzogc2FtcGxlKFtmYWxzZSwgdHJ1ZV0pCiAgZW5kCgogIGRlZnAgcnczc2F0X2xvb3AoXywgXywgXywgXywgXywgdHJ1ZSkgZG8gICAgICAgICAgICAgICAgICAgICAgICAgICAgIyBXNwogICAgIuWFhei2s+WPr+iDveOBp+OBguOCiyIgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICMgVzgKICBlbmQKCiAgZGVmcCBydzNzYXRfbG9vcChfLCBfLCAwLCAwLCBfLCBfKSBkbwogICAgIuOBiuOBneOCieOBj+WFhei2s+S4jeWPr+iDveOBp+OBguOCiyIgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgIyBXMTcKICBlbmQKCiAgZGVmcCBydzNzYXRfbG9vcChmLCBuLCAwLCByLCBfLCBfKSBkbwogICAgeCA9IHc0KG4pCiAgICBydzNzYXRfbG9vcChmLCBuLCBuICogMywgciAtIDEsIHgsIHNhdGlzZmllZD8oZiwgeCkpICAgICAgICAgICMgVzE1LFcxNgogIGVuZAoKICBkZWZwIHJ3M3NhdF9sb29wKGYsIG4sIGssIHIsIHgsIF8pIGRvCiAgICBjID0gZi5jbGF1c2VzIHw+IEVudW0uZmlsdGVyKCYoIXNhdGlzZmllZD8oJjEsIHgpKSkgfD4gc2FtcGxlICAgICAjIFcxMAogICAgJXtpbmRleDogaX0gPSBzYW1wbGUoYy5saXRlcmFscykgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgIyBXMTEKICAgIHgyID0gZm9yIGogPC0gMC4ubi0xIGRvICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICMgVzEyCiAgICAgIGlmIGkgPT0gaiwgZG86ICFFbnVtLmF0KHgsIGopLCBlbHNlOiBFbnVtLmF0KHgsIGopCiAgICBlbmQKICAgIHJ3M3NhdF9sb29wKGYsIG4sIGsgLSAxLCByLCB4Miwgc2F0aXNmaWVkPyhmLCB4MikpICAgICAgICAgICAgIyBXMTMsVzE0CiAgZW5kCgogIGRlZiBydzNzYXQoZiwgbiwgcikgZG8KICAgIHggPSB3NChuKQogICAgcnczc2F0X2xvb3AoZiwgbiwgbiAqIDMsIHIsIHgsIHNhdGlzZmllZD8oZiwgeCkpICAgICAgICAgICMgVzIsVzMsVzUsVzYKICBlbmQKCiAgZGVmIG1haW4gZG8KICAgIHAxID0gY2xhdXNlKFtsaXRlcmFsKDAsIGZhbHNlKSwgbGl0ZXJhbCgxLCBmYWxzZSksIGxpdGVyYWwoMiwgZmFsc2UpXSkKICAgIHAyID0gY2xhdXNlKFtsaXRlcmFsKDMsIGZhbHNlKSwgbGl0ZXJhbCgxLCBmYWxzZSksIGxpdGVyYWwoMiwgdHJ1ZSApXSkKICAgIHAzID0gY2xhdXNlKFtsaXRlcmFsKDAsIHRydWUgKSwgbGl0ZXJhbCgzLCBmYWxzZSksIGxpdGVyYWwoMiwgZmFsc2UpXSkKICAgIHA0ID0gY2xhdXNlKFtsaXRlcmFsKDAsIHRydWUgKSwgbGl0ZXJhbCgzLCB0cnVlICksIGxpdGVyYWwoMSwgZmFsc2UpXSkKICAgIHA1ID0gY2xhdXNlKFtsaXRlcmFsKDMsIHRydWUgKSwgbGl0ZXJhbCgxLCB0cnVlICksIGxpdGVyYWwoMiwgZmFsc2UpXSkKICAgIHA2ID0gY2xhdXNlKFtsaXRlcmFsKDAsIHRydWUgKSwgbGl0ZXJhbCgxLCB0cnVlICksIGxpdGVyYWwoMiwgdHJ1ZSApXSkKICAgIHA3ID0gY2xhdXNlKFtsaXRlcmFsKDAsIGZhbHNlKSwgbGl0ZXJhbCgzLCB0cnVlICksIGxpdGVyYWwoMiwgdHJ1ZSApXSkKICAgIHA4ID0gY2xhdXNlKFtsaXRlcmFsKDAsIGZhbHNlKSwgbGl0ZXJhbCgzLCBmYWxzZSksIGxpdGVyYWwoMSwgdHJ1ZSApXSkKCiAgICBmID0gY25mKFtwMSwgcDIsIHAzLCBwNCwgcDUsIHA2LCBwNywgcDhdKQogICAgIyBmID0gY25mKFtwMSwgcDIsIHAzLCBwNCwgcDUsIHA2LCBwOF0pCiAgICBydzNzYXQoZiwgNCwgMykgfD4gSU8ucHV0cwogICAgIyA9PiDjgYrjgZ3jgonjgY/lhYXotrPkuI3lj6/og73jgafjgYLjgosKICBlbmQKICAKZW5kCgpSVzNTQVQubWFpbg==