The method builds upon Proof-Number Search (PNS) and its space-efficient variant, Depth-First Proof-Number Search (DFPN), and extends them with Grundy numbers for impartial games, culminating in a two-level massively parallel algorithm called PNS-PDFPN.
Proof-Number Search (PNS): This is a best-first search algorithm for NAND trees. It selects and expands a most proving node (MPN) by associating each node v with a proof number pn(v) and a disproof number dn(v). These numbers are lower bounds on the minimum number of leaves to be solved to prove or disprove v. For leaves, pn(v) = dn(v) = 1. For terminals, pn(v) = ∞ and dn(v) = 0. For internal nodes, pn(v) = min_c dn(c) and dn(v) = Σ_c pn(c). The algorithm iteratively finds an MPN by descending from the root, always selecting the child with the lowest disproof number, expands it, and updates numbers on the path back to the root.
Depth-First Proof-Number Search (DFPN): A space-efficient variant of PNS that stores only the nodes along the currently explored path P to the MPN, along with their children. DFPN maintains two thresholds, pt(v) and dt(v), for each node v on P. The MPN occurs in the subtree of v if pn(v) < pt(v) and dn(v) < dt(v). If these conditions are not met, DFPN backtracks. DFPN is often combined with a transposition table to balance time and memory.
Grundy Numbers: For impartial games, the Sprague-Grundy Theorem allows simplifying game trees. A Grundy number gn(P) (nimber) is recursively defined: gn(P) = 0 for terminal positions, and gn(P) = min N₀ \ G otherwise, where G is the set of Grundy numbers of P's children. The outcome of a combination of positions P₁ + ... + Pk is loss if and only if gn(P₁) ⊕ ... ⊕ gn(Pk) = 0. The paper formalizes extended NAND trees with Grundy numbers, categorizing nodes as decomposable, atomic, or Grundy.
DFPN with Grundy Numbers (DFPN with GN): This variant adapts DFPN for extended NAND trees with Grundy numbers. It introduces an additional threshold mt(v) for each node v on the path P, with parameters ps(v) and ds(v).
Key Equations: For an atomic node v, with w as the next node to be selected and w' as its child with the second-lowest disproof number, the thresholds are set as:
pt(w) = dt(v) – dn(v) + pn(w)
dt(w) = min{pt(v), dn(w') + 1}
mt(w) = mt(v)
For a decomposable node v, if v has been generated:
pt(w) = pt(v)
dt(w) = dt(v)
mt(w) = mt(v)
If v has not been generated:
pt(w) = dt(w) = ∞
mt(w) = t(v) – pn(v) + min{pn(w), dn(w)}
where ps(w) = ds(w) = 0 and t(v) = min{pt(v), dt(v), mt(v) – min{ps(v), ds(v)}}.
PNS-PDFPN Algorithm: This new parallel variant operates on two parallelized levels:
- First-Level Parallelization (Distributed Memory): A master process maintains the current proof state and assigns jobs (pseudo-MPN leaves) to workers asynchronously. Workers process these jobs and send back results (proof and disproof numbers) to the master. The master maintains a database of key computed results shared with all workers.
- Second-Level Parallelization (Shared Memory): Each worker performs a parallel DFPN algorithm (PDFPN) using multiple threads on a single cluster node. Threads share a lock-protected transposition table of proof and disproof numbers. Disproof numbers are virtually increased during node selection to decrease redundant computation in shared subtrees.
- Enhancements for Impartial Games: PNS with GN and DFPN with GN are incorporated. All computed Grundy numbers are shared as key results. For decomposable nodes, the next node
w is selected to minimize min{pn(w), dn(w)}.