Skip to content

Instantly share code, notes, and snippets.

@khang06
Created September 15, 2021 21:19
Show Gist options
  • Save khang06/1ef3b6c0117c42fa43b2a38bcf6fa91f to your computer and use it in GitHub Desktop.
Save khang06/1ef3b6c0117c42fa43b2a38bcf6fa91f to your computer and use it in GitHub Desktop.
Solving/ruining the fun of a hard logic puzzle with Z3
from z3 import *
from typing import List
# Please use this responsibly and not in any remotely competitive environment
class LogicSolver:
def __init__(self, comparables: List[int]):
self.comparables = comparables
self.vars = {}
self.solver = Solver()
def add_set(self, setVals: str):
s = self.solver
addedVals = []
for val in setVals.split():
z3obj = Int(val)
addedVals.append(z3obj)
self.vars[val] = z3obj
#s.add(z3obj >= self.min, z3obj <= self.max)
s.add(Or([z3obj == x for x in self.comparables])) # TODO: there has to be a better way
s.add(Distinct(addedVals))
def print_results(self):
print(self.solver.check())
print(self.solver.model())
# define possibilities
ls = LogicSolver([55, 60, 65, 70, 75, 80, 85])
ls.add_set('al betsy cora donna edwin faith gideon')
ls.add_set('m550 m775 m1250 m1500 m1825 m2000 m2500')
ls.add_set('anthon cromwell philo quasqueton springfield van zwingle')
# helper functions
s = ls.solver
def mixed_pairs(a, b, c, d):
s.add(Or(And(a == c, b == d), And(a == d, b == c)))
def either_or(a, b, c):
s.add(Or(a == b, a == c))
# define constraints
# evil global stuff!!!
globals().update(ls.vars)
# Of the tank bought by Donna Drake and the tank bought by Cora Carey,
# one is going to Zwingle and the other cost $2,000.
mixed_pairs(donna, cora, zwingle, m2000)
# Of the tank going to Anthon and the $550 display,
# one was bought by Faith Frisk and the other is 60 gallons.
mixed_pairs(anthon, m550, faith, 60)
# The $2,000 fish tank is somewhat larger than the tank bought by Faith Frisk.
s.add(m2000 > faith)
# The 85 gallon fish tank didn't cost $1,825.
s.add(85 != m1825)
# The fish tank going to Van Wert is somewhat larger than the display bought by Edwin Ellis.
s.add(van > edwin)
# The tank going to Van Wert is 5 gallons smaller than the $775 display.
s.add(van == m775 - 5)
# The seven tanks are the display going to Cromwell, the display bought by Donna Drake,
# the 55 gallon tank, the $1,500 display, the 70 gallon display, the 80 gallon tank and the 65 gallon tank.
s.add(Distinct(cromwell, donna, 55, m1500, 70, 80, 65))
# The display bought by Edwin Ellis isn't 55 gallons.
s.add(edwin != 55)
# The $2,500 display is either the fish tank going to Van Wert or the 80 gallon fish tank.
either_or(m2500, van, 80)
# The tank bought by Faith Frisk is somewhat larger than the display bought by Gideon Gates.
s.add(faith > gideon)
# The fish tank going to Zwingle is 10 gallons larger than the $775 fish tank.
s.add(zwingle == m775 + 10)
# The display bought by Al Ayala is 5 gallons smaller than the display bought by Donna Drake.
s.add(al == donna - 5)
# The $1,500 display is 5 gallons larger than the tank going to Quasqueton.
s.add(m1500 == quasqueton + 5)
# Of the $1,500 fish tank and the display bought by Donna Drake,
# one is going to Springfield and the other is 60 gallons.
mixed_pairs(m1500, donna, springfield, 60)
# go!
ls.print_results()
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment