Manually solve, rather than generic Z3 (#273)

since it's a simple system of equations, solving the equations by hand was faster.

Author: peckb1

README.md

@@ -159,7 +159,7 @@ as the value which passed the given day/phase combination
 
 #### 2024
 * Day 11 The fact that the order of stones didn't actually matter helped to allow us to just keep a list of how many we had.
-* Day 13 Being able to solve the basic with shortest path while needing math for part two is always fun re-learning linear algebra.
+* Day 13 Being able to solve the basic with shortest path while needing math for part two is always fun re-learning linear algebra. And refactoring always speeds things up.
 
 ## Takeaways
 

src/main/kotlin/me/peckb/aoc/_2024/calendar/day13/Day13.kt

@@ -1,121 +1,66 @@
 package me.peckb.aoc._2024.calendar.day13
 
-import com.microsoft.z3.BitVecNum
-import com.microsoft.z3.BitVecSort
-import com.microsoft.z3.Context
-import com.microsoft.z3.Expr
-import com.microsoft.z3.Status
-import me.peckb.aoc._2024.calendar.day13.ClawGameDijkstra.GameNode
 import javax.inject.Inject
 import me.peckb.aoc.generators.InputGenerator.InputGeneratorFactory
-import me.peckb.aoc.pathing.GenericIntDijkstra
+import kotlin.math.roundToLong
 
 class Day13 @Inject constructor(
   private val generatorFactory: InputGeneratorFactory,
 ) {
   fun partOne(filename: String) = generatorFactory.forFile(filename).read { input ->
     input.chunked(4)
-      .mapNotNull { (a, b, p, _) ->
-        val aSpeed = parse(a.split("A: ").last()).let{ (x, y) -> Speed(x, y)    }
-        val bSpeed = parse(b.split("B: ").last()).let{ (x, y) -> Speed(x, y)    }
-        val prize = parse(p.split(": ").last()).let{ (x, y) -> GameNode(x, y) }
-
-        val game = ClawGameDijkstra(aSpeed, bSpeed, prize)
-
-        val solutions = game.solve(GameNode(0, 0).withGame(game), prize.withGame(game))
-
-        solutions[prize]
-      }
+      .mapNotNull { (a, b, p, _) -> solve(a, b, p, 0) }
       .sum()
   }
 
   fun partTwo(filename: String) = generatorFactory.forFile(filename).read { input ->
     input.chunked(4)
-      .mapNotNull { (a, b, p, _) ->
-        val aSpeed = parse(a.split("A: ").last()).let{ (x, y) -> Speed(x, y)    }
-        val bSpeed = parse(b.split("B: ").last()).let{ (x, y) -> Speed(x, y)    }
-        val prize = parse(p.split(": ").last()).let{ (x, y) -> x + BUFFER to y + BUFFER }
-
-        Context().use { ctx ->
-          val solver = ctx.mkSolver()
-
-          val longType = ctx.mkBitVecSort(64)
-          fun variableOf(name: String) = ctx.mkConst(name, longType)
-          fun valueOf(value: Long) = ctx.mkNumeral(value, longType) as BitVecNum
-          operator fun Expr<BitVecSort>.times(t: Expr<BitVecSort>) = ctx.mkBVMul(this, t)
-          operator fun Expr<BitVecSort>.plus(t: Expr<BitVecSort>) = ctx.mkBVAdd(this, t)
-          infix fun Expr<BitVecSort>.equalTo(t: Expr<BitVecSort>) = ctx.mkEq(this, t)
-          infix fun Expr<BitVecSort>.greaterThan(t: Expr<BitVecSort>) = ctx.mkBVSGT(this, t)
-          infix fun Expr<BitVecSort>.lessThan(t: Expr<BitVecSort>) = ctx.mkBVSLT(this, t)
-
-          val zero = valueOf(0)
-          val max = valueOf(500_000_000_000)
-          val aPress = variableOf("x")
-          val bPress = variableOf("y")
-          val aXSpeed = valueOf(aSpeed.x.toLong())
-          val aYSpeed = valueOf(aSpeed.y.toLong())
-          val bXSpeed = valueOf(bSpeed.x.toLong())
-          val bYSpeed = valueOf(bSpeed.y.toLong())
-          val prizeX = valueOf(prize.first)
-          val prizeY = valueOf(prize.second)
-
-          solver.add(aPress greaterThan zero)
-          solver.add(bPress greaterThan zero)
-          solver.add(aPress lessThan max)
-          solver.add(bPress lessThan max)
-          solver.add((aXSpeed * aPress) + (bXSpeed * bPress) equalTo prizeX)
-          solver.add((aYSpeed * aPress) + (bYSpeed * bPress) equalTo prizeY)
-
-          val status = solver.check()
-
-          if (status == Status.SATISFIABLE) {
-            val model = solver.model
-            val aButtonCost = (model.evaluate(aPress, true) as BitVecNum).long * A_COST
-            val bButtonCost = (model.evaluate(bPress, true) as BitVecNum).long * B_COST
-
-            aButtonCost + bButtonCost
-          } else {
-            null
-          }
-        }
-      }
+      .mapNotNull { (a, b, p, _) -> solve(a, b, p, BUFFER) }
       .sum()
   }
 
-  private fun parse(data: String): Pair<Int, Int> {
-    return data.split(", ").map{ it.drop(2).toInt() }.let { (x, y) -> x to y }
+  private fun parse(data: String): Pair<Long, Long> {
+    return data.split(", ").map{ it.drop(2).toLong() }.let { (x, y) -> x to y }
   }
 
-  companion object {
-    private const val BUFFER = 10000000000000
-    private const val A_COST = 3
-    private const val B_COST = 1
-  }
-}
+  private fun solve(a: String, b: String, p: String, buffer: Long): Long? {
+    val aSpeed = parse(a.split("A: ").last()).let{ (x, y) -> Speed(x, y) }
+    val bSpeed = parse(b.split("B: ").last()).let{ (x, y) -> Speed(x, y) }
+    val prize = parse(p.split(": ").last()).let{ (x, y) -> x + buffer to y + buffer }
 
-class ClawGameDijkstra(val speedA: Speed, val speedB: Speed, val destination: GameNode) : GenericIntDijkstra<GameNode>() {
-
-  data class GameNode(val x: Int, val y: Int) : DijkstraNode<GameNode> {
-    lateinit var game: ClawGameDijkstra
-
-    fun withGame(game: ClawGameDijkstra) = apply { this.game = game }
+    return findCost(aSpeed, bSpeed, prize)
+  }
 
-    override fun neighbors(): Map<GameNode, Int> {
-      return mutableMapOf<GameNode, Int>().apply {
-        if (x + game.speedA.x <= game.destination.x && y + game.speedA.y <= game.destination.y) {
-          put(GameNode(x + game.speedA.x, y + game.speedA.y).withGame(game), A_COST)
-        }
-        if (x + game.speedB.x <= game.destination.x && y + game.speedB.y <= game.destination.y) {
-          put(GameNode(x + game.speedB.x, y + game.speedB.y).withGame(game), B_COST)
-        }
-      }
-    }
+  private fun findCost(aSpeed: Speed, bSpeed: Speed, prize: Pair<Long, Long>): Long? {
+    val py = prize.second.toDouble()
+    val px = prize.first.toDouble()
+    val ax = aSpeed.x.toDouble()
+    val ay = aSpeed.y.toDouble()
+    val bx = bSpeed.x.toDouble()
+    val by = bSpeed.y.toDouble()
+
+    // ax*a + bx*b = px (solve for a)
+    // ... a = px/ax - bx/ax * b
+    // ay*a + by*b = py (replace a with above)
+    // ay(px/ax - bx-ax) + by*b = py (solve for b)
+    // ... b = (py - ay*(px/ax)) / (by - (ay*bx)/ax)
+    val b = ((py - ay * (px/ax)) / (by - (ay*bx)/ax)).roundToLong()
+    // replace b in original a = ...
+    val a = (px/ax - bx/ax * b).roundToLong()
+
+    // grab our new location
+    val loc = (aSpeed.x * a) + (bSpeed.x * b) to (aSpeed.y * a) + (bSpeed.y * b)
+
+    // if we're there, the system is solved!
+    return if (loc == prize) { a * A_COST + b * B_COST } else { null }
   }
 
   companion object {
+    private const val BUFFER = 10000000000000
+
     private const val A_COST = 3
     private const val B_COST = 1
   }
 }
 
-data class Speed(val x: Int, val y: Int)
+data class Speed(val x: Long, val y: Long)