Advertisement
Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- #!/usr/bin/env python
- from itertools import combinations
- import pycosat
- import random
- # while True:
- # bits = input('Input (binary string, e.g. 1001): ')
- # nbits = len(bits)
- # if nbits >= 3:
- # break
- # print('Please input at least 3 bits.')
- nbits = 100
- bits = [random.randint(0,1) for i in range(nbits)]
- print(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])
- terms.append(v+1 if mask else -v-1)
- clauses.append(terms)
- 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(clauses)
- print('input length: {}'.format(nbits))
- print('combinations: {} == C({}, 3)'.format(ncombs, nbits))
- print('clauses: {} == 4 * {}'.format(len(clauses), ncombs))
- print(pycosat.solve(clauses))
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement