#advent of code 2025
#day 10
#can probably rewrite it from scratch instead of using z3
#will try later
#part 1 is way too slow as well

from z3 import *
import heapq

machineInstructions=[];
PuzzleInput=open("10.in","r");
for l in PuzzleInput:
	l=l.strip();
	diagram, residue=l.split("] ");
	diagram=list([1*(light=="#") for light in diagram.replace("[","")])
	buttons, joltage = residue.split(" {");
	joltage=list([int(jolt) for jolt in joltage.replace("}","").split(",")]);
	buttons=[tuple([int(but) for but in button.replace(")","").replace("(","").split(",")]) for button in buttons.split(" ")];
	machineInstructions.append((diagram, buttons, joltage));
PuzzleInput.close();

#part 1
def findSequence(machinstr):
	target,options,power=machinstr; #power unused
	state=[0 for t in target];
	visited=list();
	queue=[];
	heapq.heappush(queue,(0,state,[0 for b in range(len(options))]));
	while queue:
		presses,currentState,prevButtons=heapq.heappop(queue);
		if currentState==target:
			return presses;
		if prevButtons in visited:
			continue;
		visited.append(prevButtons);
		
		for o in range(len(options)):
			newstate=[cs for cs in currentState];
			for s in options[o]:
				newstate[s]=(newstate[s]+1)%2;
			newbuttons=[prevButtons[b]+1*(b==o) for b in range(len(prevButtons))];
			heapq.heappush(queue,(presses+1,newstate,newbuttons));
	return 999999;

def adjustPower(machinstr):
	lights,options,power=machinstr; #lights unused
	buttons=[[1*(b in but) for b in range(len(power))] for but in options];
	solver=z3.Optimize();
	xVector=[z3.Int(f'x{x}') for x in range(len(buttons))]; 
	powerVector=[z3.Int(f'p{p}') for p in range(len(power))];
	
	for x in range(len(buttons)):
		solver.add(z3.Int(f'x{x}')>=0);
	
	for p in range(len(powerVector)):
		solver.add(powerVector[p]==power[p]);
	
	for p in range(len(power)):
		solver.add(powerVector[p]==z3.Sum([xVector[x] for x in range(len(buttons)) if buttons[x][p]==1]));
	
	solver.minimize(z3.Sum(xVector));
	solver.check();
	model=solver.model();
	presses=[model[mult].as_long() for mult in xVector];
	score=sum(presses);
	return score


part1=0;
part2=0;

for mi,instr in enumerate(machineInstructions):
	part1+=findSequence(instr);
	part2+=adjustPower(instr);	
print("part 1",part1);
print("part 2",part2);