feat: 2025 Day 10 Part 2

closes #13

Author: mfulton26

.gitignore

@@ -0,0 +1 @@
+node_modules/

2025/day/10/part/2/solve.mts

@@ -0,0 +1,34 @@
+import process from "node:process";
+import { text } from "node:stream/consumers";
+import { init } from "z3-solver";
+import { parseManual } from "../../manuals.ts";
+
+export default async function solve(input: string) {
+  const manual = parseManual(input);
+  const { Context } = await init();
+  let sum = 0;
+  for (const { buttons, requirements } of manual) {
+    const { Int, Optimize } = Context("main");
+    const variables = buttons.map((_, i) => Int.const(`b${i}`));
+    const optimize = new Optimize();
+    optimize.add(
+      ...requirements.map((requirement, lightIndex) =>
+        buttons.keys()
+          .filter((buttonIndex) => buttons[buttonIndex].includes(lightIndex))
+          .map((buttonIndex) => variables[buttonIndex])
+          .reduce((a, b) => a.add(b), Int.val(0))
+          .eq(Int.val(requirement))
+      ),
+      ...variables.map((variable) => variable.ge(0)),
+    );
+    const sumExpression = variables.reduce((a, x) => a.add(x), Int.val(0));
+    optimize.minimize(sumExpression);
+    if (await optimize.check() !== "sat") throw new Error("No solution found");
+    sum += +optimize.model().eval(sumExpression);
+  }
+  return sum;
+}
+
+const input = await text(process.stdin);
+const output = await solve(input);
+console.log(output);

2025/day/10/part/2/solve.test.ts

@@ -0,0 +1,12 @@
+import solve from "./solve.ts";
+
+import { assertEquals } from "@std/assert";
+
+Deno.test("example", async () => {
+  const input = `\
+[.##.] (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}`;
+
+  assertEquals(await solve(input), 33);
+});

2025/day/10/part/2/solve.ts

@@ -0,0 +1,17 @@
+/** delegates to Node.js until https://github.com/denoland/deno/issues/17171 is fixed */
+export default async function solve(input: string) {
+  const command = new Deno.Command("node", {
+    args: [`${import.meta.dirname}/solve.mts`],
+    stdin: "piped",
+    stdout: "piped",
+  });
+
+  const child = command.spawn();
+  const writer = child.stdin.getWriter();
+  await writer.write(new TextEncoder().encode(input));
+  writer.releaseLock();
+  await child.stdin.close();
+
+  const { stdout } = await child.output();
+  return +new TextDecoder().decode(stdout);
+}

deno.json

@@ -1,12 +1,13 @@
 {
+  "nodeModulesDir": "auto",
   "tasks": {
     "prepare": "cp -r :year/day/:day",
     "serve": "deno run -A main.ts",
     "solve": "./bin/aoc.ts solve"
   },
   "imports": {
     "@deno/emit": "jsr:@deno/emit@^0.46.0",
-    "@graph-algorithm/minimum-cut": "https://esm.sh/@graph-algorithm/minimum-cut@2.0.0",
+    "@graph-algorithm/minimum-cut": "npm:@graph-algorithm/minimum-cut@^2.0.0",
     "@lib/": "./lib/",
     "@std/assert": "jsr:@std/assert@^1.0.9",
     "@std/cli": "jsr:@std/cli@^1.0.8",
@@ -15,6 +16,7 @@
     "@std/fs": "jsr:@std/fs@^1.0.6",
     "@std/path": "jsr:@std/path@^1.0.8",
     "nerdamer": "npm:nerdamer@^1.1.13",
-    "pretty-ms": "npm:pretty-ms@^9.3.0"
+    "pretty-ms": "npm:pretty-ms@^9.3.0",
+    "z3-solver": "npm:z3-solver@^4.15.4"
   }
 }