Advertisement
Guest User

Untitled

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