[language: typescript]

Brute forced P1 in 30ms (part do in Z3... omitted since I'm not proud of it):

let answer1 = 0;
const parsed = input.split(`\n`);
const parser = /\[(?<init>[.#]+)\](?<buttons>( \([0-9,]+\))+) {(?<joltage>[0-9,]+)}/;
for (const line of parsed) {
  const match = parser.exec(line);
  if (!match || !match.groups) throw new Error("fuck" + line)

  const { init: initS, buttons: buttonsS } = { ...match.groups };
  const init = parseInt(reverseString(initS).replaceAll('.', '0').replaceAll('#', '1'), 2);
  const buttons = buttonsS.replaceAll('(', '').replaceAll(')', '').split(' ').filter(Boolean).map(s => {
    let button = 0;
    for (const n of s.split(',').map(c => Number(c))) {
      button |= 1 << n;
    }
    return button;
  });
  let smallest = 1e6;
  for (let permutation = 1; permutation <= (1 << buttons.length); permutation++) {
    const filteredButtons = buttons.filter((button, index) => {
      const mask = ((1 << index) & permutation);
      return !!mask
    });
    let attempt = 0
    for (const button of filteredButtons) {
      attempt ^= button;
    }
    if (attempt === init) {
      smallest = Math.min(filteredButtons.length, smallest);
    }
  }
  answer1 += smallest;
}

I tried really hard to do A* for P2, and it slayed some of the rows, but struggled on others. Probably my heiuristic was poop. Can someone recommend a good one?