Examples/python sat

examples/python-sat/README.md

@@ -0,0 +1,18 @@
+# python-sat Examples
+
+Each sub-directory contains a self-contained example. The order in
+which the examples are to appear is specified in `order.json` (an
+array of directory names in the expected order).
+
+In each example directory you'll find:
+
+* `config.toml` - must conform to the specification outlined here:
+  https://docs.pyscript.net/latest/user-guide/configuration/ This is
+  parsed and ultimately turned into a JSON representation as part of
+  the package's API object.
+* `setup.py` - Python code for contextual and environmental setup,
+  NOT SEEN BY THE END USER, but is run before the `code.py` code is
+  evaluated. Allows us to create useful (IPython) shims, avoid
+  repeating boilerplate and whatnot.
+* `code.py` - the actual code added to the editor which forms the
+  practical example of using the package.

examples/python-sat/cardinality_pigeonhole/code.py

@@ -0,0 +1,76 @@
+# ---------------------------------------------------------------------
+# Cardinality encodings: "at most k of these literals are true".
+# ---------------------------------------------------------------------
+#
+# Pure CNF can't directly say "at most one"; it has to be encoded as
+# a bunch of binary clauses. PySAT's `pysat.card` does this for you
+# with several well-known encodings.
+#
+# Classic warm-up: can you place N pigeons into N-1 holes such that
+# each pigeon is in some hole and no hole holds more than one
+# pigeon? The pigeonhole principle says no -- and the SAT solver
+# will agree.
+
+from pysat.formula import CNF, IDPool
+from pysat.card import CardEnc, EncType
+from pysat.solvers import Solver
+
+
+def pigeonhole(n_pigeons, n_holes):
+    """Build a pigeonhole CNF and return (formula, var_map)."""
+    pool = IDPool()
+    # x[p, h] is true iff pigeon p sits in hole h.
+    x = lambda p, h: pool.id(("x", p, h))
+
+    formula = CNF()
+
+    # Each pigeon must occupy at least one hole.
+    for p in range(n_pigeons):
+        formula.append([x(p, h) for h in range(n_holes)])
+
+    # No hole can hold more than one pigeon: AtMost1 over each column.
+    for h in range(n_holes):
+        col = [x(p, h) for p in range(n_pigeons)]
+        at_most_one = CardEnc.atmost(
+            lits=col, bound=1, vpool=pool, encoding=EncType.pairwise,
+        )
+        formula.extend(at_most_one.clauses)
+
+    return formula, x
+
+heading("Pigeonhole: 4 pigeons into 3 holes")
+formula, x = pigeonhole(n_pigeons=4, n_holes=3)
+note(
+    f"Encoded into <strong>{len(formula.clauses)}</strong> clauses "
+    "over the original placement variables plus any auxiliaries "
+    "introduced by the cardinality encoder."
+)
+
+with Solver(name="glucose3", bootstrap_with=formula.clauses) as solver:
+    sat_4_3 = solver.solve()
+note(f"4 pigeons, 3 holes satisfiable? <strong>{sat_4_3}</strong> (as expected).")
+
+# Loosen the constraints: same number of holes as pigeons. Now there's
+# plenty of room and we can read off a valid assignment.
+heading("Pigeonhole: 4 pigeons into 4 holes")
+formula, x = pigeonhole(n_pigeons=4, n_holes=4)
+
+with Solver(name="glucose3", bootstrap_with=formula.clauses) as solver:
+    sat_4_4 = solver.solve()
+    model = set(solver.get_model() or [])
+
+note(f"4 pigeons, 4 holes satisfiable? <strong>{sat_4_4}</strong>")
+
+# Read the placement out of the model by checking each x(p, h) variable.
+rows = []
+for p in range(4):
+    for h in range(4):
+        if x(p, h) in model:
+            rows.append(f"<tr><td>Pigeon {p}</td><td>Hole {h}</td></tr>")
+            break
+
+display(HTML(
+    "<table border='1' cellpadding='6' cellspacing='0'>"
+    "<tr><th>Pigeon</th><th>Assigned hole</th></tr>"
+    f"{''.join(rows)}</table>"
+), append=True)

examples/python-sat/cardinality_pigeonhole/config.toml

@@ -0,0 +1 @@
+packages = ["python-sat"]

examples/python-sat/cardinality_pigeonhole/setup.py

@@ -0,0 +1,17 @@
+"""Lighter setup for cell 3: same names, no IPython shim."""
+import js
+from pyscript import window, HTML, display as _display
+
+js.alert = window.alert
+
+
+def display(*args, **kwargs):
+    return _display(*args, **kwargs, target=__pyscript_display_target__)
+
+
+def heading(text, level=2):
+    display(HTML(f"<h{level}>{text}</h{level}>"), append=True)
+
+
+def note(text):
+    display(HTML(f"<p>{text}</p>"), append=True)

examples/python-sat/enumerate_models/code.py

@@ -0,0 +1,45 @@
+# ---------------------------------------------------------------------
+# Enumerating every satisfying assignment with enum_models().
+# ---------------------------------------------------------------------
+#
+# Many problems aren't just "is there a solution?" but "what are all
+# the solutions?". PySAT's `enum_models()` yields models one at a
+# time, blocking each one internally so the next call returns a
+# genuinely different assignment.
+
+from pysat.formula import CNF
+from pysat.solvers import Solver
+
+
+heading("All ways to pack a 3-item picnic basket")
+note(
+    "Variables: 1 = sandwich, 2 = salad, 3 = cake. Constraints: "
+    "the basket must contain a sandwich OR a salad, and you "
+    "refuse to bring salad without cake."
+)
+
+picnic = CNF()
+picnic.append([1, 2])     # sandwich OR salad
+picnic.append([-2, 3])    # salad -> cake
+
+items = {1: "sandwich", 2: "salad", 3: "cake"}
+
+# Collect every model. For tiny formulas this is fine; for big ones
+# you'd usually cap the count or stop early.
+solutions = []
+with Solver(name="glucose3", bootstrap_with=picnic.clauses) as solver:
+    for model in solver.enum_models():
+        chosen = tuple(items[v] for v in model if v > 0)
+        solutions.append(chosen)
+
+note(f"Total satisfying baskets: <strong>{len(solutions)}</strong>")
+
+rows = "".join(
+    f"<tr><td>{i + 1}</td><td>{', '.join(basket) or '(empty)'}</td></tr>"
+    for i, basket in enumerate(solutions)
+)
+display(HTML(
+    "<table border='1' cellpadding='6' cellspacing='0'>"
+    "<tr><th>#</th><th>Basket contents</th></tr>"
+    f"{rows}</table>"
+), append=True)

examples/python-sat/enumerate_models/config.toml

@@ -0,0 +1 @@
+packages = ["python-sat"]

examples/python-sat/enumerate_models/setup.py

@@ -0,0 +1,17 @@
+"""Lighter setup for cell 2: same names, no IPython shim."""
+import js
+from pyscript import window, HTML, display as _display
+
+js.alert = window.alert
+
+
+def display(*args, **kwargs):
+    return _display(*args, **kwargs, target=__pyscript_display_target__)
+
+
+def heading(text, level=2):
+    display(HTML(f"<h{level}>{text}</h{level}>"), append=True)
+
+
+def note(text):
+    display(HTML(f"<p>{text}</p>"), append=True)

examples/python-sat/order.json

@@ -0,0 +1,5 @@
+[
+    "sat_basics",
+    "enumerate_models",
+    "cardinality_pigeonhole"
+]

examples/python-sat/sat_basics/code.py

@@ -0,0 +1,52 @@
+"""
+A first taste of PySAT: build a CNF formula, hand it to a SAT solver,
+and read off a satisfying assignment.
+
+PySAT exposes many state-of-the-art SAT solvers behind a single,
+uniform Python API. See https://pysathq.github.io for the full docs.
+
+Variables in PySAT are positive integers (1, 2, 3, ...). A clause is
+a list of literals; a negative integer means the negation of that
+variable. A formula in conjunctive normal form (CNF) is a list of
+clauses that must all be satisfied simultaneously.
+"""
+from IPython.core.display import display, HTML
+
+# python-sat imports for the examples below.
+from pysat.formula import CNF
+from pysat.solvers import Solver
+
+
+# Three Boolean variables: 1 = "Alice attends",
+# 2 = "Bob attends", 3 = "Carol attends".
+# We want to pick a guest list satisfying these social constraints:
+#   - At least one of Alice or Bob must come.
+#   - Bob and Carol have a feud, so they can't both come.
+#   - If Alice comes, Carol comes too (Alice -> Carol, i.e. -1 v 3).
+party = CNF()
+party.append([1, 2])      # Alice OR Bob
+party.append([-2, -3])    # NOT Bob OR NOT Carol
+party.append([-1, 3])     # NOT Alice OR Carol
+
+heading("A tiny party-planning SAT problem")
+note(
+    "Three variables, three clauses. The solver finds a guest list "
+    "consistent with every constraint."
+)
+note(f"Clauses: {party.clauses}")
+
+# Glucose 3 is a fast, well-known CDCL solver bundled with PySAT.
+# Pass `bootstrap_with` to load the formula in one go.
+with Solver(name="glucose3", bootstrap_with=party.clauses) as solver:
+    is_sat = solver.solve()
+    model = solver.get_model() if is_sat else None
+
+names = {1: "Alice", 2: "Bob", 3: "Carol"}
+note(f"Satisfiable? <strong>{is_sat}</strong>")
+note(f"Raw model (positive = true, negative = false): {model}")
+
+if model:
+    attending = [names[v] for v in model if v > 0]
+    declined = [names[-v] for v in model if v < 0]
+    note(f"Attending: <strong>{', '.join(attending) or '(none)'}</strong>")
+    note(f"Not attending: {', '.join(declined) or '(none)'}")

examples/python-sat/sat_basics/config.toml

@@ -0,0 +1 @@
+packages = ["python-sat"]

examples/python-sat/sat_basics/setup.py

@@ -0,0 +1,42 @@
+"""
+Shim IPython's display API onto PyScript so example code written in a
+Jupyter/IPython idiom runs unmodified in the browser.
+"""
+
+import sys
+import types
+import js
+from pyscript import window, HTML, display as _display
+
+js.alert = window.alert
+
+
+def display(*args, **kwargs):
+    """Wrap pyscript.display so output lands in the example target."""
+    return _display(
+        *args, **kwargs, target=__pyscript_display_target__,
+    )
+
+
+ipython = types.ModuleType("IPython")
+core = types.ModuleType("IPython.core")
+core_display = types.ModuleType("IPython.core.display")
+core_display.display = display
+core_display.HTML = HTML
+ipython.core = core
+core.display = core_display
+ipython.version_info = (9, 0, 2, '')
+ipython.get_ipython = lambda: None
+ipython.display = core_display
+sys.modules["IPython"] = ipython
+sys.modules["IPython.core"] = core
+sys.modules["IPython.core.display"] = core_display
+sys.modules["IPython.display"] = core_display
+
+
+def heading(text, level=2):
+    display(HTML(f"<h{level}>{text}</h{level}>"), append=True)
+
+
+def note(text):
+    display(HTML(f"<p>{text}</p>"), append=True)