Skip to content

Commit

Permalink
2023-16 optimizer solution - refactoring
Browse files Browse the repository at this point in the history
  • Loading branch information
jurisk committed Dec 17, 2023
1 parent 1b2eaf0 commit 8a3c3cb
Show file tree
Hide file tree
Showing 6 changed files with 72 additions and 38 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,8 @@ import com.microsoft.z3.IntNum
import com.microsoft.z3.IntSort
import jurisk.geometry.Area3D
import jurisk.geometry.Coords3D
import jurisk.optimization.{abs, boolToInt}
import jurisk.optimization.abs
import jurisk.optimization.boolToInt
import jurisk.utils.FileInput._
import jurisk.utils.Parsing.StringOps

Expand Down
Original file line number Diff line number Diff line change
@@ -1,7 +1,8 @@
package jurisk.adventofcode.y2022

import cats.implicits._
import com.microsoft.z3.{Context, IntNum}
import com.microsoft.z3.Context
import com.microsoft.z3.IntNum
import jurisk.adventofcode.y2022.Advent21.Expression._
import jurisk.adventofcode.y2022.Advent21.Operation._
import jurisk.utils.FileInput._
Expand Down
78 changes: 45 additions & 33 deletions scala2/src/main/scala/jurisk/adventofcode/y2023/Advent16.scala
Original file line number Diff line number Diff line change
@@ -1,14 +1,20 @@
package jurisk.adventofcode.y2023

import cats.implicits._
import com.microsoft.z3.BoolExpr
import com.microsoft.z3.Context
import com.microsoft.z3.IntNum
import com.microsoft.z3.Status
import com.microsoft.z3.enumerations.Z3_lbool
import com.microsoft.z3.{BoolExpr, Context, IntNum, Status}
import jurisk.adventofcode.y2023.Advent16.Square.Empty
import jurisk.collections.BiMap
import jurisk.collections.BiMap.BiDirectionalArrowAssociation
import jurisk.geometry.Coords2D
import jurisk.geometry.Direction2D
import jurisk.geometry.Direction2D._
import jurisk.geometry.{Coords2D, Direction2D, Field2D}
import jurisk.optimization.{One, boolToInt}
import jurisk.geometry.Field2D
import jurisk.optimization.One
import jurisk.optimization.boolToInt
import jurisk.utils.FileInput._
import jurisk.utils.Parsing.StringOps
import jurisk.utils.Simulation
Expand Down Expand Up @@ -126,13 +132,18 @@ object Advent16 {
endState.incomingEdgesProcessed.map { case (c, _) => c }.size
}

private def solveByOptimization(
sealed trait MinimizeOrMaximize
object MinimizeOrMaximize {
case object Minimize extends MinimizeOrMaximize
case object Maximize extends MinimizeOrMaximize
}

private[y2023] def solveByOptimization(
field: Input,
initialSquare: Coords2D,
initialDirection: CardinalDirection2D,
initial: Option[(Coords2D, CardinalDirection2D)],
optimizationDirection: MinimizeOrMaximize,
debug: Boolean = false,
): Long = {
val debug = false

implicit val ctx: Context = new Context
import ctx._

Expand Down Expand Up @@ -220,18 +231,20 @@ object Advent16 {
)

// Only for Part 1 - initialSquare incoming initialDirection is 1, others are 0
o.Add(
mkEq(
incomingBool(initialSquare, initialDirection),
mkBool(true),
initial foreach { case (initialSquare, initialDirection) =>
o.Add(
mkEq(
incomingBool(initialSquare, initialDirection),
mkBool(true),
)
)
)
}

// `result` is sum of all squares which have incoming
val resultVar = mkIntConst("result")
// `energized` is sum of all squares which have incoming
val energizedVar = mkIntConst("energized")
o.Add(
mkEq(
resultVar,
energizedVar,
mkAdd(
field.allCoords.map { c =>
boolToInt(
Expand All @@ -248,25 +261,29 @@ object Advent16 {

// Note - I hoped that we can solve Part 2 in one go if we maximise, but the loops in the middle got turned on then,
// leading to results that were too high.
val objective1 = o.MkMinimize(resultVar)

val objective = optimizationDirection match {
case MinimizeOrMaximize.Minimize => o.MkMinimize(energizedVar)
case MinimizeOrMaximize.Maximize => o.MkMaximize(energizedVar)
}

if (debug) {
println(s"Optimizer: $o")
println(s"Optimizer:\n$o")
}

val status = o.Check()
assert(status == Status.SATISFIABLE)

if (debug) {
println(s"Lower: ${objective1.getLower}")
println(s"Upper: ${objective1.getUpper}")
println(s"Objective 1: $objective1")
println(s"Objective: $objective")
println(s"Lower:\n${objective.getLower}")
println(s"Upper:\n${objective.getUpper}")
}

val model = o.getModel

if (debug) {
println(s"Model: $model")
println(s"Model:\n$model")

val debugField = field
.mapByCoords { c =>
Expand Down Expand Up @@ -310,7 +327,7 @@ object Advent16 {
Field2D.printCharField(debugField)
}

val result = model.evaluate(resultVar, true)
val result = model.evaluate(energizedVar, true)
result match {
case intNum: IntNum => intNum.getInt64
case _ => s"Expected IntNum: $result".fail
Expand All @@ -329,25 +346,20 @@ object Advent16 {
solveBySimulation(field, Coords2D.Zero, Direction2D.W)

private[y2023] def part1Optimization(field: Input): Long =
solveByOptimization(field, Coords2D.Zero, Direction2D.W)
solveByOptimization(field, (Coords2D.Zero, Direction2D.W).some, MinimizeOrMaximize.Minimize)

private[y2023] def part2Helper(
field: Input,
f: (Field2D[Square], Coords2D, CardinalDirection2D) => Long,
): Long = {
private[y2023] def part2Simulation(field: Input): Long = {
val solutions = edgeIncomings(field) map {
case (initialSquare, initialDirection) =>
f(field, initialSquare, initialDirection)
solveBySimulation(field, initialSquare, initialDirection)
}

solutions.max
}

private[y2023] def part2Simulation(field: Input): Long =
part2Helper(field, solveBySimulation)

// Note - this fails due to loops being "turned on"
private[y2023] def part2Optimization(field: Input): Long =
part2Helper(field, solveByOptimization)
solveByOptimization(field, none, MinimizeOrMaximize.Maximize, debug = false)

def parseFile(fileName: String): Input =
parse(readFileText(fileName))
Expand Down
4 changes: 3 additions & 1 deletion scala2/src/main/scala/jurisk/geometry/Field2D.scala
Original file line number Diff line number Diff line change
@@ -1,6 +1,8 @@
package jurisk.geometry

import cats.{Eval, Foldable, Functor}
import cats.Eval
import cats.Foldable
import cats.Functor
import cats.implicits._
import jurisk.algorithms.pathfinding.Bfs
import jurisk.collections.BiMap
Expand Down
6 changes: 5 additions & 1 deletion scala2/src/main/scala/jurisk/optimization/package.scala
Original file line number Diff line number Diff line change
@@ -1,6 +1,10 @@
package jurisk

import com.microsoft.z3.{BoolSort, Context, Expr, IntNum, IntSort}
import com.microsoft.z3.BoolSort
import com.microsoft.z3.Context
import com.microsoft.z3.Expr
import com.microsoft.z3.IntNum
import com.microsoft.z3.IntSort

package object optimization {
def Zero(implicit ctx: Context): IntNum = ctx.mkInt(0)
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -2,12 +2,24 @@ package jurisk.adventofcode.y2023

import org.scalatest.freespec.AnyFreeSpec
import Advent16._
import cats.implicits._
import jurisk.geometry.{Coords2D, Direction2D}
import org.scalatest.matchers.should.Matchers._

class Advent16Spec extends AnyFreeSpec {
private val testData: Input = parseFile("2023/16-test.txt")
private val realData: Input = parseFile("2023/16.txt")

"solveByOptimization - simple maximization test that fails due to a loop" ignore {
val test = parse(
"""/-
|/|
|\/
|""".stripMargin)

solveByOptimization(test, (Coords2D.Zero, Direction2D.W).some, MinimizeOrMaximize.Maximize, debug = true) shouldEqual 1
}

"part 1" - {
val TestAnswer = 46
val RealAnswer = 7415
Expand Down Expand Up @@ -48,7 +60,9 @@ class Advent16Spec extends AnyFreeSpec {
}

"optimize" - {
"test" in {
// One-pass Part 2 using optimization doesn't work (see other comments and the failing test)

"test" ignore {
part2Optimization(testData) shouldEqual TestAnswer
}

Expand Down

0 comments on commit 8a3c3cb

Please sign in to comment.