1+ package me.peckb.aoc._2025.calendar.day10
2+
3+ import com.microsoft.z3.ArithExpr
4+ import com.microsoft.z3.Context
5+ import com.microsoft.z3.IntExpr
6+ import com.microsoft.z3.IntNum
7+ import com.microsoft.z3.IntSort
8+ import com.microsoft.z3.Status
9+ import javax.inject.Inject
10+ import me.peckb.aoc.generators.InputGenerator.InputGeneratorFactory
11+ import kotlin.collections.component1
12+ import kotlin.collections.component2
13+ import kotlin.math.min
14+
15+ class Day10 @Inject constructor(
16+ private val generatorFactory : InputGeneratorFactory ,
17+ ) {
18+ fun partOne (filename : String ) = generatorFactory.forFile(filename).readAs(::day10) { input ->
19+ input.sumOf { machine -> flipLights(machine.indicatorLights, machine.buttonSchematics) }
20+ }
21+
22+ fun partTwo (filename : String ) = generatorFactory.forFile(filename).readAs(::day10) { input ->
23+ input.sumOf { machine -> enableJoltages(machine) }
24+ }
25+
26+ private fun enableJoltages (machine : Machine ) : Int {
27+ return Context ().use { ctx ->
28+ val opt = ctx.mkOptimize()
29+
30+ fun intVariableOf (name : String ) = ctx.mkIntConst(name)
31+
32+ fun intValueOf (value : Int ) = ctx.mkInt(value)
33+
34+ infix fun IntExpr.gte (t : IntExpr ) = ctx.mkGe(this , t)
35+
36+ operator fun ArithExpr<IntSort>.plus (t : IntExpr ) = ctx.mkAdd(this , t)
37+
38+ infix fun ArithExpr<IntSort>.equalTo (t : IntExpr ) = ctx.mkEq(this , t)
39+
40+ fun List<IntExpr>.sum () = ctx.mkAdd(* this .toTypedArray())
41+
42+ val ZERO = intValueOf(0 )
43+
44+ val affectedJoltages = mutableMapOf<Int , MutableList <IntExpr >>()
45+ val buttonVariables = machine.buttonSchematics.mapIndexed { index, schematic ->
46+ // create button variable
47+ intVariableOf(index.toString()).also { buttonVariable ->
48+ // track the joltages if affects
49+ schematic.affectedIndices.forEach { affectedIndex ->
50+ affectedJoltages.computeIfAbsent(affectedIndex) { _ -> mutableListOf () }.add(buttonVariable)
51+ }
52+ // add it to the optimizer
53+ opt.Add (buttonVariable gte ZERO )
54+ }
55+ }
56+
57+ affectedJoltages.forEach { (joltageIndex, buttonsAffecting) ->
58+ val targetValue = intValueOf(machine.joltages[joltageIndex])
59+ val sumOfButtonPresses = buttonsAffecting.sum()
60+ opt.Add (sumOfButtonPresses equalTo targetValue)
61+ }
62+
63+ opt.MkMinimize (buttonVariables.sum())
64+
65+ val status = opt.Check ()
66+
67+ if (status == Status .SATISFIABLE ) {
68+ val model = opt.getModel()
69+ ((model.evaluate(buttonVariables.sum(), true ) as IntNum ).int)
70+ } else {
71+ throw IllegalStateException (" No Solution Found" )
72+ }
73+ }
74+ }
75+
76+ fun flipLights (goal : String , buttonSchematics : List <ButtonSchematic >): Long {
77+ val minPressesForState = mutableMapOf (" ." .repeat(goal.length) to 0L )
78+ while (! minPressesForState.containsKey(goal)) {
79+ minPressesForState.entries.toList().forEach { (light, cost) ->
80+ val nextStates = possibleLights(light, buttonSchematics)
81+ nextStates.forEach { state ->
82+ if (minPressesForState.containsKey(state)) {
83+ minPressesForState[state] = min(minPressesForState[state]!! , cost + 1 )
84+ } else {
85+ minPressesForState[state] = cost + 1
86+ }
87+ }
88+ }
89+ }
90+
91+ return minPressesForState[goal]!!
92+ }
93+
94+ fun possibleLights (current : String , buttonSchematics : List <ButtonSchematic >): List <String > {
95+ return buttonSchematics.map { applyLightPress(current, it) }
96+ }
97+
98+ private fun applyLightPress (current : String , buttonSchematic : ButtonSchematic ): String {
99+ return current.mapIndexed { index, c ->
100+ if (buttonSchematic.affectedIndices.contains(index)) {
101+ if (c == ' #' ) { ' .' } else { ' #' }
102+ } else { c }
103+ }.joinToString(" " )
104+ }
105+
106+ private fun day10 (line : String ): Machine {
107+ // SAMPLE: [.##.] (3) (1,3) (2) (2,3) (0,2) (0,1) {3,5,4,7}
108+ val indicatorLights = line.substringBefore(' ]' ).drop(1 )
109+ val buttonSchematics = line.substringAfter(" ] " ).substringBefore(" {" ).split(" " ).map { buttonList ->
110+ val buttonIndices = buttonList.drop(1 ).dropLast(1 ).split(" ," ).map { it.toInt() }
111+ ButtonSchematic (buttonIndices)
112+ }
113+ val joltages = line.substringAfter(' {' ).dropLast(1 ).split(" ," ).map { it.toInt() }
114+
115+ return Machine (indicatorLights, buttonSchematics, joltages)
116+ }
117+ }
118+
119+ data class Machine (
120+ val indicatorLights : String ,
121+ val buttonSchematics : List <ButtonSchematic >,
122+ val joltages : List <Int >,
123+ )
124+
125+ data class ButtonSchematic (val affectedIndices : List <Int >)
0 commit comments