feat: homework sheet 5

Author: phillip-keldenich

homework/HW05/HW05.pdf

@@ -0,0 +1,8 @@
+.venv/
+__pycache__/
+.pytest_cache/
+.ruff_cache/
+*.pyc
+dist/
+build/
+*.egg-info/

homework/HW05/exercise01/.gitignore

@@ -0,0 +1,13 @@
+# n queens problem SAT/CP-SAT solver
+By running `pip install -e .` in a suitably-configured environment (containing pip),
+you should be able to install the basic solver skeleton (which is incomplete).
+Running tests can be done by running `pytest` in this directory.
+
+## Running the solvers on some n
+```queens-sat 123 --time-limit=300```
+```queens-cpsat 123 --time-limit=300```
+
+## Implementation notes
+For the SAT version, you essentially only have to edit the `NQueensSATModeler` class in `sat_model.py`.
+For the CP-SAT version, you have to edit the `NQueensCPSAT` class in `cpsat_model.py`.
+

homework/HW05/exercise01/README.md

@@ -0,0 +1,44 @@
+[build-system]
+requires = ["hatchling>=1.25"]
+build-backend = "hatchling.build"
+
+[project]
+name = "queens"
+version = "0.1.0"
+description = "Teaching scaffold for solving the N-queens problem with a SAT solver (PySAT) and a CP solver (OR-Tools)."
+readme = "README.md"
+requires-python = ">=3.11"
+license = { text = "MIT" }
+authors = [
+  { name = "Phillip Keldenich" },
+  { name = "Dominik Krupke" },
+]
+dependencies = [
+  "python-sat>=1.9.dev5",
+  "ortools>=9.14.6206",
+  "pytest"
+]
+
+[project.optional-dependencies]
+dev = [
+  "pytest>=9.0",
+  "ruff>=0.11",
+]
+
+[project.scripts]
+queens-sat = "queens.cli:sat_main"
+queens-cpsat = "queens.cli:cpsat_main"
+
+[tool.hatch.build.targets.wheel]
+packages = ["src/queens"]
+
+[tool.pytest]
+minversion = "9.0"
+testpaths = ["tests"]
+
+[tool.ruff]
+line-length = 100
+target-version = "py311"
+
+[tool.ruff.lint]
+select = ["E", "F", "I", "B"]

homework/HW05/exercise01/pyproject.toml

@@ -0,0 +1,3 @@
+"""N-queens solvers using a SAT solver (PySAT) and a CP solver (OR-Tools)."""
+
+__version__ = "0.1.0"

homework/HW05/exercise01/src/queens/__init__.py

@@ -0,0 +1,67 @@
+import argparse
+from collections.abc import Sequence
+
+from queens.model_cpsat import NQueensCPSAT
+from queens.model_sat import solve_with_sat
+
+
+def _positive_int(value: str) -> int:
+    try:
+        n = int(value)
+    except ValueError as exc:
+        raise argparse.ArgumentTypeError("n must be an integer") from exc
+    if n < 1:
+        raise argparse.ArgumentTypeError("n must be a positive integer")
+    return n
+
+
+def _positive_float(value: str) -> float:
+    try:
+        time_limit = float(value)
+    except ValueError as exc:
+        raise argparse.ArgumentTypeError("time limit must be a number") from exc
+    if time_limit <= 0:
+        raise argparse.ArgumentTypeError("time limit must be positive")
+    return time_limit
+
+
+def _build_parser(program_name: str) -> argparse.ArgumentParser:
+    parser = argparse.ArgumentParser(prog=program_name)
+    parser.add_argument("n", type=_positive_int, help="size of the n x n board")
+    parser.add_argument(
+        "--time-limit",
+        type=_positive_float,
+        default=None,
+        help="optional solver time limit in seconds",
+    )
+    return parser
+
+
+def _print_result(
+    n: int, result: list[list[bool]] | bool | None, build_time: float, solve_time: float
+):
+    if isinstance(result, list):
+        status = f"solution found for n={n}"
+    elif result is False:
+        status = f"n={n} is unsatisfiable"
+    else:
+        status = f"timeout occurred for n={n}"
+    print(f"Status: {status}")
+    print(f"Model build time: {build_time:.6f}s")
+    print(f"Solve time: {solve_time:.6f}s")
+
+
+def sat_main(argv: Sequence[str] | None = None) -> int:
+    args = _build_parser("queens-sat").parse_args(argv)
+    times: dict[str, float] = {}
+    result = solve_with_sat(args.n, time_limit=args.time_limit, times=times)
+    _print_result(args.n, result, times["build_time"], times["solve_time"])
+    return 0
+
+
+def cpsat_main(argv: Sequence[str] | None = None) -> int:
+    args = _build_parser("queens-cpsat").parse_args(argv)
+    model = NQueensCPSAT(args.n)
+    result = model.solve(time_limit=args.time_limit)
+    _print_result(args.n, result, model.model_build_time, model.solve_time)
+    return 0

homework/HW05/exercise01/src/queens/cli.py

@@ -0,0 +1,46 @@
+from time import perf_counter
+
+from ortools.sat.python import cp_model
+
+
+class NQueensCPSAT:
+    def _build_model(self):
+        """
+        Build the model (i.e., create a list of variables via 
+        `self.model.new_bool_var` and add constraints like 
+        `self.model.add_exactly_one` or
+        `self.model.add_at_most_one`).
+        """
+        # TODO
+        raise NotImplementedError()
+
+    def _decode_solution(self):
+        """
+        Decode the solution found by and stored in self.solver;
+        you can access the value of some boolean variable like
+        `self.solver.boolean_value(x)`.
+        """
+        # TODO
+        raise NotImplementedError()
+
+    def __init__(self, n):
+        self.n = n
+        self.model = cp_model.CpModel()
+        before = perf_counter()
+        self._build_model()
+        after = perf_counter()
+        self.model_build_time = after - before
+
+    def solve(self, time_limit: float | None = None) -> bool | None | list[list[bool]]:
+        before = perf_counter()
+        self.solver = cp_model.CpSolver()
+        if time_limit is not None:
+            self.solver.parameters.max_time_in_seconds = time_limit
+        status = self.solver.solve(self.model)
+        after = perf_counter()
+        self.solve_time = after - before
+        if status in (cp_model.CpSolverStatus.FEASIBLE, cp_model.CpSolverStatus.OPTIMAL):
+            return self._decode_solution()
+        if status == cp_model.CpSolverStatus.INFEASIBLE:
+            return False
+        return None

homework/HW05/exercise01/src/queens/model_cpsat.py

@@ -0,0 +1,103 @@
+from threading import Timer
+from time import perf_counter
+
+from pysat.formula import CNF
+from pysat.solvers import Solver
+
+
+class NQueensSATModeler:
+    """
+    Modeler class for the n queens problem using SAT.
+    """
+
+    def __init__(self, n):
+        self.n = n
+        self.cnf: CNF | None = None
+        self._cnf_breaks_symmetries = False
+
+    def create_formula(self, break_symmetries=False) -> CNF:
+        """
+        Create a CNF formula representing the N-queens problem.
+        If break_symmetries is True, this method may add additional
+        constraints that break a mirror symmetry of the problem,
+        which may help some SAT solvers find solutions faster.
+        The only hard requirement is that, if break_symmetries is False,
+        the returned formula must be satisfied by all valid N-queens solutions.
+        """
+        if self.cnf is not None and self._cnf_breaks_symmetries == break_symmetries:
+            return self.cnf
+        self.cnf = CNF()
+        self._cnf_breaks_symmetries = break_symmetries
+        # TODO: add clauses to self.cnf (via self.cnf.append or self.cnf.extend);
+        # e.g., self.cnf.append([1, -2, 3, 4]) for (x1 OR NOT x2 OR x3 OR x4)
+        raise NotImplementedError()
+        return self.cnf
+
+    def decode_solution(self, model: list[int]) -> list[list[bool]]:
+        """
+        Decodes a model (list of literals like [1, -2, 3, -4, ...])
+        as returned by a PySAT SAT solver into a 2D list of booleans.
+        """
+        # TODO
+        raise NotImplementedError()
+
+    def encode_assignment(self, assignment: list[list[bool]]) -> list[int]:
+        """
+        Encodes a 2D list of booleans representing an N-queens solution
+        into a list of literals (like [1, -2, 3, -4, ...]) that can be used
+        as input to a PySAT SAT solver or be used by debug/test methods to
+        check that the formula is satisfied by what should be a satisfying assignment.
+        As long as the formula created by create_formula was created with
+        break_symmetries=False, the returned list of literals should satisfy
+        the formula if and only if the input assignment is a valid N-queens solution.
+        """
+        # TODO
+        raise NotImplementedError()
+
+
+def solve_with_sat(
+    n,
+    break_symmetries=False,
+    solver_name="Cadical300",
+    time_limit: float | None = None,
+    times: dict | None = None,
+) -> list[list[bool]] | bool | None:
+    """
+    Run the named SAT solver on the given n (potentially with symmetry breaking
+    constraints, if implemented) and with a time limit.
+    This method should not need to be changed; all necessary changes should be
+    local to the NQueensSATModeler class.
+    """
+    before = perf_counter()
+    modeler = NQueensSATModeler(n)
+    formula = modeler.create_formula(break_symmetries=break_symmetries)
+    solver = Solver(name=solver_name)
+    timer = None
+
+    def interrupt():
+        solver.interrupt()
+
+    try:
+        solver.append_formula(formula.clauses, no_return=True)
+        build = perf_counter()
+        if times is not None:
+            times["build_time"] = build - before
+        if time_limit is not None:
+            timer = Timer(time_limit, interrupt, [solver])
+            timer.start()
+            r = solver.solve_limited(expect_interrupt=True)
+        else:
+            r = solver.solve()
+        after = perf_counter()
+        if times is not None:
+            times["solve_time"] = after - build
+        if r is None:
+            return None
+        if r is False:
+            return False
+        model: list[int] = solver.get_model()  # type: ignore
+        return modeler.decode_solution(model)
+    finally:
+        if timer is not None:
+            timer.cancel()
+        solver.delete()

homework/HW05/exercise01/src/queens/model_sat.py

@@ -0,0 +1,26 @@
+def verify_assignment(n, assignment: list[list[bool]]):
+    for row_index, row in enumerate(assignment):
+        s = sum(row)
+        if s != 1:
+            raise ValueError(f"Row {row_index} has {s} queens, expected 1")
+
+    for col_index in range(n):
+        s = sum(assignment[row_index][col_index] for row_index in range(n))
+        if s != 1:
+            raise ValueError(f"Column {col_index} has {s} queens, expected 1")
+
+    for row_index, row in enumerate(assignment):
+        for col_index, cell in enumerate(row):
+            if not cell:
+                continue
+            for direction in [(-1, -1), (-1, 1), (1, -1), (1, 1)]:
+                for step in range(1, n):
+                    r = row_index + direction[0] * step
+                    c = col_index + direction[1] * step
+                    if r < 0 or r >= n or c < 0 or c >= n:
+                        break
+                    if assignment[r][c]:
+                        raise ValueError(
+                            f"Queens at ({row_index}, {col_index}) and ({r}, {c}) "
+                            "are attacking each other diagonally"
+                        )

homework/HW05/exercise01/src/queens/verify.py

@@ -0,0 +1,17 @@
+from queens.cli import cpsat_main, sat_main
+
+
+def test_sat_cli_reports_solution(capsys):
+    assert sat_main(["4"]) == 0
+    out = capsys.readouterr().out
+    assert "Status: solution found for n=4" in out
+    assert "Model build time:" in out
+    assert "Solve time:" in out
+
+
+def test_cpsat_cli_reports_unsatisfiable(capsys):
+    assert cpsat_main(["2"]) == 0
+    out = capsys.readouterr().out
+    assert "Status: n=2 is unsatisfiable" in out
+    assert "Model build time:" in out
+    assert "Solve time:" in out