ash/lib/sat_solver/utils.ex
Zach Daniel 665a9fb5c4 improvement: optimize sat solving
1. only convert to CNF once
2. group predicates that only appear in specific combinations to limit amount of variables provided to the sat solver

Number 2 above does technically slow down all cases a bit, but the optimization is really important when it matters. And cases that don't need this optimization still happen on the order microseconds anyway.
2022-11-15 01:45:55 -05:00

62 lines
1.3 KiB
Elixir

defmodule Ash.SatSolver.Utils do
@moduledoc false
def replace_ordered_sublist([], _sublist, _replacement), do: []
def replace_ordered_sublist([h | tail] = list, sublist, replacement) do
if List.starts_with?(list, sublist) do
[replacement | Enum.drop(list, length(sublist))]
else
[h | replace_ordered_sublist(tail, sublist, replacement)]
end
end
def is_ordered_sublist_of?(_, []), do: false
def is_ordered_sublist_of?(sublist, [_ | rest] = list) do
List.starts_with?(list, sublist) || is_ordered_sublist_of?(sublist, rest)
end
def ordered_sublists(list) do
front = sublists_front(list)
back =
list
|> sublists_back()
|> Enum.reject(&(&1 in front))
front ++ back
end
def sublists_back([_, _]), do: []
def sublists_back([]), do: []
def sublists_back([_]), do: []
def sublists_back(list) do
list = :lists.droplast(list)
[list | sublists_back(list)]
end
def sublists_front(list) do
list
|> do_sublists_front()
|> Enum.reject(fn
^list ->
true
[_] ->
true
_ ->
false
end)
end
def do_sublists_front([]) do
[]
end
def do_sublists_front([_first | rest] = list) do
[list | do_sublists_front(rest)]
end
end