public
Created

sudoku generator for smtlib input format

  • Download Gist
sudoku_smt.py
Python
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52
import numpy
 
MODEL = """\
53..7....
6..195...
.98....6.
8...6...3
4..8.3..1
7...2...6
.6....28.
...419..5
....8..79
"""
 
def select(list):
return ' '.join('(select a {0})'.format(l) for l in list)
 
def main(model):
lines = []
lines.append('(set-logic AUFLIRA)')
lines.append('(set-option :produce-models true)')
lines.append('(declare-fun a () (Array Int Int))')
index = numpy.arange(81).reshape(9,9)
for i in xrange(9):
lines.append('(assert (distinct {}))'.format(select(index[:,i])))
lines.append('(assert (distinct {}))'.format(select(index[i,:])))
 
r0 = (i % 3) * 3
c0 = (i // 3) * 3
lines.append('(assert (distinct {}))'.format(
select(index[r0:r0+3,c0:c0+3].ravel())
))
 
for i in xrange(81):
lines.append('(assert (< 0 (select a {0})))'.format(i))
lines.append('(assert (> 10 (select a {0})))'.format(i))
 
for i, n in zip(xrange(81), model):
if n != '.':
lines.append('(assert (= {0} (select a {1})))'.format(n, i))
 
lines.append('(check-sat)')
lines.append('(get-value ({}))'.format(select(xrange(81))))
 
return lines
 
with open('sod1.smt', 'w') as out:
model = MODEL.replace('\n', '').replace('\r', '').strip()
out.write('\n'.join(main(model)))
out.write('\n')
print "Done, now run 'builds/bin/cvc4 --lang smt sod1.smt'"

Please sign in to comment on this gist.

Something went wrong with that request. Please try again.