From fffd76406e8415ad7f7af00d22cf9036b79766e1 Mon Sep 17 00:00:00 2001 From: "Nicholas H.Tollervey" Date: Fri, 29 May 2026 15:47:15 +0100 Subject: [PATCH 1/2] Add PyScript examples for python-sat Generated by apply_llm_response.py from prompts/python-sat/response.toml. Examples included: - sat_basics: SAT basics: solving a simple formula - enumerate_models: Enumerating all solutions - cardinality_pigeonhole: Cardinality constraints and the pigeonhole principle Generated-By: apply_llm_response.py --- examples/python-sat/README.md | 18 +++++ .../python-sat/cardinality_pigeonhole/code.py | 71 +++++++++++++++++++ .../cardinality_pigeonhole/config.toml | 1 + .../cardinality_pigeonhole/setup.py | 22 ++++++ examples/python-sat/enumerate_models/code.py | 41 +++++++++++ .../python-sat/enumerate_models/config.toml | 1 + examples/python-sat/enumerate_models/setup.py | 21 ++++++ examples/python-sat/order.json | 5 ++ examples/python-sat/sat_basics/code.py | 47 ++++++++++++ examples/python-sat/sat_basics/config.toml | 1 + examples/python-sat/sat_basics/setup.py | 46 ++++++++++++ 11 files changed, 274 insertions(+) create mode 100644 examples/python-sat/README.md create mode 100644 examples/python-sat/cardinality_pigeonhole/code.py create mode 100644 examples/python-sat/cardinality_pigeonhole/config.toml create mode 100644 examples/python-sat/cardinality_pigeonhole/setup.py create mode 100644 examples/python-sat/enumerate_models/code.py create mode 100644 examples/python-sat/enumerate_models/config.toml create mode 100644 examples/python-sat/enumerate_models/setup.py create mode 100644 examples/python-sat/order.json create mode 100644 examples/python-sat/sat_basics/code.py create mode 100644 examples/python-sat/sat_basics/config.toml create mode 100644 examples/python-sat/sat_basics/setup.py diff --git a/examples/python-sat/README.md b/examples/python-sat/README.md new file mode 100644 index 0000000..d589e24 --- /dev/null +++ b/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. diff --git a/examples/python-sat/cardinality_pigeonhole/code.py b/examples/python-sat/cardinality_pigeonhole/code.py new file mode 100644 index 0000000..0bfd0fb --- /dev/null +++ b/examples/python-sat/cardinality_pigeonhole/code.py @@ -0,0 +1,71 @@ +# --------------------------------------------------------------------- +# 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. + +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 {len(formula.clauses)} 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? {sat_4_3} (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? {sat_4_4}") + +# 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"Pigeon {p}Hole {h}") + break + +display(HTML( + "" + "" + f"{''.join(rows)}
PigeonAssigned hole
" +), append=True) diff --git a/examples/python-sat/cardinality_pigeonhole/config.toml b/examples/python-sat/cardinality_pigeonhole/config.toml new file mode 100644 index 0000000..8a705a4 --- /dev/null +++ b/examples/python-sat/cardinality_pigeonhole/config.toml @@ -0,0 +1 @@ +packages = ["python-sat"] diff --git a/examples/python-sat/cardinality_pigeonhole/setup.py b/examples/python-sat/cardinality_pigeonhole/setup.py new file mode 100644 index 0000000..a33bb13 --- /dev/null +++ b/examples/python-sat/cardinality_pigeonhole/setup.py @@ -0,0 +1,22 @@ +"""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"{text}"), append=True) + + +def note(text): + display(HTML(f"

{text}

"), append=True) + + +from pysat.formula import CNF, IDPool +from pysat.card import CardEnc, EncType +from pysat.solvers import Solver diff --git a/examples/python-sat/enumerate_models/code.py b/examples/python-sat/enumerate_models/code.py new file mode 100644 index 0000000..d5bb7e0 --- /dev/null +++ b/examples/python-sat/enumerate_models/code.py @@ -0,0 +1,41 @@ +# --------------------------------------------------------------------- +# 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. + +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: {len(solutions)}") + +rows = "".join( + f"{i + 1}{', '.join(basket) or '(empty)'}" + for i, basket in enumerate(solutions) +) +display(HTML( + "" + "" + f"{rows}
#Basket contents
" +), append=True) diff --git a/examples/python-sat/enumerate_models/config.toml b/examples/python-sat/enumerate_models/config.toml new file mode 100644 index 0000000..8a705a4 --- /dev/null +++ b/examples/python-sat/enumerate_models/config.toml @@ -0,0 +1 @@ +packages = ["python-sat"] diff --git a/examples/python-sat/enumerate_models/setup.py b/examples/python-sat/enumerate_models/setup.py new file mode 100644 index 0000000..67c6102 --- /dev/null +++ b/examples/python-sat/enumerate_models/setup.py @@ -0,0 +1,21 @@ +"""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"{text}"), append=True) + + +def note(text): + display(HTML(f"

{text}

"), append=True) + + +from pysat.formula import CNF +from pysat.solvers import Solver diff --git a/examples/python-sat/order.json b/examples/python-sat/order.json new file mode 100644 index 0000000..1697b2c --- /dev/null +++ b/examples/python-sat/order.json @@ -0,0 +1,5 @@ +[ + "sat_basics", + "enumerate_models", + "cardinality_pigeonhole" +] diff --git a/examples/python-sat/sat_basics/code.py b/examples/python-sat/sat_basics/code.py new file mode 100644 index 0000000..eb49bd0 --- /dev/null +++ b/examples/python-sat/sat_basics/code.py @@ -0,0 +1,47 @@ +""" +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 + +# 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? {is_sat}") +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: {', '.join(attending) or '(none)'}") + note(f"Not attending: {', '.join(declined) or '(none)'}") diff --git a/examples/python-sat/sat_basics/config.toml b/examples/python-sat/sat_basics/config.toml new file mode 100644 index 0000000..8a705a4 --- /dev/null +++ b/examples/python-sat/sat_basics/config.toml @@ -0,0 +1 @@ +packages = ["python-sat"] diff --git a/examples/python-sat/sat_basics/setup.py b/examples/python-sat/sat_basics/setup.py new file mode 100644 index 0000000..8ea1104 --- /dev/null +++ b/examples/python-sat/sat_basics/setup.py @@ -0,0 +1,46 @@ +""" +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.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"{text}"), append=True) + + +def note(text): + display(HTML(f"

{text}

"), append=True) + + +# python-sat imports for the examples below. +from pysat.formula import CNF +from pysat.solvers import Solver From a695a01fa751aa9eacdf9eb45671f11c3d75c2ba Mon Sep 17 00:00:00 2001 From: "Nicholas H.Tollervey" Date: Thu, 11 Jun 2026 16:26:25 +0100 Subject: [PATCH 2/2] Fix imports. --- examples/python-sat/cardinality_pigeonhole/code.py | 5 +++++ examples/python-sat/cardinality_pigeonhole/setup.py | 5 ----- examples/python-sat/enumerate_models/code.py | 4 ++++ examples/python-sat/enumerate_models/setup.py | 4 ---- examples/python-sat/sat_basics/code.py | 5 +++++ examples/python-sat/sat_basics/setup.py | 5 ----- 6 files changed, 14 insertions(+), 14 deletions(-) diff --git a/examples/python-sat/cardinality_pigeonhole/code.py b/examples/python-sat/cardinality_pigeonhole/code.py index 0bfd0fb..b7c879c 100644 --- a/examples/python-sat/cardinality_pigeonhole/code.py +++ b/examples/python-sat/cardinality_pigeonhole/code.py @@ -11,6 +11,11 @@ # 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() diff --git a/examples/python-sat/cardinality_pigeonhole/setup.py b/examples/python-sat/cardinality_pigeonhole/setup.py index a33bb13..696b64c 100644 --- a/examples/python-sat/cardinality_pigeonhole/setup.py +++ b/examples/python-sat/cardinality_pigeonhole/setup.py @@ -15,8 +15,3 @@ def heading(text, level=2): def note(text): display(HTML(f"

{text}

"), append=True) - - -from pysat.formula import CNF, IDPool -from pysat.card import CardEnc, EncType -from pysat.solvers import Solver diff --git a/examples/python-sat/enumerate_models/code.py b/examples/python-sat/enumerate_models/code.py index d5bb7e0..c147070 100644 --- a/examples/python-sat/enumerate_models/code.py +++ b/examples/python-sat/enumerate_models/code.py @@ -7,6 +7,10 @@ # 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: " diff --git a/examples/python-sat/enumerate_models/setup.py b/examples/python-sat/enumerate_models/setup.py index 67c6102..1b3de81 100644 --- a/examples/python-sat/enumerate_models/setup.py +++ b/examples/python-sat/enumerate_models/setup.py @@ -15,7 +15,3 @@ def heading(text, level=2): def note(text): display(HTML(f"

{text}

"), append=True) - - -from pysat.formula import CNF -from pysat.solvers import Solver diff --git a/examples/python-sat/sat_basics/code.py b/examples/python-sat/sat_basics/code.py index eb49bd0..a5904e9 100644 --- a/examples/python-sat/sat_basics/code.py +++ b/examples/python-sat/sat_basics/code.py @@ -12,6 +12,11 @@ """ 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: diff --git a/examples/python-sat/sat_basics/setup.py b/examples/python-sat/sat_basics/setup.py index 8ea1104..b4f3ee1 100644 --- a/examples/python-sat/sat_basics/setup.py +++ b/examples/python-sat/sat_basics/setup.py @@ -39,8 +39,3 @@ def heading(text, level=2): def note(text): display(HTML(f"

{text}

"), append=True) - - -# python-sat imports for the examples below. -from pysat.formula import CNF -from pysat.solvers import Solver