DPLL Visualizer

defmodule DpllSolver do
  @moduledoc """
  A pure functional implementation of the DPLL algorithm.
  """

  @spec solve([[integer]]) :: {:sat, map} | :unsat
  def solve(clauses) do
    case dpll(clauses, %{}) do
      {:sat, model} -> {:sat, model}
      :unsat -> :unsat
    end
  end

  defp dpll(clauses, model) do
    cond do
      # Check for empty clauses (conflict)
      Enum.any?(clauses, &(&1 == [])) -> :unsat
      
      # Check if all clauses are satisfied
      clauses == [] -> {:sat, model}
      
      true ->
        # 1. Unit Propagation
        case find_unit_clause(clauses) do
          nil -> 
            # 2. Pure Literal Elimination
            case find_pure_literal(clauses) do
              nil -> 
                # 3. Branching (Splitting)
                var = choose_variable(clauses)
                case dpll(assign(clauses, var, true), Map.put(model, var, true)) do
                  {:sat, m} -> {:sat, m}
                  :unsat -> dpll(assign(clauses, var, false), Map.put(model, var, false))
                end
              lit -> 
                dpll(assign(clauses, lit, true), Map.put(model, lit, true))
            end
          lit -> 
            dpll(assign(clauses, lit, true), Map.put(model, lit, true))
        end
    end
  end

  defp assign(clauses, lit, val) do
    # Returns new clauses with lit satisfied and !lit removed
    Enum.map(clauses, fn clause ->
      cond do
        lit in clause -> :removed
        -lit in clause -> List.delete(clause, -lit)
        true -> clause
      end
    end)
    |> Enum.reject(&(&1 == :removed))
  end

  defp find_unit_clause(clauses) do
    Enum.find_value(clauses, fn
      [lit] -> lit
      _ -> nil
    end)
  end

  defp find_pure_literal(clauses) do
    all_lits = List.flatten(clauses)
    Enum.find_value(all_lits, fn lit ->
      if (-lit) not in all_lits, do: lit, else: nil
    end)
  end

  defp choose_variable(clauses) do
    List.flatten(clauses) |> hd |> abs
  end
end