Challenge Description#

After drilling his whole life, Simon wanted something really hard to drill. So, of course, he turned to NP-Hard problems. However, he’s a bit stuck, since this requires some Sciency-Fancy stuff for which you need to help him out.

Analysis#

The challenge gave one image (drillthis.png) and one remote endpoint (nc chals2.apoorvctf.xyz 14001). The service always printed a graph in edge-list format (n m followed by m undirected edges) and then asked for a single submission. At first glance this looked like a standard “compute one NP-hard graph metric” task, but the server responses were intentionally trollish: repeated runs returned different YouTube links and multiple flag-like strings that did not validate as the real flag.

I confirmed this behavior by repeatedly connecting and sending fixed values, including 0 and also computed candidates. The terminal token at the end clearly came from a decoy pool, so the key was to infer the answer format rather than trusting those immediate outputs. The image strongly indicated a minimum vertex cover style illustration (selected vertices covering all edges), so I solved MVC exactly with Z3.

The important catch was that sending only the scalar size (for example 133) was not enough. The service expected the actual vertex set, space-separated. Once I submitted the exact set of vertices from the model, the service returned a new flag string that validated.

Here is the successful run command and its relevant output.

1
import socket,re
2
from z3 import Optimize,Bool,Sum,If,Or,sat
3

4
HOST='chals2.apoorvctf.xyz'; PORT=14001
5
ansi=re.compile(r'\x1b\[[0-9;?]*[A-Za-z]')
6

7
def parse_graph(text):
8
    lines=[ln.strip() for ln in text.splitlines() if ln.strip()]
9
    i=lines.index('Graph:')
10
    n,m=map(int,lines[i+1].split())
11
    edges=[]
12
    for k in range(m):
13
        u,v=map(int,lines[i+2+k].split())
14
        edges.append((u,v))
15
    return n,m,edges
16

17
s=socket.create_connection((HOST,PORT),timeout=20)
18
b=b''
19
while b'Submit your answer:' not in b:
20
    c=s.recv(65536)
21
    if not c: break
22
    b+=c
23
pre=ansi.sub('',b.decode('utf-8','replace'))
24
n,m,edges=parse_graph(pre)
25

26
x={i:Bool(f'x{i}') for i in range(1,n+1)}
27
opt=Optimize()
28
for u,v in edges:
29
    opt.add(Or(x[u],x[v]))
30
obj=Sum([If(x[i],1,0) for i in range(1,n+1)])
31
opt.minimize(obj)
32
assert opt.check()==sat
33
md=opt.model()
34
sel=[i for i in range(1,n+1) if md.eval(x[i], model_completion=True)]
35
payload=' '.join(map(str,sel))
36

37
s.sendall((payload+'\n').encode())
38
out=b''
39
while True:
40
    c=s.recv(65536)
41
    if not c: break
42
    out+=c
43
s.close()
44

45
alltxt=ansi.sub('',(b+out).decode('utf-8','replace'))
46
print('\n'.join([ln for ln in alltxt.splitlines() if ln.strip()][-6:]))

1
python solve.py

1
Submit your answer:
2
===================================================
3
apoorvctf{My_Dr4LL_is_The_Dr4LL_Th4t_wiLL_pi3rc3_the_NP-H3vens!!__420}
4
===================================================

That was the turning point: same core NP-hard idea, but wrong output format had been causing all the fake-out endings.

Solution#

1
import socket,re
2
from z3 import Optimize,Bool,Sum,If,Or,sat
3

4
HOST='chals2.apoorvctf.xyz'; PORT=14001
5
ansi=re.compile(r'\x1b\[[0-9;?]*[A-Za-z]')
6

7
def parse_graph(text):
8
    lines=[ln.strip() for ln in text.splitlines() if ln.strip()]
9
    i=lines.index('Graph:')
10
    n,m=map(int,lines[i+1].split())
11
    edges=[]
12
    for k in range(m):
13
        u,v=map(int,lines[i+2+k].split())
14
        edges.append((u,v))
15
    return n,m,edges
16

17
s=socket.create_connection((HOST,PORT),timeout=20)
18
b=b''
19
while b'Submit your answer:' not in b:
20
    c=s.recv(65536)
21
    if not c: break
22
    b+=c
23
pre=ansi.sub('',b.decode('utf-8','replace'))
24
n,m,edges=parse_graph(pre)
25

26
x={i:Bool(f'x{i}') for i in range(1,n+1)}
27
opt=Optimize()
28
for u,v in edges:
29
    opt.add(Or(x[u],x[v]))
30
obj=Sum([If(x[i],1,0) for i in range(1,n+1)])
31
opt.minimize(obj)
32
assert opt.check()==sat
33
md=opt.model()
34
sel=[i for i in range(1,n+1) if md.eval(x[i], model_completion=True)]
35
payload=' '.join(map(str,sel))
36

37
s.sendall((payload+'\n').encode())
38
out=b''
39
while True:
40
    c=s.recv(65536)
41
    if not c: break
42
    out+=c
43
s.close()
44

45
alltxt=ansi.sub('',(b+out).decode('utf-8','replace'))
46
print(alltxt)

1
python solve.py

1
apoorvctf{My_Dr4LL_is_The_Dr4LL_Th4t_wiLL_pi3rc3_the_NP-H3vens!!__420}