There is no interface, Cure invokes z3 via Erlang port https://github.com/am-kantox/cure-lang/blob/main/src%2Fsmt%2Fcure_smt_process.erl
mudasobwa
Creator of Cure
hauleth
Even with this PRs it doesn’t work, as the solver always used downloaded HiGHS binary instead of using user-provided one. In addition to that HiGHS 1.9.0 (which is downloaded) has some bug, which causes wrong result for my input, and if I change version to 1.12.0 it fails, as it requires additional external libraries (OpenBLAS IIRC). I have forked Dantzig to remove the HiGHS downloader (as it is working improperly anyway) in general and make it more into “CPLEX library” that can be then used with any solver and move solvers downloading and management to separate libs. Something like Nx or Ecto is doing. That way it can use Z3, HiGHS or anything else that can ingest this particular file format (and potentially implement other export formats as well).
@mudasobwa I was also thinking about implementing SMT-LIB generator in Elixir, so it would provide a way to use any SMT solver with Elixir without worrying about compiling binaries and stuff.
2
antoine-duchenet
Yes, my solution does not use any solver library:
defmodule Y2025.D10 do
use Day, input: "2025/10", part1: ~c"l", part2: ~c"l"
defp part2(input) do
lines = input |> parse_input() |> Enum.with_index()
lines
|> Map.new(fn {_, idx} -> {idx, 1000} end)
|> Stream.unfold(fn old_map ->
new_map =
Enum.reduce(lines, old_map, fn {l, idx}, acc ->
maybe_new_min = maybe_min_presses(l)
Map.update!(acc, idx, &min(&1, maybe_new_min))
end)
old_sum = old_map |> Map.values() |> Enum.sum()
new_sum = new_map |> Map.values() |> Enum.sum()
{min(old_sum, new_sum), new_map}
end)
|> Stream.map(&IO.inspect/1)
|> Stream.transform({nil, 100, 100}, &until_stable/2)
|> Enum.take(1)
|> hd()
end
defp until_stable(value, {last_value, requirement, count}) do
case {value == last_value, count} do
{true, 0} ->
{:halt, {value, requirement, count - 1}}
{true, 1} ->
{[value], {value, requirement, count - 1}}
{true, _} ->
{[], {value, requirement, count - 1}}
{false, _} ->
{[], {value, requirement, requirement - 1}}
end
end
defp maybe_min_presses(%{lights: _, buttons: buttons, requirements: requirements}) do
target_map = index(requirements)
repair(buttons, target_map)
end
defp repair(buttons, target_map) do
[initial_candidate] =
buttons
|> Enum.sort_by(&Enum.count/1, :desc)
|> Enum.take(1)
target_sum =
target_map
|> Map.values()
|> Enum.sum()
initial_presses = div(target_sum, length(initial_candidate))
buttons_map =
buttons
|> Enum.map(&{&1, if(&1 == initial_candidate, do: initial_presses, else: 0)})
|> Map.new()
initial_map =
target_map
|> Map.keys()
|> Enum.map(&if Enum.member?(initial_candidate, &1), do: initial_presses, else: 0)
|> index()
repair_rec(initial_map, target_map, buttons_map)
end
defp repair_rec(target_map, target_map, buttons_map) do
buttons_map
|> Map.values()
|> Enum.sum()
end
defp repair_rec(current_map, target_map, buttons_map) do
candidates =
buttons_map
|> Map.keys()
|> Enum.map(&{score(&1, current_map, target_map), &1})
|> Enum.sort_by(&elem(&1, 0), :desc)
add = Enum.take(candidates, Enum.random(1..3))
sub = Enum.take(candidates, -Enum.random(1..3))
mutations =
if Enum.random(0..3) == 0 do
candidates
|> Enum.shuffle()
|> Enum.take(Enum.random(1..3))
else
[]
end
{next_map, new_buttons_map} =
add
|> Enum.concat(sub)
|> Enum.concat(mutations)
|> Enum.reduce({current_map, buttons_map}, &apply_button/2)
repair_rec(next_map, target_map, new_buttons_map)
end
defp apply_button({score, button}, {current_map, buttons_map}) do
dir =
cond do
score > 0 and Map.get(buttons_map, button) > 0 and Enum.random(0..49) == 0 -> -1
score > 0 -> 1
score < 0 and Map.get(buttons_map, button) > 0 -> -1
true -> 0
end
new_map =
Enum.reduce(button, current_map, fn idx, acc ->
Map.update!(acc, idx, &(&1 + dir))
end)
new_buttons_map = Map.update!(buttons_map, button, fn count -> count + dir end)
{new_map, new_buttons_map}
end
defp score(button, current_map, target_map) do
Enum.reduce(button, 0, fn idx, acc ->
c = Map.fetch!(current_map, idx)
t = Map.fetch!(target_map, idx)
cond do
c < t ->
acc + Math.sqrt(t - c)
c > t ->
acc - Math.sqrt(c - t)
true ->
acc
end
end)
end
defp index(lights) do
lights
|> Enum.with_index()
|> Enum.reduce(%{}, fn {light, idx}, acc -> Map.put(acc, idx, light) end)
end
defp parse_input(input), do: Enum.map(input, &parse_line/1)
defp parse_line(line) do
[lights | rest] =
~r/[\[\(\{]([\d\.\#,]+)[\}\)\]]/
|> Regex.scan(line)
|> Enum.map(&Enum.at(&1, 1))
{buttons, [requirements]} =
rest
|> Enum.map(
&(&1
|> Utils.splitrim(",")
|> Enum.map(fn num_str -> String.to_integer(num_str) end))
)
|> Enum.split(-1)
%{lights: Utils.splitrim(lights, ""), buttons: buttons, requirements: requirements}
end
end
It’s basically a recursive reparation approach with genetic programming inspiration. Those parameters converged “pretty quickly” :
- A single iteration takes around ~1 second, it processes all the machines
- We wait for the minimum (sum) to be stable for 100 iterations
- Each iteration “repairs” each machine until it reaches the target numeric counters state, keeping track of the button presses count
- The initial state (numeric counters and presses count) is filled with a very rough approximation, it is reset on each reparation
- Each reparation step presses between 1 and 3 buttons, prioritized by a score (how relevant each button is to converge)
- Each reparation step unpresses between 1 and 3 buttons, prioritized by a score (how irrelevant each button is to converge)
- There is 25% chance that 1 to 3 additional buttons (mutations) get triggered, pressed or unpressed depending on their relevance to converge
- There is a slight 2% chance that any button that should be pressed would be unpressed (only if it can be unpressed, it helps to converge quicker by jumping out of rabbit holes caused by the very basic / poor scoring method)
It took ~5min20sec to give the answer for my input, but I suspect it may vary a lot 
1
Kevo
That seems pretty quick from where I’m at. I’m running it now and it does seem to be slowly working it’s way down to the correct result, but it’s been going for about 2 hours. It might take another hour or two to finally get to the right number at the rate it’s been counting down.
0
antoine-duchenet
I can’t say I’m surprised, the time it takes to converge vary a lot for my input and seems very sensible to the parameters (but I did not benchmark it cleanly, so it might just be an impression). It’s not a very reliable solution in its current state, and I’m not sure I’ll take time to improve it 
0
Kevo
I let it run overnight and it was still working its way down toward the correct value, but I gave up on it in the end. Still, I think it was a good attempt without using a solver. 
1
ironcamel
I’m guessing this solution for part 2 did not work. The problem I see is that z3 doesn’t provide the actual optimal (minimum) value on it’s first run. It provides a guess at what the optimal value is. What the official z3 api bindings do is they repeatedly call z3 behind the scenes. Each time z3 is called, the previous value it returned is used to add a new constraint. This is repeated until the result doesn’t change.
For example, consider this z3 input which attempts to find the 2 integers which multiply to 24, and have the minimum sum:
(declare-const x Int)
(declare-const y Int)
(assert (= (* x y) 24))
(assert (> x 0))
(assert (> y 0))
(minimize (+ x y))
(check-sat)
(get-model)
That outputs 8 and 3:
(
(define-fun x () Int
8)
(define-fun y () Int
3)
)
This is obviously wrong because the sum of 8 and 3 is 11 which is not optimal. The optimal answer is 6 and 4 which has a sum of 10. To get the optimal value, you have to run z3 again with the added constraint that the next answer should try to be more optimal than the previous answer: (assert (< (+ x y) 11))
(declare-const x Int)
(declare-const y Int)
(assert (= (* x y) 24))
(assert (> x 0))
(assert (> y 0))
(minimize (+ x y))
(assert (< (+ x y) 11))
(check-sat)
(get-model)
Now that will output the correct values of 6 and 4.
0
lud
Well I added a unit test with my expected solution and it works 100% of times without a second call.
0
Kevo
z3 worked on my input. I tried a couple of the different solver options in this thread, having no experience with any of them, and z3 was the only one that worked without error for me. Thanks btw, @lud . I fully expected it not to work on my input or to give me some error, but I just brew installed z3, set the path, and it worked on the first try. Now I just need to go back when I have time and dig into how it all works so I can actually understand it.
(Time, who has time? 
)
1
KeithFrost
I became obsessed with this problem after it took me a whole day to get a solution to Part 2. I have now implemented three different solutions: one, an exceedingly clever one (I can say this, because I didn’t think of the algorithm) which extends the Part 1 solution by finding all of the ways (with 0 or 1 presses of each button) to match the least significant bits of the desired joltages, and then recursing on the now-even joltages divided by two, until the desired joltages are all zero. I’ll post that one here, because it is the shortest self-contained solution (the other two are a long self-contained Elixir solution which implements Bareiss’s algorithm for reduction of integer matrices and then searches values of the remaining free variables for solutions, and another one that composes Prolog code that invokes SWI Prolog’s CLPQ solver).
defmodule Machine do
defstruct target: 0, buttons: %{}, joltages: %{}, parity_map: %{}
def parse_target(target_str) do
to_charlist(target_str)
|> Enum.with_index()
|> Enum.reduce(0, fn {ch, i}, t ->
case ch do
?. ->
t
?# ->
Bitwise.bor(t, Bitwise.bsl(1, i))
end
end)
end
def parse_buttons(buttons_str) do
Regex.scan(~r"\(([\d,]+)\)\s*", buttons_str)
|> Enum.map(fn [_match, button_str] ->
String.split(button_str, ",")
|> Enum.map(&String.to_integer/1)
end)
|> Enum.with_index(fn l, i -> {i, MapSet.new(l)} end)
|> Map.new()
end
def parse_joltages(joltages_str) do
String.split(joltages_str, ",")
|> Enum.map(&String.to_integer/1)
|> Enum.with_index(fn jolt, i -> {i, jolt} end)
|> Map.new()
end
def parse_line(line) do
case Regex.run(~r"\[([.#]+)\]\s*([^{]+)\s*{([^}]+)}", line) do
[_match, target_str, buttons_str, joltages_str] ->
%__MODULE__{
target: parse_target(target_str),
buttons: parse_buttons(String.trim(buttons_str)),
joltages: parse_joltages(joltages_str)
}
end
end
def parse(lines) do
Enum.map(lines, &parse_line/1)
|> Enum.map(&compute_parity_map/1)
end
def joltage_parity(joltages) do
Enum.reduce(joltages, 0, fn {j, v}, parity ->
Bitwise.bor(parity, Bitwise.bsl(Bitwise.band(v, 1), j))
end)
end
def count_bpushes(bpushed, acc \\ 0) do
if bpushed == 0 do
acc
else
bpushed = Bitwise.band(bpushed, bpushed - 1)
count_bpushes(bpushed, acc + 1)
end
end
def compute_parity_map(machine = %__MODULE__{buttons: buttons}) do
bpush_options = 0..(Bitwise.bsl(1, map_size(buttons)) - 1)
parity_map = Enum.reduce(bpush_options, %{}, fn bpushed, map ->
delta_jolts = Enum.reduce(buttons, %{}, fn {i, set}, djolts ->
if Bitwise.band(1, Bitwise.bsr(bpushed, i)) == 1 do
Enum.reduce(set, djolts, fn j, djolts ->
Map.update(djolts, j, 1, fn v -> v + 1 end)
end)
else
djolts
end
end)
parity = joltage_parity(delta_jolts)
push_count = count_bpushes(bpushed)
push = {push_count, bpushed, delta_jolts}
Map.update(map, parity, [push], fn pushes -> [push | pushes] end)
end)
%__MODULE__{machine | parity_map: parity_map}
end
def solve1(%__MODULE__{target: target, parity_map: parity_map}) do
parity_map[target]
|> Enum.map(fn {push_count, _bpushed, _delta_jolts} -> push_count end)
|> Enum.min()
end
def reduced_joltages(joltages, delta_jolts) do
Enum.reduce(delta_jolts, joltages, fn {j, dv}, joltages ->
Map.update!(joltages, j, fn v -> v - dv end)
end)
end
def solve2(mach = %__MODULE__{joltages: joltages, parity_map: parity_map}) do
if Enum.all?(joltages, fn {_j, v} -> v == 0 end) do
0
else
target = joltage_parity(joltages)
push_options = Map.get(parity_map, target, [])
Enum.map(push_options, fn {push_count, _bpushed, delta_jolts} ->
rjoltages = reduced_joltages(joltages, delta_jolts)
{push_count, rjoltages}
end)
|> Enum.reject(fn {_count, rjoltages} ->
Enum.any?(rjoltages, fn {j, v} ->
if Bitwise.band(v, 1) == 1, do: raise("odd joltage #{v} at #{j}")
v < 0
end)
end)
|> Enum.map(fn {count, rjoltages} ->
rjoltages = Enum.map(rjoltages, fn {j, v} -> {j, Bitwise.bsr(v, 1)} end)
|> Map.new()
count2 = solve2(%__MODULE__{mach | joltages: rjoltages})
if count2 != nil do
count + Bitwise.bsl(count2, 1)
end
end)
|> Enum.min(fn -> nil end)
end
end
end
1