Solve 2025 day 10 part 2 using Z3

Author: sim642

src/main/scala/eu/sim642/adventofcode2025/Day10.scala

@@ -1,7 +1,10 @@
 package eu.sim642.adventofcode2025
 
+import com.microsoft.z3.{ArithExpr, Context, IntExpr, IntSort, Status}
 import eu.sim642.adventofcodelib.graph.{BFS, Dijkstra, GraphSearch, TargetNode, UnitNeighbors}
 
+import scala.jdk.CollectionConverters.*
+
 object Day10 {
 
   type Lights = Vector[Boolean]
@@ -25,9 +28,19 @@ object Day10 {
 
   def sumFewestPresses(machines: Seq[Machine]): Int = machines.map(fewestPresses).sum
 
+  /*
+     x0  x1    x2  x3    x4    x5
+     (3) (1,3) (2) (2,3) (0,2) (0,1)
+  0:                     x4    x5    = 3
+  1:     x1                    x5    = 5
+  2:           x2  x3    x4          = 4
+  3: x0            x3                = 7
+
+   */
+
   // TODO: optimize
   def fewestPresses2(machine: Machine): Int = {
-    val graphSearch = new GraphSearch[Joltages] with UnitNeighbors[Joltages] with TargetNode[Joltages] {
+    /*val graphSearch = new GraphSearch[Joltages] with UnitNeighbors[Joltages] with TargetNode[Joltages] {
       override val startNode: Joltages = machine.joltages.map(_ => 0)
 
       override def unitNeighbors(joltages: Joltages): IterableOnce[Joltages] =
@@ -36,10 +49,34 @@ object Day10 {
       override val targetNode: Joltages = machine.joltages
     }
 
-    BFS.search(graphSearch).target.get._2
+    BFS.search(graphSearch).target.get._2*/
+
+    val ctx = new Context(Map("model" -> "true").asJava)
+    import ctx._
+    val s = mkOptimize()
+
+    val buttonVars = machine.buttons.zipWithIndex.map((_, i) => mkIntConst(s"x$i"))
+    val lhss =
+      machine.buttons
+        .lazyZip(buttonVars)
+        .foldLeft(machine.joltages.map[ArithExpr[IntSort]](i => mkInt(i)))({ case (accs, (button, buttonVar)) =>
+          button.foldLeft(accs)((accs, i) => accs.updated(i, mkSub(accs(i), buttonVar)))
+        })
+
+    for (lhs <- lhss)
+      s.Add(mkEq(lhs, mkInt(0)))
+
+    for (v <- buttonVars)
+      s.Add(mkGe(v, mkInt(0)))
+
+    val presses = buttonVars.foldLeft[ArithExpr[IntSort]](mkInt(0))((acc, v) => mkAdd(acc, v))
+    s.MkMinimize(presses)
+    assert(s.Check() == Status.SATISFIABLE)
+    //println(s.getModel)
+    s.getModel.evaluate(presses, false).toString.toInt
   }
 
-  def sumFewestPresses2(machines: Seq[Machine]): Int = machines.map(fewestPresses2).sum
+  def sumFewestPresses2(machines: Seq[Machine]): Int = machines.map(fewestPresses2).tapEach(println).sum
 
   def parseMachine(s: String): Machine = s match {
     case s"[$lightsStr] $buttonsStr {$joltagesStr}" =>

src/test/scala/eu/sim642/adventofcode2025/Day10Test.scala

@@ -23,6 +23,6 @@ class Day10Test extends AnyFunSuite {
   }
 
   test("Part 2 input answer") {
-    //assert(sumFewestPresses2(parseMachines(input)) == 449)
+    assert(sumFewestPresses2(parseMachines(input)) == 17848)
   }
 }