@@ -3,6 +3,8 @@ package adventofcode.year2025
33import adventofcode.Puzzle
44import adventofcode.PuzzleInput
55import adventofcode.common.Permutations.powersets
6+ import com.microsoft.z3.Context
7+ import com.microsoft.z3.Status.SATISFIABLE
68
79class Day10Factory (
810 customInput : PuzzleInput ? = null ,
@@ -28,6 +30,46 @@ class Day10Factory(
2830 }.size
2931 }
3032
33+ override fun partTwo () =
34+ parseInput()
35+ .sumOf { machine ->
36+ Context ().use { ctx ->
37+ val solver = ctx.mkOptimize()
38+
39+ // Create variables for button presses and ensure they are positive.
40+ val buttons =
41+ machine.buttons.indices
42+ .map { index -> ctx.mkIntConst(" button#$index " ) }
43+ .onEach { button -> solver.Add (ctx.mkGe(button, ctx.mkInt(0 ))) }
44+
45+ // Create equations: For each joltage counter, ensure the sum of all button presses is equal to the specified joltage
46+ machine.joltages.forEachIndexed { counter, joltage ->
47+ val pressedButtons =
48+ machine.buttons
49+ .withIndex()
50+ .filter { (_, counters) -> counter in counters }
51+ .map { buttons[it.index] }
52+
53+ solver.Add (ctx.mkEq(ctx.mkAdd(* pressedButtons.toTypedArray()), ctx.mkInt(joltage)))
54+ }
55+
56+ // Solve for the minimum number of button presses
57+ val buttonPresses = ctx.mkIntConst(" buttonPresses" )
58+ solver.Add (ctx.mkEq(buttonPresses, ctx.mkAdd(* buttons.toTypedArray())))
59+ solver.MkMinimize (buttonPresses)
60+
61+ when (solver.Check ()) {
62+ SATISFIABLE ->
63+ solver.model
64+ .evaluate(buttonPresses, false )
65+ .toString()
66+ .toInt()
67+
68+ else -> 0
69+ }
70+ }
71+ }
72+
3173 companion object {
3274 private data class Machine (
3375 val lights : List <Boolean >,
0 commit comments