From 204e42236e609d956fd9931cea1b8ea78b467e32 Mon Sep 17 00:00:00 2001 From: Pascal Syma Date: Wed, 10 Dec 2025 13:40:56 +0100 Subject: [PATCH] Solve 2025-10, add z3 solver --- 2025/10/2025-10.run.xml | 7 +++++ 2025/10/index.test.ts | 11 ++++++++ 2025/10/index.ts | 58 +++++++++++++++++++++++++++++++++++++++++ 2025/10/part2.ts | 57 ++++++++++++++++++++++++++++++++++++++++ 2025/10/run.ts | 8 ++++++ bun.lock | 7 +++++ package.json | 3 ++- 7 files changed, 150 insertions(+), 1 deletion(-) create mode 100644 2025/10/2025-10.run.xml create mode 100644 2025/10/index.test.ts create mode 100644 2025/10/index.ts create mode 100644 2025/10/part2.ts create mode 100644 2025/10/run.ts diff --git a/2025/10/2025-10.run.xml b/2025/10/2025-10.run.xml new file mode 100644 index 0000000..9f02776 --- /dev/null +++ b/2025/10/2025-10.run.xml @@ -0,0 +1,7 @@ + + + + \ No newline at end of file diff --git a/2025/10/index.test.ts b/2025/10/index.test.ts new file mode 100644 index 0000000..31a7960 --- /dev/null +++ b/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); + }); +}); diff --git a/2025/10/index.ts b/2025/10/index.ts new file mode 100644 index 0000000..9b0d47c --- /dev/null +++ b/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(); + + 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(); +} diff --git a/2025/10/part2.ts b/2025/10/part2.ts new file mode 100644 index 0000000..db06886 --- /dev/null +++ b/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)); diff --git a/2025/10/run.ts b/2025/10/run.ts new file mode 100644 index 0000000..226fb13 --- /dev/null +++ b/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); diff --git a/bun.lock b/bun.lock index 15413f2..51a7a63 100644 --- a/bun.lock +++ b/bun.lock @@ -5,6 +5,7 @@ "name": "aoc", "dependencies": { "javascript-astar": "^0.4.1", + "z3-solver": "^4.15.4", }, "devDependencies": { "@types/bun": "latest", @@ -44,6 +45,8 @@ "ansi-styles": ["ansi-styles@4.3.0", "", { "dependencies": { "color-convert": "^2.0.1" } }, "sha512-zbB9rCJAT1rbjiVDb2hqKFHNYLxgtk8NURxZ3IZwD3F6NtxbXZQCnnSi1Lkx+IDohdPlFp222wVALIheZJQSEg=="], + "async-mutex": ["async-mutex@0.3.2", "", { "dependencies": { "tslib": "^2.3.1" } }, "sha512-HuTK7E7MT7jZEh1P9GtRW9+aTWiDWWi9InbZ5hjxrnRa39KS4BW04+xLBhYNS2aXhHUIKZSw3gj4Pn1pj+qGAA=="], + "balanced-match": ["balanced-match@1.0.2", "", {}, "sha512-3oSeUO0TMV67hN1AmbXsK4yaqU7tjiHlbxRDZOpH0KW9+CeX4bRAaX0Anxt0tx2MrpRpWwQaPwIlISEJhYU5Pw=="], "brace-expansion": ["brace-expansion@2.0.1", "", { "dependencies": { "balanced-match": "^1.0.0" } }, "sha512-XnAIvQ8eM+kC6aULx6wuQiwVsnzsi9d3WxzV3FpWTGA19F621kwdbsAcFKXgKUHZWsy+mY6iL1sHTxWEFCytDA=="], @@ -124,6 +127,8 @@ "strip-ansi-cjs": ["strip-ansi@6.0.1", "", { "dependencies": { "ansi-regex": "^5.0.1" } }, "sha512-Y38VPSHcqkFrCpFnQ9vuSXmquuv5oXOKpGeT6aGrr3o3Gc9AlVa6JBfUSOCnbxGGZF+/0ooI7KrPuUSztUdU5A=="], + "tslib": ["tslib@2.8.1", "", {}, "sha512-oJFu94HQb+KVduSUQL7wnpmqnfmLsOA/nAh6b6EH0wCEoK0/mPeXU6c3wKDV83MkOuHPRHtSXKKU99IBazS/2w=="], + "typescript": ["typescript@5.7.2", "", { "bin": { "tsc": "bin/tsc", "tsserver": "bin/tsserver" } }, "sha512-i5t66RHxDvVN40HfDd1PsEThGNnlMCMT3jMUuoh9/0TaqWevNontacunWyN02LA9/fIbEWlcHZcgTKb9QoaLfg=="], "undici-types": ["undici-types@5.26.5", "", {}, "sha512-JlCMO+ehdEIKqlFxk6IfVoAUVmgz7cU7zD/h9XZ0qzeosSHmUJVOzSQvvYSYWXkFXC+IfLKSIffhv0sVZup6pA=="], @@ -142,6 +147,8 @@ "yocto-queue": ["yocto-queue@1.1.1", "", {}, "sha512-b4JR1PFR10y1mKjhHY9LaGo6tmrgjit7hxVIeAmyMw3jegXR4dhYqLaQF5zMXZxY7tLpMyJeLjr1C4rLmkVe8g=="], + "z3-solver": ["z3-solver@4.15.4", "", { "dependencies": { "async-mutex": "^0.3.2" } }, "sha512-Tcv55+k5VsPQEX7R3gIu5ieUeLp9fP1r+8+c85dQORj/v4Fy+LvOzVzZZtg4mJjUgfIhGCg6ZfAeiUiUxDPRVg=="], + "@isaacs/cliui/string-width": ["string-width@5.1.2", "", { "dependencies": { "eastasianwidth": "^0.2.0", "emoji-regex": "^9.2.2", "strip-ansi": "^7.0.1" } }, "sha512-HnLOCR3vjcY8beoNLtcjZ5/nxn2afmME6lhrDrebokqMap+XbeW8n9TXpPDOqdGK5qcI3oT0GKTW6wC7EMiVqA=="], "@isaacs/cliui/strip-ansi": ["strip-ansi@7.1.0", "", { "dependencies": { "ansi-regex": "^6.0.1" } }, "sha512-iq6eVVI64nQQTRYq2KtEg2d2uU7LElhTJwsH4YzIHZshxlgZms/wIc4VoDQTlG/IvVIrBKG06CrZnp0qv7hkcQ=="], diff --git a/package.json b/package.json index 8a89056..0312bf8 100644 --- a/package.json +++ b/package.json @@ -26,6 +26,7 @@ "typescript": "^5.7.2" }, "dependencies": { - "javascript-astar": "^0.4.1" + "javascript-astar": "^0.4.1", + "z3-solver": "^4.15.4" } }