Basic solving of a "suko" puzzle using pysmt

suko-smt.py

from pysmt.shortcuts import Symbol, Plus, Equals, GE, LE, And, Int, AllDifferent, get_model
from pysmt.typing import INT

########
# Author: David Cannings
#   Date: June 2017
#
# Basic example using pysmt to solve "Suko", a puzzle printed in some
# UK newspapers and available online.
#
# This is based on the Github example code for pysmt.  It would be
# trivial to add argparse to make a generic suko SMT solver.
#
# See: https://edeca.net/post/2017/06/solving-suko-with-pysmt/
########

# Setup symbols from A1..C3, this could be a list but named
# items are easier to use later.
cells = {}
for col in ['a', 'b', 'c']:
    for row in ['1', '2', '3']:
        key = col + row
        cells[key] = Symbol(key, INT)

# All cells must be >=1 and <=9
valid_range = And([And(GE(c, Int(1)), LE(c, Int(9))) for c in cells.values()])

# We must use the numbers 1..9 exactly once each
no_repeats = AllDifferent(cells.values())

# The three shaded areas must add to these values
sum_area_1 = Equals(Plus(cells['a1'], cells['b1'], cells['b2']), Int(17))
sum_area_2 = Equals(Plus(cells['a2'], cells['a3'], cells['b3']), Int(12))
sum_area_3 = Equals(Plus(cells['c1'], cells['c2'], cells['c3']), Int(16))

# The four squares adjacent to circles must equal these numbers
sum_circle_1 = Equals(
    Plus(cells['a1'], cells['a2'], cells['b1'], cells['b2']), Int(21))
sum_circle_2 = Equals(
    Plus(cells['b1'], cells['c1'], cells['b2'], cells['c2']), Int(29))
sum_circle_3 = Equals(
    Plus(cells['a2'], cells['b2'], cells['a3'], cells['b3']), Int(21))
sum_circle_4 = Equals(
    Plus(cells['b2'], cells['c2'], cells['b3'], cells['c3']), Int(22))

# All conditions must be true, all of the time
formula = And(valid_range, no_repeats, sum_area_1, sum_area_2,
              sum_area_3, sum_circle_1, sum_circle_2, sum_circle_3, sum_circle_4)

print(formula)
model = get_model(formula)
if model:
    print(model)
else:
    print("No solution found!")