Solutions to the second round of homework

02-sat-advanced/homework-students-solutions/elblasco_hw_21.py

@@ -0,0 +1,104 @@
+#!/usr/bin/env python3
+
+from pysmt.shortcuts import And, ExactlyOne, Solver, Symbol, BOOL, TRUE
+
+vars = {
+    f"x{i}{j}{k}": Symbol(f"x{i}{j}{k}", BOOL)
+    for i in range(1, 10)
+    for j in range(1, 10)
+    for k in range(1, 10)
+}
+
+assertions = []
+
+# Each number is contained exactly once in each row
+for number in range(1, 10):
+    for row in range(1, 10):
+        assertions.append(
+            ExactlyOne(
+                vars[f"x{row}{col}{number}"]
+                for col in range(1, 10)
+            )
+        )
+
+# Each number is contained exactly once in each column
+for number in range(1, 10):
+    for col in range(1, 10):
+        assertions.append(
+            ExactlyOne(
+                vars[f"x{row}{col}{number}"]
+                for row in range(1, 10)
+            )
+        )
+
+# Each number is contained exactly once in each 3x3 square
+for number in range(1, 10):
+    for srow in range(1, 10, 3):
+        for scol in range(1, 10, 3):
+            assertions.append(
+                ExactlyOne(
+                    vars[f"x{col}{row}{number}"]
+                    for row in range(srow, srow + 3)
+                    for col in range(scol, scol + 3)
+                )
+            )
+
+# Each number should appear exactly once in the first diagonal
+for number in range(1, 10):
+    assertions.append(
+        ExactlyOne(
+            vars[f"x{row_col}{row_col}{number}"]
+            for row_col in range(1, 10)
+        )
+    )
+
+# Each number should appear once exactly once in the second diagonal
+for number in range(1, 10):
+    assertions.append(
+        ExactlyOne(
+            vars[f"x{row_col}{10 - row_col}{number}"]
+            for row_col in range(1, 10)
+        )
+    )
+
+# Hidden: Exactly one number for each cell
+for col in range(1, 10):
+    for row in range(1, 10):
+        assertions.append(
+            ExactlyOne(
+                vars[f"x{row}{col}{number}"]
+                for number in range(1, 10)
+            )
+        )
+
+# Numbers on the homework slide
+assertions.append(
+    And(
+        vars["x135"], vars["x171"], vars["x244"], vars["x259"], vars["x262"],
+        vars["x319"], vars["x393"], vars["x423"], vars["x486"], vars["x529"],
+        vars["x581"], vars["x622"], vars["x687"], vars["x711"], vars["x798"],
+        vars["x846"], vars["x858"], vars["x867"], vars["x933"], vars["x974"]
+    )
+)
+
+
+def print_sudoku_table(model: dict):
+    for row in range(1, 10):
+        if (row - 1) % 3 == 0:
+            print("")
+        for col in range(1, 10):
+            if (col - 1) % 3 == 0:
+                print(" ", end='')
+            for num in range(1, 10):
+                if model[vars[f"x{row}{col}{num}"]] is TRUE():
+                    print(num, end='')
+        print('')
+
+
+with Solver("msat") as solver:
+    solver.add_assertions(assertions)
+    if solver.solve():
+        model = solver.get_model()
+        print_sudoku_table(model)
+    else:
+        print("UNSAT")

02-sat-advanced/homework-students-solutions/elblasco_hw_22.py

@@ -0,0 +1,114 @@
+#!/usr/bin/env python3
+
+# https://logic.puzzlebaron.com/play.php?u2=9db6a5914e4ef572fe50bc57bac9efd5
+
+from pysmt.shortcuts import Or, And, ExactlyOne, Solver, Symbol, BOOL, TRUE
+
+months = ["jan", "feb", "mar", "apr"]
+names = ["guadalupe", "keith", "ollie", "yvette"]
+cultures = ["ashdage", "fujishiro", "stosam", "yersim"]
+
+nvars = {
+    f"{month}{name}": Symbol(f"{month}{name}", BOOL)
+    for month in months
+    for name in names
+}
+
+cvars = {
+    f"{month}{culture}": Symbol(f"{month}{culture}", BOOL)
+    for month in months
+    for culture in cultures
+}
+
+assertions = []
+
+# 1.Ollie has been studying the Stosam culture.
+assertions.append(
+    Or(
+        And(nvars[f"{month}ollie"], cvars[f"{month}stosam"])
+        for month in months
+    )
+)
+
+# 2. Keith will publish 1 month after the person who has been studying the
+# Stosam culture.
+
+assertions.append(
+    Or(
+        And(nvars["febkeith"], cvars["janstosam"]),
+        And(nvars["markeith"], cvars["febstosam"]),
+        And(nvars["aprkeith"], cvars["marstosam"])
+    )
+)
+
+# 3. The student who will publish in March is either the person who has been
+# studying the Yersim culture or Guadalupe.
+
+assertions.append(
+    ExactlyOne(
+        cvars["maryersim"], nvars["marguadalupe"]
+    )
+)
+
+# 4. The student who has been studying the Fujishiro culture will publish 1
+# month after Yvette.
+
+assertions.append(
+    ExactlyOne(
+        And(nvars["janyvette"], cvars["febfujishiro"]),
+        And(nvars["febyvette"], cvars["marfujishiro"]),
+        And(nvars["maryvette"], cvars["aprfujishiro"])
+    )
+)
+
+# Each month must be associated with exactly one name
+for month in months:
+    assertions.append(
+        ExactlyOne(
+            nvars[f"{month}{name}"] for name in names
+        )
+    )
+
+# Each month must be associated with exactly one culture
+for month in months:
+    assertions.append(
+        ExactlyOne(
+            cvars[f"{month}{culture}"] for culture in cultures
+        )
+    )
+
+# Each name must be associated with exactly one month
+for name in names:
+    assertions.append(
+        ExactlyOne(
+            nvars[f"{month}{name}"] for month in months
+        )
+    )
+
+# Each culture must be associated with exactly one month
+for culture in cultures:
+    assertions.append(
+        ExactlyOne(
+            cvars[f"{month}{culture}"] for month in months
+        )
+    )
+
+with Solver("msat") as solver:
+    solver.add_assertions(assertions)
+    if solver.solve():
+        # print("SAT", solver.get_model())
+        model = solver.get_model()
+        for month in months:
+            name_out = [
+                name
+                for name in names
+                if model[nvars[f"{month}{name}"]] is TRUE()
+            ][0]
+            culture_out = [
+                culture
+                for culture in cultures
+                if model[cvars[f"{month}{culture}"]] is TRUE()
+            ][0]
+            print(f"Month {month}: {name_out} {culture_out}")
+    else:
+        print("UNSAT")