Skip to content

Instantly share code, notes, and snippets.

Last active January 24, 2021 13:28
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
Star You must be signed in to star a gist
What would you like to do?
# Usage: <cnf-file> <sat-solver-output-file>
import re
import sys
def strip_cnf_mapping(filename):
# lines look like 'c var 1 == 000001 chosen'
mapping = {}
pattern = re.compile('c var ([^\\s]+) == ([^\\s]+) chosen')
with open(filename) as f:
for line in f:
if line.startswith('p'): continue
if not line.startswith('c'): return mapping
m = re.match(pattern, line)
if m is None: continue
mapping[int(m.groups()[0])] = m.groups()[1]
return mapping
def strip_sat_solution(filename):
pos = []
with open(filename) as f:
for line in f:
if not line.startswith('v'): continue
pos += [int(x) for x in line[1:].strip().split(' ') if int(x) > 0]
return pos
def verify_commafree(codewords):
n = len(codewords[0])
cws = set(c for c in codewords)
for x in codewords:
for y in codewords:
for i in range(1,n):
cw = x[i:]+y[:i]
if cw in cws:
print("CONFLICT: %s, %s, and %s." % (x,y,cw))
return False
return True
if __name__ == '__main__':
if len(sys.argv) < 3:
print('Usage: %s <cnf-file> <sat-solver-output-file>' % sys.argv[0])
mapping = strip_cnf_mapping(sys.argv[1])
solution = strip_sat_solution(sys.argv[2])
code = [mapping[code_id] for code_id in solution
if mapping.get(code_id) is not None]
assert verify_commafree(code)
print('{' + ', '.join(sorted(code)) + '}')
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment