Module grounding 

Finite-domain grounding.

A logic grid — and any finite, domain-closed problem — becomes DECIDABLE by expanding bounded quantifiers over the finite set of individuals named in the premises:

∀x. φ(x)   over {a, b, c, d}   →   φ(a) ∧ φ(b) ∧ φ(c) ∧ φ(d)
∃x. φ(x)   over {a, b, c, d}   →   φ(a) ∨ φ(b) ∨ φ(c) ∨ φ(d)

The result is QUANTIFIER-FREE, so our kernel proves it (certified, explainable) and Z3 decides it in milliseconds — no e-matching, no search blowup, guaranteed to terminate. This is general and reusable: it knows nothing about any specific puzzle, only about quantifiers and the finite domain the premises declare.

Functions

at_most_one_lemmas

“Exactly one φ” entails “at most one φ” — for every premise of the form ∃x(φ(x) ∧ ∀y(φ(y) → y = x)) (what Cardinal(1) produces), emit the PAIRWISE uniqueness ∀x∀y((φ(x) ∧ φ(y)) → x = y).

column_closure_lemmas

HIDDEN SINGLE — the COLUMN closure, dual of the row closure. Each Exactly one φ premise (∃x(φ(x) ∧ ∀y(φ(y) → y = x)), e.g. “exactly one trip is in Florida”) entails that AT LEAST ONE row holds the value: ⋁_{r∈dom} value(r). The row closure says a row takes SOME value; this says a value is taken by SOME row. Together with functionality (a row takes at most one value), it is the deduction a human calls a “hidden single” — once every other row is excluded from a value, the remaining row MUST hold it, and the EXISTING literal unit-propagation forces it.

definite_property_implications

“The unique D-trip has property P.” Each single-∃ definite-description clue ∃x(D(x) ∧ … ∧ P(x)) whose anchor D is a SINGLETON grid value (it carries an Exactly one … premise, so the description denotes a unique row) entails the propagatable rule ∀t(D(t) → P(t)); when P is ALSO a singleton value the biconditional ∀t(P(t) → D(t)) too — e.g. “the Florida trip is the hunting trip” ⇒ In(t,Florida) ↔ Hunt(t). Sound: a singleton value names a unique row, so any row holding it IS that row and therefore carries the clue’s property. This replaces the existential (whose sort-aware grounding still explodes to a row-disjunction) with row-indexed implications the incremental solver propagates.

discharge_unary_facts

Discharge known ground UNARY facts (Trip(Alpha), …) throughout the premises: each is true, so replace it with True and simplify True ∧ X ↦ X, True → X ↦ X. Unit propagation on the sort facts — it strips the sort guards out of every grounded clause ((Trip(x) ∧ In(x,FL)) ∧ … ↦ In(x,FL) ∧ …, and a closure Trip(t) → D ↦ D becomes a bare disjunction fact), leaving the pure value-literal clauses propagation runs on in ONE step. Sound: a true conjunct/antecedent carries no information.

domain_constants

The DOMAIN of a problem: every constant named across exprs. For a domain-closed finite problem this is the universe of individuals to ground over.

functionality_lemmas

FUNCTIONALITY — the missing half of a grid’s bijection. Each closure ∀x(guard(x) → L1 ∨ L2 ∨ … ∨ Ln) says a row takes AT LEAST one value; this emits the AT MOST ONE companion ∀x(Li → ¬Lj) for every ordered pair of distinct disjuncts. A trip is in exactly one state (one year, …), so a value assigned to a row EXCLUDES the row’s other values — the propagation that, together with value-uniqueness, determines the whole grid. Sound: for a square grid functionality is entailed by closure + value-uniqueness + counting, and it is in any case the inherent single-valuedness of the attribute. Each Li must be an atom mentioning the bound variable (a genuine closure), so unrelated ∀→∨ premises are skipped.

ground

Ground every quantifier in e over domain (Herbrand expansion): a universal becomes the conjunction of its instances, an existential the disjunction. The returned expression is quantifier-free when domain covers the universe.

ground_problem

Ground a whole problem — premises AND goal — over the domain of constants they name. The returned premises and goal are quantifier-free (so the kernel proves them, certified, and Z3 decides them instantly).

ground_problem_sorted

ground_problem but sort-aware (each quantifier grounds over its guard sort). The default entry point for finite-domain solving.

ground_sorted

SORT-AWARE grounding: a guarded quantifier expands only over its sort’s domain (∀x(Trip(x)→…) over the trips), falling back to fallback (the full universe) for an unsorted quantifier. Sound for a domain-closed problem and dramatically smaller than universe-grounding — the optimization the larger puzzles need.

simplify_trivial_identities

Fold away trivial (reflexive) identities and the boolean constants they create: a grounded ∃x∃y of-pair has a DIAGONAL instance (x = y = c) carrying ¬(c = c), which is False, so that disjunct must drop. Without it the solver would face an unsatisfiable disjunct it cannot refute (the kernel has no reflexivity rule to prove c = c). Identity(c,c) ↦ True, ¬True ↦ False, then ∧/∨/→ constant-fold.

sort_domains

Per-sort domains: for each UNARY predicate used as a sort guard (Trip, Year, …), the constants asserted to have it. Built from the ground facts the declarations produce (Trip(Alpha), Trip(Beta), …). This is what lets grounding expand ∀x(Trip(x)→…) over the 4 trips, not the whole universe.