1 files changed, 76 insertions, 0 deletions
diff --git a/2025/aoc2025-d10.py b/2025/aoc2025-d10.py
new file mode 100644
index 0000000..17cb090
--- /dev/null
+++ b/2025/aoc2025-d10.py
@@ -0,0 +1,76 @@
+#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);