Skip to content

Instantly share code, notes, and snippets.

Created June 3, 2017 14:05
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save edeca/640fad378a6e847ab77aa47fb607d8b4 to your computer and use it in GitHub Desktop.
Save edeca/640fad378a6e847ab77aa47fb607d8b4 to your computer and use it in GitHub Desktop.
Basic solving of a "suko" puzzle using pysmt
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:
# 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)
model = get_model(formula)
if model:
print("No solution found!")
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment