Solve 2025-10, add z3 solver

2025/10/2025-10.run.xml

@@ -0,0 +1,7 @@
+<component name="ProjectRunConfigurationManager">
+  <configuration default="false" name="2025-10" type="BunRunConfiguration">
+    <option name="program" value="2025/10/run.ts" />
+    <option name="workingDirectory" value="$PROJECT_DIR$" />
+    <method v="2" />
+  </configuration>
+</component>

2025/10/index.test.ts

@@ -0,0 +1,11 @@
+import { describe, expect, it } from 'bun:test';
+import { solveFirst } from './index.ts';
+
+describe('2025-10', () => {
+  const testInput = `[.##.] (3) (1,3) (2) (2,3) (0,2) (0,1) {3,5,4,7}
+[...#.] (0,2,3,4) (2,3) (0,4) (0,1,2) (1,2,3,4) {7,5,12,7,2}
+[.###.#] (0,1,2,3,4) (0,3,4) (0,1,2,4,5) (1,2) {10,11,11,5,10,5}`;
+  it('first', () => {
+    expect(solveFirst(testInput)).toBe(7);
+  });
+});

2025/10/index.ts

@@ -0,0 +1,58 @@
+import { sumArray } from '../../utils/array.ts';
+
+type Indicators = boolean[];
+export function parseInput(input: string) {
+  return input.split('\n').map((row) => {
+    const buttons = row.split(' ').map((p) => p.substring(1, p.length - 1));
+    const indicators = buttons
+      .splice(0, 1)[0]
+      .split('')
+      .map((d) => d === '#') as Indicators;
+    const joltage = buttons.splice(-1, 1)[0].split(',').map(Number);
+
+    return {
+      buttons: buttons.map((btns) => btns.split(',').map(Number)),
+      indicators,
+      joltage
+    };
+  });
+}
+
+export function solveFirst(input: string): number {
+  const machines = parseInput(input);
+  const steps = machines.map(({ buttons, indicators }) => {
+    const start = new Array(indicators.length).fill(false) as Indicators;
+    const queue = [[start, 0] as [Indicators, number]];
+    const visited = new Set<string>();
+
+    const goal = toStr(indicators);
+
+    while (queue.length > 0) {
+      const [state, step] = queue.shift()!;
+      const stateStr = toStr(state);
+      if (stateStr === goal) {
+        return step;
+      }
+      if (visited.has(stateStr)) {
+        continue;
+      }
+      visited.add(stateStr);
+      buttons.forEach((button) => {
+        const alteration = [...state];
+        button.forEach((b) => (alteration[b] = !alteration[b]));
+        if (visited.has(toStr(alteration))) {
+          return;
+        }
+        queue.push([alteration, step + 1]);
+      });
+    }
+
+    return 0;
+  });
+
+  return sumArray(steps);
+}
+
+function toStr(state: Indicators) {
+  return state.map((v) => (v ? '#' : '.')).join();
+}

2025/10/part2.ts

@@ -0,0 +1,57 @@
+import { type Arith, init } from 'z3-solver';
+
+import { readFile } from 'fs/promises';
+import { dirname, join } from 'path';
+import { fileURLToPath } from 'url';
+import { parseInput } from './index.ts';
+
+if (globalThis.Bun !== undefined) {
+  console.error('This only runs with node!');
+  process.exit(1);
+}
+
+const data = await readFile(
+  join(dirname(fileURLToPath(import.meta.url)), 'input.txt'),
+  'utf8'
+);
+const cleanData = parseInput(data.trim());
+
+const { Context } = await init();
+const counts = await Promise.all(
+  cleanData.map(async ({ buttons, joltage }) => {
+    const { Optimize, Int } = Context('main');
+
+    const bbtns = buttons.map((b) =>
+      new Array(joltage.length).fill(0).map((_, i) => (b.includes(i) ? 1 : 0))
+    );
+    const solver = new Optimize();
+
+    const vars = bbtns.map((_, i) => {
+      const v = Int.const(i.toString());
+      solver.add(v.ge(0));
+
+      return v;
+    });
+
+    joltage.forEach((vol, i) => {
+      const condition = bbtns.reduce(
+        (cond, btn, y) => (btn[i] === 1 ? cond.add(vars[y]) : cond),
+        Int.val(0) as Arith
+      );
+
+      solver.add(condition.eq(Int.val(vol)));
+    });
+
+    const sumVars = vars.reduce((a, v) => a.add(v), Int.val(0));
+
+    solver.minimize(sumVars);
+
+    const result = await solver.check();
+    if (result === 'sat') {
+      return Number(solver.model().eval(sumVars).toString());
+    }
+    return 0;
+  })
+);
+
+console.log(counts.reduce((a, c) => a + c, 0));

2025/10/run.ts

@@ -0,0 +1,8 @@
+import { join } from 'path';
+import { solveFirst } from './index.ts';
+
+const input = await Bun.file(join(__dirname, 'input.txt')).text();
+
+const firstAnswer = solveFirst(input);
+
+console.log(firstAnswer);