GSAT with random walk
Algorithms AIMech:GSATWithRandomWalk DRAFT
Aliases: GWSAT
A GSAT variant that mixes a uniformly chosen flip from the distinct variables currently occurring in unsatisfied clauses with a globally best GSAT flip, using a fixed probability to choose the focused random move.
Identity Notes & Concept Scope
This is the mixed random-walk extension of GSAT described by Selman and Kautz and clarified in the later noise paper. Its focused move samples a duplicate-free union of eligible variables, not a clause followed by one of its variables. The latter distribution underlies the separately described WSAT family. It is also distinct from unrestricted GSAT random noise and from a pure clause-first walk for 2-SAT. No normalized identity match was found across all 442 pinned AIO labels/scoped synonyms and 316 preceding native IDs/names/aliases. Full-checkout fixed-string searches included ignored and hidden files in worktree and main, returning 7 and 7 lines respectively. All seven unique lines were inspected, and the sorted checkout hit sets were identical: neighboring GSAT/WalkSAT mentions and saved review/ledger references, not existing candidate records. Eight exact AIO CLASS nodes with scoped synonyms/comments and outgoing edges and four full native neighboring records were inspected. Absence is bounded to this snapshot and semantic neighborhood.
Claims & Grounded Evidence
2 Claims
Mechanism
#method
Maintain a complete assignment of the variables in the input CNF formula. Stop successfully when it satisfies the formula. Otherwise, with fixed probability p, select uniformly from the distinct variables appearing in at least one currently unsatisfied clause and flip the chosen variable. With probability 1−p, evaluate all single-variable flips and choose a largest increase in the total number of satisfied clauses, breaking tied best choices randomly as in GSAT. The random and greedy branches can make non-improving moves. The extension can use the GSAT outer random-initialization, per-attempt flip budget and restart/attempt budget. The 1994 paper explicitly explains the duplicate-free variable list, which gives equal probabilities to eligible variables even when their clause occurrence counts differ.
Scope
#documented-name
The UBCSAT project documents GWSAT as GSAT with Random Walk and associates that named implementation with the Selman–Kautz extension.
⚠️ Curated Limitations & Negative Results
- The focused random branch and the global greedy branch use different candidate sets. Replacing the former by random-clause-then-random-variable sampling changes the transition distribution, even at p=1. Shared behavior at p=0 does not make the full variant identical to basic GSAT.
- Finite search failure is not a proof of unsatisfiability. The polynomial analysis cited for pure random walks on satisfiable 2-CNF does not establish a corresponding general-CNF bound for this mixture.
- The noise parameter, CNF encoding, initialization and outer budgets affect behavior. No single best p, universal speedup or numerical benchmark claim is curated. Empty clauses or empty candidate sets require explicit handling outside the described nonempty-variable flip rule.
- The record curates the move policy and its stated GSAT context, not an executed solver or a certification of every loop boundary. The original GSAT pre-flip-only pseudocode boundary remains an implementation choice to declare.
Artificial Intelligence Ontology (AIO) Grounding
Explicit AIO Snapshot Assessment: No Match
Rationale: No suitable target was established for these symbolic SAT-search variants in the inspected snapshot and semantic neighborhood. Stochastic moves, noise terminology and logical formulas do not justify a forced learning-task, neural-layer or language-model mapping.
Search Scope: All 442 pinned AIO labels/scoped synonyms and 316 preceding maintained IDs/names/aliases; ignored/hidden full-checkout text in main and worktree; semantic labels for search, heuristics, satisfiability, logic, reasoning, noise and randomness; eight exact AIO CLASS nodes and four complete native neighbors.
| Examined AIO Candidate | Rejection Reason |
|---|---|
AIO:ReasoningLLM
|
A language model performing reasoning during language tasks is not a CNF assignment-search algorithm. |
AIO:TrainingStrategy
|
These SAT procedures do not require preprocessing or training a machine-learning model. |
AIO:MachineLearningTask
|
Searching a supplied formula for a model does not itself require developing a method that learns from data. |
AIO:ReinforcementLearning
|
Random exploration and greedy clause scores do not make this fixed-formula search a reinforcement-learning task or a learned action-value method. |
AIO:MarkovChain
|
Fixed configurations can admit a Markov description, but that representation does not establish this named algorithm’s identity or a specific semantic mapping to the pinned network/model class. No transition-model concept is curated here. |
AIO:ArtificialNeuralNetwork
|
The described mechanisms manipulate Boolean assignments and clause counts, without requiring a network of artificial neurons. |
AIO:NoiseDenseLayer
|
Random variable flips in SAT search are not noise injection into dense-layer weights for neural regularization. |
AIO:GaussianNoiseLayer
|
The noise is a choice of discrete search move, not additive zero-centered Gaussian regularization of neural inputs. |
Evidence Sources & Primary Literature
3 Sources| Source ID | Publication / Document | Type / Access | Reference & Checksum |
|---|---|---|---|
method-source
|
Bart Selman, Henry A. Kautz, Bram Cohen
|
primary paper
full_text
|
sha256:fd839ba6780a…
|
original-extension
|
Bart Selman, Henry Kautz
|
primary paper
full_text
|
sha256:f301bd7ff353…
|
algorithm-documentation
|
UBCSAT project
|
official documentation
documentation
|
sha256:032a526131ab…
|
Curation Provenance
Curator: Codex
Method: ai_assisted
Model: GPT-6
Created: 2026-10-11T15:17:13Z
Updated: 2026-10-11T15:17:13Z
Source File:
data/curated/GSATWithRandomWalk.yaml