Skip to content

Commit

Permalink
Solution for 2023-12-24, part 2 (Z3)
Browse files Browse the repository at this point in the history
  • Loading branch information
@pkoziol
pkoziol committed Dec 24, 2023
1 parent 3326031 commit 7726b9a
Show file tree
Hide file tree
Showing 3 changed files with 232 additions and 20 deletions.
124 changes: 109 additions & 15 deletions src/main/kotlin/biz/koziolek/adventofcode/year2023/day24/day24.kt
View file
Original file line number Diff line number Diff line change
@@ -1,6 +1,7 @@
package biz.koziolek.adventofcode.year2023.day24

import biz.koziolek.adventofcode.*
import java.time.LocalDateTime

fun main() {
val inputFile = findInput(object {})
Expand All @@ -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"
}

Expand All @@ -32,16 +35,7 @@ fun parseHails(lines: Iterable<String>): List<Hail> =
}

fun countFutureIntersections(hails: List<Hail>, testArea: Pair<LongCoord, LongCoord>): 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
Expand All @@ -50,6 +44,17 @@ fun countFutureIntersections(hails: List<Hail>, testArea: Pair<LongCoord, LongCo
&& testArea.contains(intersection.position)
}

private fun generatePairs(hails: List<Hail>): Sequence<Pair<Hail, Hail>> =
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
Expand All @@ -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(
Expand All @@ -96,3 +113,80 @@ fun findIntersection(first: Hail, second: Hail): Intersection? {
throw RuntimeException("Error while intersecting $first and $second", e)
}
}

fun findRockPosition(hails: List<Hail>, x: IntRange, y: IntRange, z: IntRange, logPrefix: String = ""): LongCoord3d {
val hailsWithDifferentVectors = generateHails(hails, x, y, z)
var index = 0L
val points = mutableListOf<LongCoord>()

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<Hail>, x: IntRange, y: IntRange, z: IntRange): Sequence<List<Hail>> =
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<Hail>): LongCoord? {
var commonIntersection: Intersection? = null
val intersections = mutableMapOf<Intersection, Int>()

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())
}
}
78 changes: 78 additions & 0 deletions src/main/kotlin/biz/koziolek/adventofcode/year2023/day24/day24part2.z3.txt
View file
Original file line number Diff line number Diff line change
@@ -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))
50 changes: 45 additions & 5 deletions src/test/kotlin/biz/koziolek/adventofcode/year2023/day24/Day24Test.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand All @@ -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
)
Expand All @@ -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)
}
}

0 comments on commit 7726b9a

Please sign in to comment.