In [30]:
given = """
E N T E R L A S E R L A S E R R E S A L
L A S E R O B S I D I A N L A S E R G W
E R E S A L L A S E R L M R R E S A L A
L A S E R R E S A L A O E R L A S E R L
L L E M I T T E R S O S E L R E S A L L
A A M R E S A L E N A S L A L A S E R R
S S R E S A L R S L A R A S R E S A L E
E E L A S E R T R L L E S E L A S E R S
R R W A L L O E R R A S E R R E S A L A
L A S E R N S E L E S A R E B E R Y L L
L R L M E A S L A S E L N L L A S E R J
A E A O L A R A S A R O L R E S A L A E
S S S O L L E S E L T A L A S E R D S M
E A E N R A S E R S W R E S A L E L R I
R L R S E S A R D R L A S E R O W A E T
L R R T S E L O E T R E S A L N A S S T
A E E O A R O S O N L A S E R Y L E A E
S S S N L L A B A R R E S A L X L R L R
E A A E B L R E S A L L A S E R E X I T
R L L L A S E R E S L A S E R L A S E R
""".strip().replace(' ', '\t')
print(given)
In [3]:
print("""
Artisan
Bass speaker
Count (on)
Deprived (of)
Enjoyed together
False teeth
French cap
Gram or pound
Inform (of)
Like a birthday
Moon feature
More confident
Not capable
Place a value on
Put in danger
Race in stages
Recycle alternative
Regal
Renders undrinkable
Rip up
Suitor
Trash
Undo a wedding
Wave rider
""".replace('\t', ' '))
In [5]:
import forge
from puzzle.puzzlepedia import puzzlepedia
puzzle = puzzlepedia.parse("""
@ 6 9 7 11 3 1 8 4 10 5 12 2
* APPRAISE
* DENATURE
* IMPERIAL
* ?
* RELAY
* ?
* BEREFT
* CRAFTER
* REFUSE
* SURFER
* UNFIT
* WOOFER
""".lower())
In [22]:
import Numberjack
given = """
1 0 1 0 0
0 0 0 1 1
0 0 1 0 1
0 1 1 1 0
1 0 1 0 1
0 1 0 1 1
0 0 1 0 0
1 0 1 1 1
1 0 0 0 0
1 1 0 0 1
""".strip()
G = Numberjack.Matrix(5, 5, 'x')
model = Numberjack.Model()
options = G.row + G.col
def constrain(bits):
model.add(Numberjack.Disjunction([
Numberjack.Conjunction([bits_bit == option_bit for bits_bit, option_bit in zip(bits, option)])
for option in options
]))
for soln in given.split('\n'):
bits = [bit == '1' for bit in soln.split('\t')]
constrain(bits)
solver = model.load('Mistral')
solver.solve()
print(str(model))
print("is_sat", solver.is_sat())
print("is_unsat", solver.is_unsat())
for r in range(5):
row = []
for c in range(5):
row.append('%2d' % G[r][c].get_value())
print('\t'.join(row))
In [23]:
''.join("""
QLSRUXWGGSFCSUSLFWLSDAFHWFIXTEYYCMVT
OLTGUGHVHMVIXOUBWEZFTHYPTXCGPWGIKOLW
BFIIRBYXTOGQYFPYOZZXGMQJNUUGHNWNWATH
MYZFRGMSYUUFVYEDPTPHLJOOQLFTXARTWKOG
YNJSTTHPXNCRHOSHLKJYWVBTDCYNRGLVKMWN
HIURUSGNCIFNJWXWCPCTROYRQGELVRFWEAGT
RHTFGEWNRJGYGYKFVYEYMSPQDWKFEXUDPJRZ
EMDDUGUCGTGRGMFGRPVYIMVQUWVBGOAPKRGN
GHJTUTNYGWYWWKVTKRTRUNULGYFUYEXQRUCF
CNXJKUFKHYJVCITWIBGMGIIFRIARRIXAWJKI
SUNERQRUTFGRGFDPMJUWNBWDJWKCZJJYFVKN
WJSHPGNPLPLTULJHRSMKMAXNVZYRMYGHWNDU
ENUIWQDDLSATXFJQSZSTNPZIVERLCTLXKGTD
WZIQXWCYTGERRLFWMQMJSXILJAVGSTCRVQHW
VFJPUQNUFHEYMHNYNNLRJGJRQKXGFPRENLWR
GHDDFLLNUZHTXQRFTCXQMAJNYGILDPIZXUGK
""".strip().split('\n'))
Out[23]:
In [24]:
example = {"ver":[[1,2,3],[0],[0],[0],[0],[0],[0],[0],[0],[0],[0],[0],[0],[0],[0],[0],[0],[0],[0],[0],[0],[0],[0],[0],[0],[0],[0],[0],[0],[0],[0],[0],[0],[0],[0],[0],[0],[0]],"hor":[[12,3],[0],[0],[0],[0],[0],[0],[0],[0],[0],[0],[0],[0],[0],[0],[0],[0],[0],[0],[0],[0],[0],[0],[0],[0],[0],[0],[0],[0],[0],[0],[0],[0],[0],[0],[0],[0],[0],[0],[0],[0],[0],[0],[0],[0],[0],[0],[0],[0],[0]]}
In [26]:
ver_str = """
5 1 1 5
4 3 3 1 3 4 3 4
4 4 1 1 1 1 1 1 4 3
3 4 3 1 1 1 1 2 4 3
2 4 1 1 1 1 1 1 1 5 2
1 2 2 3 4 3 4 2 2 1
1 2 2 2 2 1
2 2 2 2
2 2 4 4 4 4 4 1 1 2 2
2 2 1 1 1 1 1 1 1 1 2 2 2 2
2 2 3 4 4 1 1 1 1 1 1 1 2 2
2 2 1 1 1 1 1 1 1 1 1 1 1 2 2
2 4 4 4 1 2 4 4 1 1 2 2
2 4 2 2
2 6 2 2
2 6 1 1 4 4 4 2 4
2 7 1 1 1 1 1 1 1 2 4
2 4 2 4 1 1 1 1 4 2 5
2 8 1 1 1 1 1 1 4 5
2 5 3 1 4 4 4 5 5
2 6 3 6 6
2 5 3 6 5
2 6 4 4 8 6
2 6 24 3 3 2
9 23 3 2 2
2 1 5 4 3 3 2 2
1 3 5 4 4 4 2 2 1
1 3 4 15 4 2 2 1
2 3 4 9 5 2 2 2
3 3 5 5 2 2 3
3 3 6 7 2 2 3
4 3 18 4 4
5 4 14 4 5
6 4 8 4 6
8 4 5 8
10 5 6 9
12 19 11
14 14 13
""".strip()
hor_str = """
00 00 0 0 00 00 00 00 0 0 0 0 0 0 0 1 1 0 0 0 0 0 0 0 0 0 0 1 1 0 0 0 0 1 1
00 00 0 0 00 00 00 00 0 0 0 0 0 0 0 1 1 0 0 0 0 0 1 0 0 0 0 1 1 0 0 0 0 1 1
00 00 0 0 00 00 00 00 0 0 0 0 0 0 0 1 1 1 0 0 0 1 1 1 0 0 0 1 1 0 0 0 5 1 1
00 00 0 0 00 00 00 00 0 2 1 1 0 0 0 1 1 1 0 0 0 5 1 1 0 0 5 1 1 3 0 0 1 1 5 1
00 00 0 0 00 00 00 00 0 1 1 1 0 0 5 1 1 1 0 0 5 1 1 3 3 0 5 1 1 5 0 0 1 1 1 3
00 00 0 3 01 00 00 00 6 1 1 1 5 0 5 1 1 3 0 0 5 1 1 5 1 0 5 1 1 5 0 5 3 1 1 1 0 1 1 0 2 06 15 3 0 1 2
00 00 4 3 02 00 03 16 5 4 3 3 3 4 3 1 1 5 2 2 2 2 2 3 3 3 3 2 2 2 2 2 1 1 1 3 5 3 4 1 5 10 03 8 3 3 3 04
07 05 5 7 13 03 19 08 7 5 4 4 4 3 4 5 5 5 2 1 2 2 2 2 2 2 2 2 2 2 2 1 4 3 4 3 3 4 4 9 9 03 04 5 5 7 8 05 05 7
09 15 5 3 03 18 04 03 3 2 2 2 2 2 3 2 3 2 3 3 2 3 3 3 3 3 3 3 3 3 3 3 3 4 3 4 4 2 3 4 4 02 02 2 3 3 3 11 15 9
12 10 9 7 06 05 04 04 3 3 2 2 1 1 2 2 2 2 3 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 3 2 3 1 1 2 2 03 04 4 5 6 7 09 10 12
""".strip()
ver = [[int(s) for s in line.split()] for line in ver_str.split('\n')]
hor_rows = [[int(s) for s in line.split()] for line in hor_str.split('\n')]
hor = []
for col_idx in range(max(map(len, hor_rows))):
col = []
hor.append(col)
for row in hor_rows:
if col_idx < len(row) and row[col_idx]:
col.append(row[col_idx])
print(ver)
print(hor)
In [27]:
import json
json.dumps({'ver': ver, 'hor': hor})
Out[27]:
In [31]:
import forge
from puzzle.puzzlepedia import puzzlepedia
puzzle = puzzlepedia.parse("""
@ 1 2 3 4 5 6 7 8 9 10
* BigOldBell
* BootyJuker
* CorkChoker
* FacePinner
* FakeTurtle
* LemurPoker
* PixieProng
* SheepStick
* SqueezeToy
* TinyStools
""".lower())
In [8]:
import Numberjack
model = Numberjack.Model()
x = {}
for name in 'abcd':
x[name] = Numberjack.Variable([4, 5, 6, 8], name)
model.add(Numberjack.AllDiff(x.values()))
model.add(Numberjack.Sum([x[n] for n in 'abcd']) == 23)
base = 1
for n in 'efgh':
base = x[n] * base
model.add(base == 42)
solver = model.load('Mistral')
solver.solve()
print("is_sat", solver.is_sat())
print("is_unsat", solver.is_unsat())
print(model)
for name in 'abcdefgh':
print(x[name], x[name].get_value())
In [ ]: