From 7726b9aa94f9c03cdc9915788a757721d1112c59 Mon Sep 17 00:00:00 2001 From: koziolek Date: Sun, 24 Dec 2023 17:47:05 +0100 Subject: [PATCH] Solution for 2023-12-24, part 2 (Z3) --- .../adventofcode/year2023/day24/day24.kt | 124 +++++++++++++++--- .../year2023/day24/day24part2.z3.txt | 78 +++++++++++ .../adventofcode/year2023/day24/Day24Test.kt | 50 ++++++- 3 files changed, 232 insertions(+), 20 deletions(-) create mode 100644 src/main/kotlin/biz/koziolek/adventofcode/year2023/day24/day24part2.z3.txt diff --git a/src/main/kotlin/biz/koziolek/adventofcode/year2023/day24/day24.kt b/src/main/kotlin/biz/koziolek/adventofcode/year2023/day24/day24.kt index a3277ad..9a6c7ce 100644 --- a/src/main/kotlin/biz/koziolek/adventofcode/year2023/day24/day24.kt +++ b/src/main/kotlin/biz/koziolek/adventofcode/year2023/day24/day24.kt @@ -1,6 +1,7 @@ package biz.koziolek.adventofcode.year2023.day24 import biz.koziolek.adventofcode.* +import java.time.LocalDateTime fun main() { val inputFile = findInput(object {}) @@ -10,7 +11,9 @@ fun main() { val testArea = LongCoord(200_000_000_000_000, 200_000_000_000_000) to LongCoord(400_000_000_000_000, 400_000_000_000_000) -data class Hail(val position: LongCoord3d, val velocity: Coord3d, val time: Long = 1) { +data class Hail(val position: LongCoord3d, + val velocity: Coord3d, + val velocityDelta: Coord3d = Coord3d(0, 0, 0)) { override fun toString() = "$position @ $velocity" } @@ -32,16 +35,7 @@ fun parseHails(lines: Iterable): List = } fun countFutureIntersections(hails: List, testArea: Pair): Int = - hails - .flatMapIndexed { index1, hail1 -> - hails.mapIndexedNotNull { index2, hail2 -> - if (index2 > index1) { - hail1 to hail2 - } else { - null - } - } - } + generatePairs(hails) .count { (hail1, hail2) -> val intersection = findIntersection(hail1, hail2) intersection != null @@ -50,6 +44,17 @@ fun countFutureIntersections(hails: List, testArea: Pair): Sequence> = + sequence { + hails.forEachIndexed { index1, hail1 -> + hails.forEachIndexed { index2, hail2 -> + if (index2 > index1) { + yield(hail1 to hail2) + } + } + } + } + fun findIntersection(first: Hail, second: Hail): Intersection? { // x1 + vx1 * time = x2 + vx2 * time // y1 + vy1 * time = y2 + vy2 * time @@ -66,19 +71,31 @@ fun findIntersection(first: Hail, second: Hail): Intersection? { // a1x + b1 = a2x + b2 // x = (b1 - b2) / (a2 - a1) + // x1 + vx1 * time1 = x + vx * time1 + // y1 + vy1 * time1 = y + vy * time1 + // z1 + vz1 * time1 = z + vz * time1 + + // x2 + vx2 * time2 = x + vx * time2 + // y2 + vy2 * time2 = y + vy * time2 + // z2 + vz2 * time2 = z + vz * time2 + + // x3 + vx3 * time3 = x + vx * time3 + // y3 + vy3 * time3 = y + vy * time3 + // z3 + vz3 * time3 = z + vz * time3 + try { // val timeX = (first.position.x.toDouble() - second.position.x) / (second.velocity.x.toDouble() - first.velocity.x) // val timeY = (first.position.y.toDouble() - second.position.y) / (second.velocity.y.toDouble() - first.velocity.y) - val a1 = first.velocity.y / first.velocity.x.toDouble() + val a1 = (first.velocity.y + first.velocityDelta.y) / (first.velocity.x.toDouble() + first.velocityDelta.x) val b1 = first.position.y - a1 * first.position.x - val a2 = second.velocity.y / second.velocity.x.toDouble() + val a2 = (second.velocity.y + second.velocityDelta.y) / (second.velocity.x.toDouble() + second.velocityDelta.x) val b2 = second.position.y - a2 * second.position.x val x = (b1 - b2) / (a2 - a1) val y = a1 * x + b1 - val time1 = (x - first.position.x) / first.velocity.x.toDouble() - val time2 = (x - second.position.x) / second.velocity.x.toDouble() + val time1 = (x - first.position.x) / (first.velocity.x.toDouble() + first.velocityDelta.x) + val time2 = (x - second.position.x) / (second.velocity.x.toDouble() + second.velocityDelta.x) return if (x.isFinite() && y.isFinite()) { Intersection( @@ -96,3 +113,80 @@ fun findIntersection(first: Hail, second: Hail): Intersection? { throw RuntimeException("Error while intersecting $first and $second", e) } } + +fun findRockPosition(hails: List, x: IntRange, y: IntRange, z: IntRange, logPrefix: String = ""): LongCoord3d { + val hailsWithDifferentVectors = generateHails(hails, x, y, z) + var index = 0L + val points = mutableListOf() + + for (newHails in hailsWithDifferentVectors) { + val point = findCommonIntersectsXY(newHails) + + if (index % 999_000_000 == 0L) { + println("${logPrefix}%,12d @ %s".format(index, LocalDateTime.now())) + } + + if (point != null) { + println("${logPrefix}Found $point at $index for dv = ${newHails.first().velocityDelta}") + points.add(point) + } + + index++ + } + + // TODO choose Z that matches + + println("${logPrefix}%,12d @ %s".format(index, LocalDateTime.now())) + + return LongCoord3d(0, 0, 0) +} + +private fun generateHails(hails: List, x: IntRange, y: IntRange, z: IntRange): Sequence> = + sequence { + for (xx in x) { + for (yy in y) { + for (zz in z) { + yield(Coord3d(xx, yy, zz)) + } + } + } + } +// .sortedBy { it.distanceTo(Coord3d(0, 0, 0)) } + .map { delta -> + hails.map { + Hail( + position = it.position, + velocity = it.velocity, + velocityDelta = delta + ) + } + } + +private fun findCommonIntersectsXY(hails: List): LongCoord? { + var commonIntersection: Intersection? = null + val intersections = mutableMapOf() + + for ((hail1, hail2) in generatePairs(hails)) { + val intersection = findIntersection(hail1, hail2) + if (intersection == null) { + continue + } + + intersections.compute(intersection) { _, v -> v?.plus(1) ?: 1 } + + if (commonIntersection == null) { + commonIntersection = intersection + } else { + // x = 354954946036320 + // y = 318916597757112 + // z = 112745502066835 + if (commonIntersection.position.distanceTo(intersection.position) > 1) { + return null + } + } + } + + return commonIntersection?.position?.let { + LongCoord(it.x.toLong(), it.y.toLong()) + } +} diff --git a/src/main/kotlin/biz/koziolek/adventofcode/year2023/day24/day24part2.z3.txt b/src/main/kotlin/biz/koziolek/adventofcode/year2023/day24/day24part2.z3.txt new file mode 100644 index 0000000..2b7a30b --- /dev/null +++ b/src/main/kotlin/biz/koziolek/adventofcode/year2023/day24/day24part2.z3.txt @@ -0,0 +1,78 @@ +(declare-const x1 Int) +(declare-const y1 Int) +(declare-const z1 Int) +(declare-const vx1 Int) +(declare-const vy1 Int) +(declare-const vz1 Int) + +(declare-const x2 Int) +(declare-const y2 Int) +(declare-const z2 Int) +(declare-const vx2 Int) +(declare-const vy2 Int) +(declare-const vz2 Int) + +(declare-const x3 Int) +(declare-const y3 Int) +(declare-const z3 Int) +(declare-const vx3 Int) +(declare-const vy3 Int) +(declare-const vz3 Int) + +(declare-const x Int) +(declare-const y Int) +(declare-const z Int) +(declare-const vx Int) +(declare-const vy Int) +(declare-const vz Int) +(declare-const time1 Int) +(declare-const time2 Int) +(declare-const time3 Int) + +(declare-const ans Int) + +(assert (= x1 327367788702047)) +(assert (= y1 294752664325632)) +(assert (= z1 162080199489440)) +(assert (= vx1 20)) +(assert (= vy1 51)) +(assert (= vz1 36)) + +(assert (= x2 349323332347395)) +(assert (= y2 429135322811787)) +(assert (= z2 397812423558610)) +(assert (= vx2 -96)) +(assert (= vy2 -480)) +(assert (= vz2 -782)) + +(assert (= x3 308103110384633)) +(assert (= y3 244954649487980)) +(assert (= z3 207561383118617)) +(assert (= vx3 220)) +(assert (= vy3 463)) +(assert (= vz3 -401)) + +(assert (= (+ x1 (* vx1 time1)) (+ x (* vx time1)))) +(assert (= (+ y1 (* vy1 time1)) (+ y (* vy time1)))) +(assert (= (+ z1 (* vz1 time1)) (+ z (* vz time1)))) +(assert (> time1 0)) + +(assert (= (+ x2 (* vx2 time2)) (+ x (* vx time2)))) +(assert (= (+ y2 (* vy2 time2)) (+ y (* vy time2)))) +(assert (= (+ z2 (* vz2 time2)) (+ z (* vz time2)))) +(assert (> time2 0)) + +(assert (= (+ x3 (* vx3 time3)) (+ x (* vx time3)))) +(assert (= (+ y3 (* vy3 time3)) (+ y (* vy time3)))) +(assert (= (+ z3 (* vz3 time3)) (+ z (* vz time3)))) +(assert (> time3 0)) + +(assert (= ans (+ x (+ y z)))) + +(check-sat) +(get-objectives) +(get-model) +(get-value (vx)) +(get-value (vy)) +(get-value (vz)) +(get-value (ans)) diff --git a/src/test/kotlin/biz/koziolek/adventofcode/year2023/day24/Day24Test.kt b/src/test/kotlin/biz/koziolek/adventofcode/year2023/day24/Day24Test.kt index bfac66b..b13982f 100644 --- a/src/test/kotlin/biz/koziolek/adventofcode/year2023/day24/Day24Test.kt +++ b/src/test/kotlin/biz/koziolek/adventofcode/year2023/day24/Day24Test.kt @@ -5,6 +5,7 @@ import biz.koziolek.adventofcode.LongCoord import biz.koziolek.adventofcode.LongCoord3d import biz.koziolek.adventofcode.findInput import org.junit.jupiter.api.Assertions.* +import org.junit.jupiter.api.Disabled import org.junit.jupiter.api.Tag import org.junit.jupiter.api.Test @@ -26,11 +27,11 @@ internal class Day24Test { val hails = parseHails(sampleInput) assertEquals( listOf( - Hail(position = LongCoord3d(19, 13, 30), velocity = Coord3d(-2, 1, -2), time = 1), - Hail(position = LongCoord3d(18, 19, 22), velocity = Coord3d(-1, -1, -2), time = 1), - Hail(position = LongCoord3d(20, 25, 34), velocity = Coord3d(-2, -2, -4), time = 1), - Hail(position = LongCoord3d(12, 31, 28), velocity = Coord3d(-1, -2, -1), time = 1), - Hail(position = LongCoord3d(20, 19, 15), velocity = Coord3d(1, -5, -3), time = 1), + Hail(position = LongCoord3d(19, 13, 30), velocity = Coord3d(-2, 1, -2)), + Hail(position = LongCoord3d(18, 19, 22), velocity = Coord3d(-1, -1, -2)), + Hail(position = LongCoord3d(20, 25, 34), velocity = Coord3d(-2, -2, -4)), + Hail(position = LongCoord3d(12, 31, 28), velocity = Coord3d(-1, -2, -1)), + Hail(position = LongCoord3d(20, 19, 15), velocity = Coord3d(1, -5, -3)), ), hails ) @@ -49,4 +50,43 @@ internal class Day24Test { val hails = parseHails(input) assertEquals(28266, countFutureIntersections(hails, testArea = testArea)) } + + @Test + @Disabled("Not finished - doesn't actually find the answer") + fun testSampleAnswer2() { + val hails = parseHails(sampleInput) + val rockPosition = findRockPosition(hails, x = -10..10, y = -10..10, z = -10..0) + assertEquals(LongCoord3d(24, 13, 10), rockPosition) + assertEquals(47, rockPosition.x + rockPosition.y + rockPosition.z) + } + + @Test + @Disabled("Not finished - doesn't actually find the answer") + fun testAnswer2b() { + val input = findInput(object {}).bufferedReader().readLines() + val hails = parseHails(input) + +// val executor = Executors.newFixedThreadPool(Runtime.getRuntime().availableProcessors()) +// +// for (x in listOf(-2000, -1500, -1000, -500, 0, 500, 1000, 1500)) { +// for (y in listOf(-2000, -1500, -1000, -500, 0, 500, 1000, 1500)) { +// for (z in listOf(-2000, -1500, -1000, -500, 0, 500, 1000, 1500)) { +// executor.execute { +// findRockPosition( +// hails, +// logPrefix = "%+5d/%+5d/%+5d: ".format(x, y, z), +// x = x..(x + 500), +// y = y..(y + 500), +// z = z..(z + 500), +// ) +// } +// } +// } +// } +// executor.shutdown() +// executor.awaitTermination(1, TimeUnit.DAYS) + + val rockPosition = findRockPosition(hails, x = -117..-117, y = -69..-69, z = 281..281) + assertEquals(786617045860267L, rockPosition.x + rockPosition.y + rockPosition.z) + } }