1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
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);
|
