Untitled

a guest
Jul 12th, 2018
444
0
Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
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):
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))