Advertisement
Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- #!/usr/bin/env python
- from itertools import combinations
- while True:
- bits = input('Input (binary string, e.g. 1001): ')
- nbits = len(bits)
- if nbits >= 3:
- break
- print('Please input at least 3 bits.')
- clauses = []
- ncombs = 0
- for indexes in combinations(range(nbits), 3):
- for pad in [ '001', '010', '100', '111' ]:
- terms = []
- for i, v in enumerate(indexes):
- mask = (pad[i] == bits[v])
- term = ' (X_{})'.format(v) if mask else 'NOT(X_{})'.format(v)
- terms.append(term)
- clause = '( ' + ' v '.join(terms) + ' )'
- clauses.append(clause)
- ncombs += 1
- if ncombs != nbits * (nbits - 1) * (nbits - 2) // 6:
- raise Exception('Error: number of combinations.')
- if len(clauses) != 4 * ncombs:
- raise Exception('Error: number of clauses.')
- print('\nConstructed 3-SAT:')
- print(' ^\n'.join(clauses) + '\n')
- print('input length: {}'.format(nbits))
- print('combinations: {} == C({}, 3)'.format(ncombs, nbits))
- print('clauses: {} == 4 * {}'.format(len(clauses), ncombs))
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement