Skip to content

Instantly share code, notes, and snippets.

@volpino volpino/sat.py
Created Oct 13, 2014

Embed
What would you like to do?
sattelite - ASIS CTF Finals 2014
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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.