周末做了两道题，想尝试下ppc结果因为电阻间不同阻值只存了后面那个被坑了一整天……Orz
PPC-M
Resistance
列KVL，设起点电压10终点电压0，然后z3求解。主办方表示卧槽这题z3居然能做？比预期解慢，但是起码是对的(:з)∠)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
77
78
79
80
81
82
83
84
85
86
87
88
89#!/usr/bin/python2
import ssl, socket
import z3
y = [z3.Real('a_%d'%i) for i in range(30)]
d = dict()
connection = dict()
nodes = set()
class Connect(object):
def __init__(self, host, port):
self.context = ssl.create_default_context()
self.conn = self.context.wrap_socket(
socket.socket(socket.AF_INET),
server_hostname=host)
self.conn.connect((host, port))
self.f = self.conn.makefile('rwb', 0)
def __enter__(self):
return self.f
def __exit__(self, type, value, traceback):
self.f.close()
ncount = 0
with Connect('programming.pwn2win.party', 9001) as f:
#b = open('d.txt','w')
#with open('test.txt','rb') as f:
for line in f:
line = line.strip()
print('received: %s' % line)
if line.startswith(b'CTF-BR{') or \
line == b'WRONG ANSWER': break
numbers = map(int, line.split())
if len(numbers)==3:
if ncount==0:
d = dict()
connection = dict()
nodes = set()
nodes.add(numbers[0])
nodes.add(numbers[1])
ar = min(numbers[0],numbers[1]),max(numbers[0],numbers[1])
if ar not in d.keys():
d[ar] = [numbers[2]]
else:
d[ar].append(numbers[2])
if numbers[0] in connection.keys():
if numbers[1] not in connection[numbers[0]]:
connection[numbers[0]].append(numbers[1])
else:
connection[numbers[0]] = [numbers[1]]
if numbers[1] in connection.keys():
if numbers[0] not in connection[numbers[1]]:
connection[numbers[1]].append(numbers[0])
else:
connection[numbers[1]] = [numbers[0]]
ncount+=1
elif len(numbers) == 2:
ncount = 0
if numbers[0]==numbers[1]:
f.write('0.000\n')
print "0.000"
continue
#solve all KVL
s = z3.Solver()
for m in nodes:
sum = 0
if m!=numbers[0] and m!=numbers[1]:
for n in connection[m]:
for k in d[min(n,m),max(n,m)]:
sum += ((y[m] - y[n]) / k)
s.add(sum == 0.0)
s.add(y[numbers[0]]==10.0)
s.add(y[numbers[1]]==0.0)
s.check()
m = s.model()
#print m
flag = map(lambda sym: m[sym], y)
start = float(eval(str(flag[numbers[0]])+'.'))
sum=0
for n in connection[numbers[0]]:
for k in d[min(numbers[0],n),max(n,numbers[0])]:
sum+=(m[y[numbers[0]]]-m[y[n]])/k
sum = eval(str(z3.simplify(sum))+'.')
f.write(("%.3f\n"%(10.0/sum)).encode('utf-8'))
print "%.3f"%(10.0/sum)
Reversing
Achievement Unlocked
golang 写的，没啥好说的，z3解
1 | import z3 |