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.

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

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

def parse_graph(text):
    lines=[ln.strip() for ln in text.splitlines() if ln.strip()]
    i=lines.index('Graph:')
    n,m=map(int,lines[i+1].split())
    edges=[]
    for k in range(m):
        u,v=map(int,lines[i+2+k].split())
        edges.append((u,v))
    return n,m,edges

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

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

s.sendall((payload+'\n').encode())
out=b''
while True:
    c=s.recv(65536)
    if not c: break
    out+=c
s.close()

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

python solve.py

Submit your answer:
===================================================
apoorvctf{My_Dr4LL_is_The_Dr4LL_Th4t_wiLL_pi3rc3_the_NP-H3vens!!__420}
===================================================

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

Solution#

# solve.py
import socket,re
from z3 import Optimize,Bool,Sum,If,Or,sat

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

def parse_graph(text):
    lines=[ln.strip() for ln in text.splitlines() if ln.strip()]
    i=lines.index('Graph:')
    n,m=map(int,lines[i+1].split())
    edges=[]
    for k in range(m):
        u,v=map(int,lines[i+2+k].split())
        edges.append((u,v))
    return n,m,edges

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

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

s.sendall((payload+'\n').encode())
out=b''
while True:
    c=s.recv(65536)
    if not c: break
    out+=c
s.close()

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

python solve.py

apoorvctf{My_Dr4LL_is_The_Dr4LL_Th4t_wiLL_pi3rc3_the_NP-H3vens!!__420}