possible z3 solution, missing per machine setup

Author: peckb1

src/main/kotlin/me/peckb/aoc/_2025/calendar/day10/Day10.kt

@@ -1,8 +1,16 @@
 package me.peckb.aoc._2025.calendar.day10
 
+import com.microsoft.z3.BitVecNum
+import com.microsoft.z3.BitVecSort
+import com.microsoft.z3.Context
+import com.microsoft.z3.Expr
+import com.microsoft.z3.Optimize
+import com.microsoft.z3.Status
 import javax.inject.Inject
 import me.peckb.aoc.generators.InputGenerator.InputGeneratorFactory
+import org.apache.commons.math3.stat.inference.TestUtils.g
 import kotlin.math.min
+import kotlin.use
 
 class Day10 @Inject constructor(
   private val generatorFactory: InputGeneratorFactory,
@@ -15,7 +23,83 @@ class Day10 @Inject constructor(
 
   fun partTwo(filename: String) = generatorFactory.forFile(filename).readAs(::day10) { input ->
     input.sumOf { machine ->
-      4
+
+      Context().use { ctx ->
+        var bestFound = Int.MAX_VALUE
+
+        val bits = 64 // the answer will fit inside a long
+
+        fun valueOf(value: Int) = ctx.mkBV(value, bits)
+
+        fun variableOf(name: String) = ctx.mkBVConst(name, bits)
+
+        infix fun Expr<BitVecSort>.equalTo(t: Expr<BitVecSort>) = ctx.mkEq(this, t)
+
+        infix fun Expr<BitVecSort>.notEqual(t: Expr<BitVecSort>) = ctx.mkNot(this equalTo t)
+
+        operator fun Expr<BitVecSort>.plus(t: Expr<BitVecSort>) = ctx.mkBVAdd(this, t)
+
+        operator fun Expr<BitVecSort>.times(t: Expr<BitVecSort>) = ctx.mkBVMul(this, t)
+
+        infix fun Expr<BitVecSort>.lessThan(t: Expr<BitVecSort>) = ctx.mkBVSLT(this, t)
+
+        infix fun Expr<BitVecSort>.gte(t: Expr<BitVecSort>) = ctx.mkBVSGE(this, t)
+
+        val a = variableOf("a")
+        val b = variableOf("b")
+        val c = variableOf("c")
+        val d = variableOf("d")
+        val e = variableOf("e")
+        val f = variableOf("f")
+
+        val optimizer = ctx.mkOptimize()
+
+        optimizer.Add(e + f equalTo valueOf(3))
+        optimizer.Add(b + f equalTo valueOf(5))
+        optimizer.Add(c + d + e equalTo valueOf(4))
+        optimizer.Add(a + b + d equalTo valueOf(7))
+//        optimizer.Add(a lessThan valueOf(10000))
+//        optimizer.Add(b lessThan valueOf(10000))
+//        optimizer.Add(c lessThan valueOf(10000))
+//        optimizer.Add(d lessThan valueOf(10000))
+//        optimizer.Add(e lessThan valueOf(10000))
+//        optimizer.Add(f lessThan valueOf(10000))
+        optimizer.Add(a gte valueOf(0))
+        optimizer.Add(b gte valueOf(0))
+        optimizer.Add(c gte valueOf(0))
+        optimizer.Add(d gte valueOf(0))
+        optimizer.Add(e gte valueOf(0))
+        optimizer.Add(f gte valueOf(0))
+
+        optimizer.MkMinimize(a + b + c + d + e + f)
+
+        optimizer.Check()
+//        while(optimizer.Check() == Status.SATISFIABLE) {
+          val model = optimizer.model
+
+          val aEval = (model.evaluate(a, true) as BitVecNum)
+          val bEval = (model.evaluate(b, true) as BitVecNum)
+          val cEval = (model.evaluate(c, true) as BitVecNum)
+          val dEval = (model.evaluate(d, true) as BitVecNum)
+          val eEval = (model.evaluate(e, true) as BitVecNum)
+          val fEval = (model.evaluate(f, true) as BitVecNum)
+
+          bestFound = min(bestFound, aEval.int + bEval.int + cEval.int + dEval.int + eEval.int + fEval.int)
+
+//          optimizer.Add(
+//            ctx.mkOr(
+//            a notEqual aEval,
+//              b notEqual bEval,
+//              c notEqual cEval,
+//              d notEqual dEval,
+//              e notEqual eEval,
+//              f notEqual fEval,
+//            )
+//          )
+//        }
+//        println(bestFound)
+        bestFound
+      }
     }
   }