Advertisement
Guest User

Untitled

a guest
Jul 12th, 2018
453
0
Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
Python 1.07 KB | None | 0 0
  1. #!/usr/bin/env python
  2.  
  3. from itertools import combinations
  4.  
  5. while True:
  6.     bits = input('Input (binary string, e.g. 1001): ')
  7.     nbits = len(bits)
  8.     if nbits >= 3:
  9.         break
  10.     print('Please input at least 3 bits.')
  11.  
  12. clauses = []
  13. ncombs = 0
  14. for indexes in combinations(range(nbits), 3):
  15.     for pad in [ '001', '010', '100', '111' ]:
  16.         terms = []
  17.         for i, v in enumerate(indexes):
  18.             mask = (pad[i] == bits[v])
  19.             term = '   (X_{})'.format(v) if mask else 'NOT(X_{})'.format(v)
  20.             terms.append(term)
  21.         clause = '( ' + ' v '.join(terms) + ' )'
  22.         clauses.append(clause)
  23.     ncombs += 1
  24.  
  25. if ncombs != nbits * (nbits - 1) * (nbits - 2) // 6:
  26.     raise Exception('Error: number of combinations.')
  27. if len(clauses) != 4 * ncombs:
  28.     raise Exception('Error: number of clauses.')
  29.  
  30. print('\nConstructed 3-SAT:')
  31. print(' ^\n'.join(clauses) + '\n')
  32. print('input length: {}'.format(nbits))
  33. print('combinations: {} == C({}, 3)'.format(ncombs, nbits))
  34. print('clauses: {} == 4 * {}'.format(len(clauses), ncombs))
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement