11package eu .sim642 .adventofcode2025
22
3- import eu .sim642 .adventofcodelib .IteratorImplicits ._
4-
3+ import eu .sim642 .adventofcodelib .IteratorImplicits .*
54import com .microsoft .z3 .{ArithExpr , Context , IntExpr , IntSort , Status }
5+ import eu .sim642 .adventofcodelib .NumberTheory
66import eu .sim642 .adventofcodelib .graph .{BFS , Dijkstra , GraphSearch , TargetNode , UnitNeighbors }
77
88import scala .collection .mutable
@@ -117,24 +117,35 @@ object Day10 {
117117 */
118118
119119 override def fewestPresses (machine : Machine ): Int = {
120- val zeroCol = machine.joltages.map(_ => 0 )
120+ val zeroCol = machine.joltages.map(_ => 0L )
121121 val rows =
122122 machine.buttons
123123 .map(button =>
124- button.foldLeft(zeroCol)((acc, i) => acc.updated(i, 1 ))
124+ button.foldLeft(zeroCol)((acc, i) => acc.updated(i, 1L ))
125125 )
126126 .transpose
127- .zip(machine.joltages)
127+ .zip(machine.joltages.map(_.toLong) )
128128
129- val m = rows.map((a, b) => (a :+ b).to(mutable.ArraySeq )).to(mutable.ArraySeq )
129+ val m : mutable. ArraySeq [mutable. ArraySeq [ Long ]] = rows.map((a, b) => (a :+ b).to(mutable.ArraySeq )).to(mutable.ArraySeq )
130130
131131 def swapRows (y1 : Int , y2 : Int ): Unit = {
132132 val row1 = m(y1)
133133 m(y1) = m(y2)
134134 m(y2) = row1
135135 }
136136
137+ def multiplyRow (y : Int , factor : Long ): Unit = {
138+ for (x2 <- 0 until (machine.buttons.size + 1 ))
139+ m(y)(x2) *= factor.toLong
140+ }
141+
137142 def reduceDown (x : Int , y1 : Int , y2 : Int ): Unit = {
143+ val c1 = m(y1)(x)
144+ assert(c1 > 0 )
145+ val c2 = m(y2)(x)
146+ val cd = NumberTheory .lcm(c1, c2.abs)
147+ multiplyRow(y1, cd / c1)
148+ multiplyRow(y2, cd / c2)
138149 val factor = m(y2)(x) / m(y1)(x)
139150 for (x2 <- x until (machine.buttons.size + 1 ))
140151 m(y2)(x2) -= factor * m(y1)(x2)
@@ -153,10 +164,13 @@ object Day10 {
153164 case None => // move to next x
154165 case Some (y2) =>
155166 swapRows(y, y2)
156- assert(m(y)(x) == 1 ) // TODO: this will probably change
167+ multiplyRow(y, m(y)(x).sign) // make leading coeff positive
168+ // assert(m(y)(x).abs == 1) // TODO: this will probably change
157169
158- for (y3 <- (y + 1 ) until m.size)
159- reduceDown(x, y, y3)
170+ for (y3 <- (y + 1 ) until m.size) {
171+ if (m(y3)(x) != 0 )
172+ reduceDown(x, y, y3)
173+ }
160174
161175 y += 1
162176 }
@@ -177,8 +191,12 @@ object Day10 {
177191 } // move to next x
178192 else {
179193 mainVars += x
180- for (y3 <- 0 until y)
181- reduceUp(x, y, y3)
194+ multiplyRow(y, m(y)(x).sign) // make leading coeff positive
195+ for (y3 <- 0 until y) {
196+ if (m(y3)(x) != 0 )
197+ // reduceUp(x, y, y3)
198+ reduceDown(x, y, y3)
199+ }
182200
183201 y += 1
184202 }
@@ -187,6 +205,8 @@ object Day10 {
187205 freeVars += x // can't break if this is here
188206 }
189207
208+ // val mSum = m.transpose.map(_.sum) // TODO: use?
209+
190210 def helper0 (sum : Int , len : Int ): Iterator [List [Int ]] = {
191211 if (len == 0 )
192212 Iterator (Nil )
@@ -200,22 +220,39 @@ object Day10 {
200220 }
201221 }
202222
203- val choices = Iterator .from(0 ).flatMap(helper0(_, freeVars.size))
223+ def eval (freeVals : List [Int ]): List [Long ] = {
224+ val mainVals = mainVars.view.zipWithIndex.map((mainVar, y) => {
225+ val row = m(y)
226+ val r = row.last - (freeVars lazyZip freeVals).map((freeVar, freeVal) => row(freeVar) * freeVal).sum
227+ if (r % row(mainVar) == 0 )
228+ r / row(mainVar)
229+ else
230+ - 1
231+ }).toList
232+ mainVals
233+ }
234+
235+ // TODO: avoid double search...
236+ val bound =
237+ Iterator .from(0 )
238+ .flatMap(helper0(_, freeVars.size))
239+ .map(freeVals => (eval(freeVals), freeVals))
240+ .filter(_._1.forall(_ >= 0 )) // all main vals must be non-negative
241+ .map((s1, s2) => s1.sum + s2.sum)
242+ .head
243+ val choices = (0 to bound.toInt).iterator.flatMap(helper0(_, freeVars.size))
244+
204245 val answer =
205246 choices
206- .map(freeVals => {
207- val mainVals = mainVars.view.zipWithIndex.map((mainVar, y) => {
208- val row = m(y)
209- row.last - (freeVars lazyZip freeVals).map((freeVar, freeVal) => row(freeVar) * freeVal).sum
210- }).toList
211- (mainVals, freeVals)
212- })
247+ .map(freeVals => (eval(freeVals), freeVals))
248+ // .take(1000) // TODO: when to stop?
249+ // .tapEach(println)
213250 .filter(_._1.forall(_ >= 0 )) // all main vals must be non-negative
214251 .map((s1, s2) => s1.sum + s2.sum)
215- .head // TODO: wrong, freeVals sum is minimal, but mainVals sum isn't
252+ .min // TODO: wrong, freeVals sum is minimal, but mainVals sum isn't
216253
217254 println(answer)
218- answer
255+ answer.toInt
219256 }
220257 }
221258
0 commit comments