# 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