Skip to content

Commit 7024da9

Browse files
peckb1peckb1
committed
Z3 implementation using ints
1 parent 269bf2d commit 7024da9

File tree

3 files changed

+62
-95
lines changed

3 files changed

+62
-95
lines changed

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

Lines changed: 60 additions & 93 deletions
Original file line numberDiff line numberDiff line change
@@ -1,111 +1,80 @@
11
package me.peckb.aoc._2025.calendar.day10
22

3-
import com.microsoft.z3.BitVecNum
4-
import com.microsoft.z3.BitVecSort
3+
import com.microsoft.z3.ArithExpr
54
import com.microsoft.z3.Context
6-
import com.microsoft.z3.Expr
7-
import com.microsoft.z3.Optimize
5+
import com.microsoft.z3.IntExpr
6+
import com.microsoft.z3.IntNum
7+
import com.microsoft.z3.IntSort
88
import com.microsoft.z3.Status
99
import javax.inject.Inject
1010
import me.peckb.aoc.generators.InputGenerator.InputGeneratorFactory
11-
import org.apache.commons.math3.stat.inference.TestUtils.g
11+
import kotlin.collections.component1
12+
import kotlin.collections.component2
1213
import kotlin.math.min
13-
import kotlin.use
1414

1515
class Day10 @Inject constructor(
1616
private val generatorFactory: InputGeneratorFactory,
1717
) {
1818
fun partOne(filename: String) = generatorFactory.forFile(filename).readAs(::day10) { input ->
19-
input.sumOf { machine ->
20-
thing(".".repeat(machine.indicatorLights.length), machine.indicatorLights, machine.buttonSchematics)
21-
}
19+
input.sumOf { machine -> flipLights(machine.indicatorLights, machine.buttonSchematics) }
2220
}
2321

2422
fun partTwo(filename: String) = generatorFactory.forFile(filename).readAs(::day10) { input ->
25-
input.sumOf { machine ->
26-
27-
Context().use { ctx ->
28-
var bestFound = Int.MAX_VALUE
29-
30-
val bits = 64 // the answer will fit inside a long
31-
32-
fun valueOf(value: Int) = ctx.mkBV(value, bits)
33-
34-
fun variableOf(name: String) = ctx.mkBVConst(name, bits)
35-
36-
infix fun Expr<BitVecSort>.equalTo(t: Expr<BitVecSort>) = ctx.mkEq(this, t)
37-
38-
infix fun Expr<BitVecSort>.notEqual(t: Expr<BitVecSort>) = ctx.mkNot(this equalTo t)
39-
40-
operator fun Expr<BitVecSort>.plus(t: Expr<BitVecSort>) = ctx.mkBVAdd(this, t)
41-
42-
operator fun Expr<BitVecSort>.times(t: Expr<BitVecSort>) = ctx.mkBVMul(this, t)
43-
44-
infix fun Expr<BitVecSort>.lessThan(t: Expr<BitVecSort>) = ctx.mkBVSLT(this, t)
45-
46-
infix fun Expr<BitVecSort>.gte(t: Expr<BitVecSort>) = ctx.mkBVSGE(this, t)
47-
48-
val a = variableOf("a")
49-
val b = variableOf("b")
50-
val c = variableOf("c")
51-
val d = variableOf("d")
52-
val e = variableOf("e")
53-
val f = variableOf("f")
54-
55-
val optimizer = ctx.mkOptimize()
56-
57-
optimizer.Add(e + f equalTo valueOf(3))
58-
optimizer.Add(b + f equalTo valueOf(5))
59-
optimizer.Add(c + d + e equalTo valueOf(4))
60-
optimizer.Add(a + b + d equalTo valueOf(7))
61-
// optimizer.Add(a lessThan valueOf(10000))
62-
// optimizer.Add(b lessThan valueOf(10000))
63-
// optimizer.Add(c lessThan valueOf(10000))
64-
// optimizer.Add(d lessThan valueOf(10000))
65-
// optimizer.Add(e lessThan valueOf(10000))
66-
// optimizer.Add(f lessThan valueOf(10000))
67-
optimizer.Add(a gte valueOf(0))
68-
optimizer.Add(b gte valueOf(0))
69-
optimizer.Add(c gte valueOf(0))
70-
optimizer.Add(d gte valueOf(0))
71-
optimizer.Add(e gte valueOf(0))
72-
optimizer.Add(f gte valueOf(0))
73-
74-
optimizer.MkMinimize(a + b + c + d + e + f)
75-
76-
optimizer.Check()
77-
// while(optimizer.Check() == Status.SATISFIABLE) {
78-
val model = optimizer.model
79-
80-
val aEval = (model.evaluate(a, true) as BitVecNum)
81-
val bEval = (model.evaluate(b, true) as BitVecNum)
82-
val cEval = (model.evaluate(c, true) as BitVecNum)
83-
val dEval = (model.evaluate(d, true) as BitVecNum)
84-
val eEval = (model.evaluate(e, true) as BitVecNum)
85-
val fEval = (model.evaluate(f, true) as BitVecNum)
86-
87-
bestFound = min(bestFound, aEval.int + bEval.int + cEval.int + dEval.int + eEval.int + fEval.int)
88-
89-
// optimizer.Add(
90-
// ctx.mkOr(
91-
// a notEqual aEval,
92-
// b notEqual bEval,
93-
// c notEqual cEval,
94-
// d notEqual dEval,
95-
// e notEqual eEval,
96-
// f notEqual fEval,
97-
// )
98-
// )
99-
// }
100-
// println(bestFound)
101-
bestFound
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")
10272
}
10373
}
10474
}
10575

106-
107-
fun thing(current: String, goal: String, buttonSchematics: List<ButtonSchematic>): Long {
108-
val minPressesForState = mutableMapOf(current to 0L)
76+
fun flipLights(goal: String, buttonSchematics: List<ButtonSchematic>): Long {
77+
val minPressesForState = mutableMapOf(".".repeat(goal.length) to 0L)
10978
while(!minPressesForState.containsKey(goal)) {
11079
minPressesForState.entries.toList().forEach { (light, cost) ->
11180
val nextStates = possibleLights(light, buttonSchematics)
@@ -128,7 +97,7 @@ class Day10 @Inject constructor(
12897

12998
private fun applyLightPress(current: String, buttonSchematic: ButtonSchematic): String {
13099
return current.mapIndexed { index, c ->
131-
if (buttonSchematic.lightsAffected.contains(index)) {
100+
if (buttonSchematic.affectedIndices.contains(index)) {
132101
if (c == '#') { '.' } else { '#' }
133102
} else { c }
134103
}.joinToString("")
@@ -153,6 +122,4 @@ data class Machine(
153122
val joltages: List<Int>,
154123
)
155124

156-
/** zero indexed */
157-
// TODO rename
158-
data class ButtonSchematic(val lightsAffected: List<Int>)
125+
data class ButtonSchematic(val affectedIndices: List<Int>)

‎src/main/kotlin/me/peckb/aoc/_2025/calendar/day10/README.md‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
## [](https://adventofcode.com/2025/day/10)
1+
## [Day 10: Factory](https://adventofcode.com/2025/day/10)

‎src/test/kotlin/me/peckb/aoc/_2025/calendar/day10/Day10Test.kt‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -23,7 +23,7 @@ internal class Day10Test {
2323

2424
@Test
2525
fun testDay10PartTwo() {
26-
assertEquals(-1, day10.partTwo(DAY_10))
26+
assertEquals(19810, day10.partTwo(DAY_10))
2727
}
2828

2929
companion object {

0 commit comments

Comments
 (0)