sattelite - ASIS CTF Finals 2014

sat.py

import socket
import pycosat

def clean(s):
    s = s.replace('(', '')
    s = s.replace(')', '')
    s = s.replace('x', '')
    s = s.replace('\xc2\xac', '-')
    s = s.replace('\xe2\x88\xa8', '')
    return map(int, s.split())


s = socket.socket()
s.connect(('asis-ctf.ir', 12435))
print s.recv(1024)
s.send('Sattelite\n')

while 1:
    msg = s.recv(1024).strip()
    print msg
    equations = [clean(x) for x in msg.split("\xe2\x88\xa7")]
    print equations
    solution = pycosat.solve(equations)
    if solution != "UNSAT":
        print solution
        solution = "".join(["0" if x < 0 else "1" for x in solution])
        if len(solution) < len(equations):
            solution += "0" * (len(equations) - len(solution))
    else:
        solution = "unsat"
    print solution
    s.send(solution + "\n")
    msg = s.recv(1024).strip()
    print msg
    if "OK" not in msg:
        break