@@ -3,6 +3,7 @@ package eu.sim642.adventofcode2025
33import com .microsoft .z3 .{ArithExpr , Context , IntExpr , IntSort , Status }
44import eu .sim642 .adventofcodelib .graph .{BFS , Dijkstra , GraphSearch , TargetNode , UnitNeighbors }
55
6+ import scala .collection .mutable
67import scala .jdk .CollectionConverters .*
78
89object Day10 {
@@ -59,15 +60,6 @@ object Day10 {
5960 * Solution, which finds fewest presses via an ILP problem, solved by Z3.
6061 */
6162 object Z3Part2Solution extends Part2Solution {
62- /*
63- x0 x1 x2 x3 x4 x5
64- (3) (1,3) (2) (2,3) (0,2) (0,1)
65- 0: x4 x5 = 3
66- 1: x1 x5 = 5
67- 2: x2 x3 x4 = 4
68- 3: x0 x1 x3 = 7
69- */
70-
7163 override def fewestPresses (machine : Machine ): Int = {
7264 val ctx = new Context (Map (" model" -> " true" ).asJava)
7365 import ctx ._
@@ -93,6 +85,103 @@ object Day10 {
9385 }
9486 }
9587
88+ object GaussianEliminationPart2Solution extends Part2Solution {
89+ /*
90+ x0 x1 x2 x3 x4 x5
91+ (3) (1,3) (2) (2,3) (0,2) (0,1)
92+ 0: x4 x5 = 3
93+ 1: x1 x5 = 5
94+ 2: x2 x3 x4 = 4
95+ 3: x0 x1 x3 = 7
96+
97+
98+ 0 0 0 0 1 1 | 3
99+ 0 1 0 0 0 1 | 5
100+ 0 0 1 1 1 0 | 4
101+ 1 1 0 1 0 0 | 7
102+
103+ 1 1 0 1 0 0 | 7
104+ 0 1 0 0 0 1 | 5
105+ 0 0 1 1 1 0 | 4
106+ 0 0 0 0 1 1 | 3
107+
108+ 1 0 0 1 0 -1 | 2
109+ 0 1 0 0 0 1 | 5
110+ 0 0 1 1 0 -1 | 1
111+ 0 0 0 0 1 1 | 3
112+
113+ 1 1 1 2 1 0 | 11
114+ -1 1 | ?
115+ */
116+
117+ override def fewestPresses (machine : Machine ): Int = {
118+ val zeroCol = machine.joltages.map(_ => 0 )
119+ val rows =
120+ machine.buttons
121+ .map(button =>
122+ button.foldLeft(zeroCol)((acc, i) => acc.updated(i, 1 ))
123+ )
124+ .transpose
125+ .zip(machine.joltages)
126+
127+ val m = rows.map((a, b) => (a :+ b).to(mutable.ArraySeq )).to(mutable.ArraySeq )
128+
129+ def swapRows (y1 : Int , y2 : Int ): Unit = {
130+ val row1 = m(y1)
131+ m(y1) = m(y2)
132+ m(y2) = row1
133+ }
134+
135+ def reduceDown (x : Int , y1 : Int , y2 : Int ): Unit = {
136+ val factor = m(y2)(x) / m(y1)(x)
137+ for (x2 <- x until (machine.buttons.size + 1 ))
138+ m(y2)(x2) -= factor * m(y1)(x2)
139+ }
140+
141+ def reduceUp (x : Int , y1 : Int , y2 : Int ): Unit = {
142+ val factor = m(y2)(x) / m(y1)(x)
143+ for (x2 <- 0 until (machine.buttons.size + 1 )) // TODO: enough to also start from x? (before zeros anyway)
144+ m(y2)(x2) -= factor * m(y1)(x2)
145+ }
146+
147+ var y = 0
148+ for (x <- machine.buttons.indices) {
149+ val y2opt = m.indices.find(y2 => y2 >= y && m(y2)(x) != 0 )
150+ y2opt match {
151+ case None => // move to next x
152+ case Some (y2) =>
153+ swapRows(y, y2)
154+ assert(m(y)(x) == 1 ) // TODO: this will probably change
155+
156+ for (y3 <- (y + 1 ) until m.size)
157+ reduceDown(x, y, y3)
158+
159+ y += 1
160+ }
161+ }
162+
163+ // check consistency
164+ for (y2 <- y until m.size)
165+ assert(m(y2).last == 0 )
166+
167+ y = 0
168+ for (x <- machine.buttons.indices) {
169+ if (y < m.size) { // TODO: break if y too big
170+ if (m(y)(x) == 0 )
171+ () // move to next x
172+ else {
173+ for (y3 <- 0 until y)
174+ reduceUp(x, y, y3)
175+
176+ y += 1
177+ }
178+ }
179+ }
180+
181+ ???
182+ }
183+ }
184+
96185 def parseMachine (s : String ): Machine = s match {
97186 case s " [ $lightsStr] $buttonsStr { $joltagesStr} " =>
98187 val lights = lightsStr.map(_ == '#' ).toVector
0 commit comments