|
| 1 | +package de.ronny_h.aoc.year2025.day10 |
| 2 | + |
| 3 | +import com.microsoft.z3.* |
| 4 | +import de.ronny_h.aoc.AdventOfCode |
| 5 | +import de.ronny_h.aoc.extensions.memoize |
| 6 | +import de.ronny_h.aoc.extensions.substringBetween |
| 7 | +import de.ronny_h.aoc.year2025.day10.LightState.OFF |
| 8 | +import de.ronny_h.aoc.year2025.day10.LightState.ON |
| 9 | + |
| 10 | +fun main() = Factory().run(481, 20142) |
| 11 | + |
| 12 | +class Factory : AdventOfCode<Int>(2025, 10) { |
| 13 | + override fun part1(input: List<String>): Int = input |
| 14 | + .parseMachineDescriptions().sumOf { |
| 15 | + Machine(it).configureIndicatorLights() |
| 16 | + } |
| 17 | + |
| 18 | + override fun part2(input: List<String>): Int = input |
| 19 | + .parseMachineDescriptions().sumOf { |
| 20 | + Machine(it).configureJoltages() |
| 21 | + } |
| 22 | +} |
| 23 | + |
| 24 | +// [.##.] (3) (1,3) (2) (2,3) (0,2) (0,1) {3,5,4,7} |
| 25 | +fun List<String>.parseMachineDescriptions(): List<MachineDescription> = |
| 26 | + map { line -> |
| 27 | + MachineDescription( |
| 28 | + indicatorLights = line.substringBefore("] (").drop(1) |
| 29 | + .map { if (it == '#') ON else OFF }, |
| 30 | + wiringSchematics = line.substringBetween("] ", " {") |
| 31 | + .split(" ").map { it.drop(1).dropLast(1).split(",").map(String::toInt) }, |
| 32 | + joltage = line.substringAfter(") {").dropLast(1).split(",").map(String::toInt), |
| 33 | + ) |
| 34 | + } |
| 35 | + |
| 36 | + |
| 37 | +data class MachineDescription( |
| 38 | + val indicatorLights: List<LightState>, |
| 39 | + val wiringSchematics: List<List<Int>>, |
| 40 | + val joltage: List<Int> |
| 41 | +) |
| 42 | + |
| 43 | +enum class LightState { |
| 44 | + OFF, ON; |
| 45 | + |
| 46 | + fun toggle() = when (this) { |
| 47 | + OFF -> ON |
| 48 | + ON -> OFF |
| 49 | + } |
| 50 | +} |
| 51 | + |
| 52 | +class Machine(private val description: MachineDescription, private val maxPressCount: Int = 7) { |
| 53 | + private val buttons = description.wiringSchematics |
| 54 | + |
| 55 | + fun configureIndicatorLights(): Int { |
| 56 | + val indicatorLightsOff = List(description.indicatorLights.size) { OFF } |
| 57 | + val target = description.indicatorLights |
| 58 | + |
| 59 | + data class RecursiveState(val state: List<LightState>, val buttonsToPress: List<Int>, val pressCount: Int) |
| 60 | + |
| 61 | + lateinit var pressButtons: (RecursiveState) -> Int |
| 62 | + pressButtons = { s -> |
| 63 | + if (s.pressCount == maxPressCount) { |
| 64 | + maxPressCount |
| 65 | + } else { |
| 66 | + val newState = s.state.toMutableList() |
| 67 | + s.buttonsToPress.forEach { newState[it] = newState[it].toggle() } |
| 68 | + if (newState.contentEquals(target)) { |
| 69 | + s.pressCount |
| 70 | + } else { |
| 71 | + buttons.minOf { pressButtons(RecursiveState(newState.toList(), it, s.pressCount + 1)) } |
| 72 | + } |
| 73 | + } |
| 74 | + } |
| 75 | + |
| 76 | + val pressButtonsMemoized = pressButtons.memoize() |
| 77 | + |
| 78 | + return buttons.minOf { pressButtonsMemoized(RecursiveState(indicatorLightsOff, it, 1)) } |
| 79 | + } |
| 80 | + |
| 81 | + /* |
| 82 | + Create equations for joltages as sum of button presses and equal to the required target joltage of the machine. |
| 83 | + Then Optimize for min of total presses. |
| 84 | + Example: |
| 85 | + x0 x1 x2 x3 x4 x5 |
| 86 | + (3) (1,3) (2) (2,3) (0,2) (0,1) |
| 87 | + 0: x4 x5 = 3 |
| 88 | + 1: x1 x5 = 5 |
| 89 | + 2: x2 x3 x4 = 4 |
| 90 | + 3: x0 x1 x3 = 7 |
| 91 | +
|
| 92 | + Use the Z3 Theorem Prover to solve the equations. |
| 93 | + - the C/C++ implementation: https://github.com/Z3Prover/z3/ |
| 94 | + - packaged for Java by https://github.com/tudo-aqua/z3-turnkey |
| 95 | + */ |
| 96 | + fun configureJoltages(): Int = with(Context()) { |
| 97 | + operator fun <R : ArithSort> ArithExpr<R>.plus(other: ArithExpr<R>) = mkAdd(this, other) |
| 98 | + fun Int.int() = mkInt(this) |
| 99 | + |
| 100 | + val optimization = mkOptimize() |
| 101 | + val buttonPresses = buttons.indices.map { mkIntConst("x$it") } |
| 102 | + |
| 103 | + // number of button presses may not be negative |
| 104 | + for (presses in buttonPresses) { |
| 105 | + optimization.Add(mkGe(presses, 0.int())) |
| 106 | + } |
| 107 | + |
| 108 | + // we want to minimize the total number of button presses |
| 109 | + val totalPresses = buttonPresses.fold<IntExpr, ArithExpr<IntSort>>(0.int()) { acc, n -> |
| 110 | + acc + n |
| 111 | + } |
| 112 | + optimization.MkMinimize(totalPresses) |
| 113 | + |
| 114 | + // create the actual system of linear equations |
| 115 | + val targetJoltages = description.joltage |
| 116 | + val joltageExpressions = MutableList<ArithExpr<IntSort>>(targetJoltages.size) { 0.int() } |
| 117 | + for ((button, presses) in buttons.zip(buttonPresses)) { |
| 118 | + for (i in button) { |
| 119 | + joltageExpressions[i] = joltageExpressions[i] + presses |
| 120 | + } |
| 121 | + } |
| 122 | + |
| 123 | + for ((joltage, targetJoltage) in joltageExpressions.zip(targetJoltages)) { |
| 124 | + optimization.Add(mkEq(joltage, targetJoltage.int())) |
| 125 | + } |
| 126 | + |
| 127 | + check(optimization.Check() == Status.SATISFIABLE) |
| 128 | + val minimalTotalPresses = optimization.model.evaluate(totalPresses, false) |
| 129 | + check(minimalTotalPresses is IntNum) |
| 130 | + return minimalTotalPresses.int |
| 131 | + } |
| 132 | +} |
| 133 | + |
| 134 | +fun <T> MutableList<T>.contentEquals(other: List<T>): Boolean { |
| 135 | + if (size != other.size) return false |
| 136 | + forEachIndexed { i, element -> if (other[i] != element) return false } |
| 137 | + return true |
| 138 | +} |
0 commit comments