|
| 1 | +package me.peckb.aoc._2024.calendar.day13 |
| 2 | + |
| 3 | +import com.microsoft.z3.BitVecNum |
| 4 | +import com.microsoft.z3.BitVecSort |
| 5 | +import com.microsoft.z3.Context |
| 6 | +import com.microsoft.z3.Expr |
| 7 | +import com.microsoft.z3.Status |
| 8 | +import me.peckb.aoc._2024.calendar.day13.ClawGameDijkstra.GameNode |
| 9 | +import javax.inject.Inject |
| 10 | +import me.peckb.aoc.generators.InputGenerator.InputGeneratorFactory |
| 11 | +import me.peckb.aoc.pathing.GenericIntDijkstra |
| 12 | + |
| 13 | +class Day13 @Inject constructor( |
| 14 | + private val generatorFactory: InputGeneratorFactory, |
| 15 | +) { |
| 16 | + fun partOne(filename: String) = generatorFactory.forFile(filename).read { input -> |
| 17 | + input.chunked(4) |
| 18 | + .mapNotNull { (a, b, p, _) -> |
| 19 | + val aSpeed = parse(a.split("A: ").last()).let{ (x, y) -> Speed(x, y) } |
| 20 | + val bSpeed = parse(b.split("B: ").last()).let{ (x, y) -> Speed(x, y) } |
| 21 | + val prize = parse(p.split(": ").last()).let{ (x, y) -> GameNode(x, y) } |
| 22 | + |
| 23 | + val game = ClawGameDijkstra(aSpeed, bSpeed, prize) |
| 24 | + |
| 25 | + val solutions = game.solve(GameNode(0, 0).withGame(game), prize.withGame(game)) |
| 26 | + |
| 27 | + solutions[prize] |
| 28 | + } |
| 29 | + .sum() |
| 30 | + } |
| 31 | + |
| 32 | + fun partTwo(filename: String) = generatorFactory.forFile(filename).read { input -> |
| 33 | + input.chunked(4) |
| 34 | + .mapNotNull { (a, b, p, _) -> |
| 35 | + val aSpeed = parse(a.split("A: ").last()).let{ (x, y) -> Speed(x, y) } |
| 36 | + val bSpeed = parse(b.split("B: ").last()).let{ (x, y) -> Speed(x, y) } |
| 37 | + val prize = parse(p.split(": ").last()).let{ (x, y) -> x + BUFFER to y + BUFFER } |
| 38 | + |
| 39 | + Context().use { ctx -> |
| 40 | + val solver = ctx.mkSolver() |
| 41 | + |
| 42 | + val longType = ctx.mkBitVecSort(64) |
| 43 | + fun variableOf(name: String) = ctx.mkConst(name, longType) |
| 44 | + fun valueOf(value: Long) = ctx.mkNumeral(value, longType) as BitVecNum |
| 45 | + operator fun Expr<BitVecSort>.times(t: Expr<BitVecSort>) = ctx.mkBVMul(this, t) |
| 46 | + operator fun Expr<BitVecSort>.plus(t: Expr<BitVecSort>) = ctx.mkBVAdd(this, t) |
| 47 | + infix fun Expr<BitVecSort>.equalTo(t: Expr<BitVecSort>) = ctx.mkEq(this, t) |
| 48 | + infix fun Expr<BitVecSort>.greaterThan(t: Expr<BitVecSort>) = ctx.mkBVSGT(this, t) |
| 49 | + infix fun Expr<BitVecSort>.lessThan(t: Expr<BitVecSort>) = ctx.mkBVSLT(this, t) |
| 50 | + |
| 51 | + val zero = valueOf(0) |
| 52 | + val max = valueOf(500_000_000_000) |
| 53 | + val aPress = variableOf("x") |
| 54 | + val bPress = variableOf("y") |
| 55 | + val aXSpeed = valueOf(aSpeed.x.toLong()) |
| 56 | + val aYSpeed = valueOf(aSpeed.y.toLong()) |
| 57 | + val bXSpeed = valueOf(bSpeed.x.toLong()) |
| 58 | + val bYSpeed = valueOf(bSpeed.y.toLong()) |
| 59 | + val prizeX = valueOf(prize.first) |
| 60 | + val prizeY = valueOf(prize.second) |
| 61 | + |
| 62 | + solver.add(aPress greaterThan zero) |
| 63 | + solver.add(bPress greaterThan zero) |
| 64 | + solver.add(aPress lessThan max) |
| 65 | + solver.add(bPress lessThan max) |
| 66 | + solver.add((aXSpeed * aPress) + (bXSpeed * bPress) equalTo prizeX) |
| 67 | + solver.add((aYSpeed * aPress) + (bYSpeed * bPress) equalTo prizeY) |
| 68 | + |
| 69 | + val status = solver.check() |
| 70 | + |
| 71 | + if (status == Status.SATISFIABLE) { |
| 72 | + val model = solver.model |
| 73 | + val aButtonCost = (model.evaluate(aPress, true) as BitVecNum).long * A_COST |
| 74 | + val bButtonCost = (model.evaluate(bPress, true) as BitVecNum).long * B_COST |
| 75 | + |
| 76 | + aButtonCost + bButtonCost |
| 77 | + } else { |
| 78 | + null |
| 79 | + } |
| 80 | + } |
| 81 | + } |
| 82 | + .sum() |
| 83 | + } |
| 84 | + |
| 85 | + private fun parse(data: String): Pair<Int, Int> { |
| 86 | + return data.split(", ").map{ it.drop(2).toInt() }.let { (x, y) -> x to y } |
| 87 | + } |
| 88 | + |
| 89 | + companion object { |
| 90 | + private const val BUFFER = 10000000000000 |
| 91 | + private const val A_COST = 3 |
| 92 | + private const val B_COST = 1 |
| 93 | + } |
| 94 | +} |
| 95 | + |
| 96 | +class ClawGameDijkstra(val speedA: Speed, val speedB: Speed, val destination: GameNode) : GenericIntDijkstra<GameNode>() { |
| 97 | + |
| 98 | + data class GameNode(val x: Int, val y: Int) : DijkstraNode<GameNode> { |
| 99 | + lateinit var game: ClawGameDijkstra |
| 100 | + |
| 101 | + fun withGame(game: ClawGameDijkstra) = apply { this.game = game } |
| 102 | + |
| 103 | + override fun neighbors(): Map<GameNode, Int> { |
| 104 | + return mutableMapOf<GameNode, Int>().apply { |
| 105 | + if (x + game.speedA.x <= game.destination.x && y + game.speedA.y <= game.destination.y) { |
| 106 | + put(GameNode(x + game.speedA.x, y + game.speedA.y).withGame(game), A_COST) |
| 107 | + } |
| 108 | + if (x + game.speedB.x <= game.destination.x && y + game.speedB.y <= game.destination.y) { |
| 109 | + put(GameNode(x + game.speedB.x, y + game.speedB.y).withGame(game), B_COST) |
| 110 | + } |
| 111 | + } |
| 112 | + } |
| 113 | + } |
| 114 | + |
| 115 | + companion object { |
| 116 | + private const val A_COST = 3 |
| 117 | + private const val B_COST = 1 |
| 118 | + } |
| 119 | +} |
| 120 | + |
| 121 | +data class Speed(val x: Int, val y: Int) |
0 commit comments