Skip to content

@teh /sudoku_smt.py
Created

Embed URL

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
sudoku generator for smtlib input format
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'"
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Something went wrong with that request. Please try again.