Propositional satisfiability asks whether some assignment of truth values makes a formula true. In conjunctive normal form, the formula is an AND of clauses and every clause is an OR of literals. A model satisfies every clause. The decision problem is NP-complete, yet a solver’s practical objective may be narrower: find one model quickly when a model exists.

Theorem-proving attacks the complementary side. To establish that a formula F is unsatisfiable, derive a proof of contradiction or prove ¬F valid in a sound and complete system. Complete backtracking and resolution can certify negative answers, but their search can grow explosively. GSAT gives up the certificate of impossibility in exchange for a very different state space.

The distinction changes what an intermediate state means. A partial-assignment prover accumulates commitments and propagates consequences; a contradiction triggers retreat. GSAT always holds a complete interpretation. Some clauses fail, but the state remains well-defined and can be evaluated by the number of clauses it satisfies. Unsatisfied clauses become a gradient-like defect rather than an immediate dead end.

The authors connect this choice to AI tasks. Deductive queries can be reduced to unsatisfiability, but planning, diagnosis and interpretation can also be formulated as finding models. They suggest that reasoning traditionally cast as theorem proving may sometimes scale better after a model-finding reformulation. This is a methodological proposal, not an equivalence of guarantees.

GSAT’s output contract is asymmetric. If it returns an assignment, checking every original clause establishes correctness: success is sound. If it exhausts its budget, a model may still exist elsewhere in the Boolean hypercube. The message “no satisfying assignment found” is an honest report about one finite search, not a semantic judgement about the formula.

At the start of each try, independently assign every variable true or false. Before each flip, test whether the current assignment satisfies all clauses. If so, return it. Otherwise calculate what would happen if each variable reversed, and select a variable whose flip gives the largest increase in the total number of satisfied clauses.

When several variables share the best score, GSAT chooses randomly among them. Tie randomness matters because a deterministic rule can reconstruct the same cycle. Random starts diversify large-scale location; random ties diversify the path inside one neighbourhood. The algorithm’s outcome is therefore a distribution over runs rather than a single fixed runtime.

MAX-FLIPS decides how long to exploit one basin before restarting. The paper offers a rough guideline of a few times the number of variables, while its table uses larger settings for some difficult random instances. MAX-TRIES normally reflects the total time the application can spend. Both are resource policies, not logical parameters.

If the best available flip improves the clause count, GSAT climbs. If the best change is zero, it moves sideways along a plateau. The pseudocode selects the largest increase even when all increases are negative; the authors note rare successful trajectories containing decreasing moves, while their focused discussion and comparison centre on admitting sideways moves rather than stopping at strict local optima.

After MAX-FLIPS without a model, all information in the current assignment is discarded. Original GSAT does not learn clauses, preserve tabu memory or estimate which restart state is promising. This simplicity makes its mechanism easy to inspect and also exposes what later stochastic local-search procedures would add.

A formula with n variables has 2ⁿ complete assignments. From any assignment, reversing variable p moves along one of n edges. GSAT does not consider multi-variable jumps inside a try. Its neighbourhood is uniform in size even though the clause landscape over those vertices can be jagged, flat or deceptive.

Define S(T) as the number of clauses satisfied by assignment T. The gain of flipping p is Δ(p|T)=S(T⊕p)−S(T). GSAT selects an element of arg max Δ. This objective ignores how strongly a clause is satisfied: a clause with three true literals and a clause with one true literal both contribute one point.

That coarseness is intentional. S is cheap to define, comparable across neighbours and reaches its exact maximum only at a model. But it creates plateaux: many assignments can satisfy the same number of clauses while differing greatly in which clauses fail and how close they are to a model.

An efficient implementation need not recount every clause after every hypothetical flip. For each variable, one can track clauses the flip would make and clauses it would break. Gain equals make minus break. After the chosen flip, update scores only for clauses containing that variable and the variables sharing those clauses. This is implementation logic consistent with the objective, though the paper’s central presentation abstracts from low-level data structures.

The hypercube view clarifies incompleteness. Greedy moves examine only adjacent vertices and restarts sample only finitely many regions. The algorithm may never visit the one vertex: or narrow basin: containing a model. Randomness reduces systematic repetition but does not turn bounded sampling into exhaustive enumeration.

A strict hill climber stops or restarts whenever no positive-gain neighbour exists. Yet a plateau can contain many assignments with the same score. One boundary vertex may have an improving edge even though the current vertex does not. Sideways moves traverse this neutral network until the search reaches an exit.

Because ties are random, GSAT does not follow one fixed plateau path. It may revisit vertices or oscillate, but MAX-FLIPS bounds the cost. Random restart supplies another attempt if the walk fails to find an exit. The method accepts wasted neutral steps because strict monotonicity can strand it much earlier.

The ablation is unusually clear. On 50-variable hard random formulas, the strict-improvement version solved 69 per cent of 100 satisfiable instances within 1,000 tries, versus 100 per cent for all moves. On 100-variable formulas it solved 39 per cent even with 100,000 tries, while all moves solved every tested instance. Parameters and machines belong with these numbers.

The N-queens contrast is sharper. For the 30-queen encoding, strict improvement still eventually solved every instance but averaged about 50,000 tries and 30 hours. With sideways moves, the reported run used one try and 2.5 seconds. Equal-score motion was not cosmetic noise; it connected the initial basin to a productive exit.

The paper notes rare successful sequences containing score-decreasing flips, but concentrates on sideways moves and ignores the rare downhill cases in this comparison. Later algorithms would formalise noise strategies that deliberately accept non-greedy movement. Canon 0084 takes up that extension.

If the probability that one try finds a model within MAX-FLIPS is p and tries are independent, the probability of at least one success after k tries is 1−(1−p)ᵏ. This elementary relation explains why a modest per-try success rate can become reliable under repetition. It also shows why runtime must be reported with success probability.

Actual tries need not be identically distributed when pseudorandom generation, formula symmetry or deterministic tie handling introduces correlations. The formula can also contain basins with radically different escape probabilities. Still, fresh complete assignments reduce dependence on one early commitment more aggressively than local backtracking.

MAX-FLIPS mediates a classic exploration–exploitation trade-off. Too small and the search abandons promising plateau crossings; too large and it spends most of its budget wandering inside a basin with negligible success chance. The paper reports that application families often admit a parameter setting usable across their instances, but this remains empirical tuning.

MAX-TRIES is not evidence about unsatisfiability. Increasing it raises the chance of discovering an existing model but never supplies a finite threshold after which non-discovery becomes a proof. An application may interpret the budget statistically or operationally: “no witness found in ten minutes”: provided it does not change the logical claim.

Restart statistics should include the distribution, not only the mean. One run may succeed immediately and another may consume the whole budget. Later work on heavy-tailed search made this issue explicit. The 1992 paper already embeds the practical response: bound the local run and try again.

Choose N variables, K=3 literals per clause and L clauses. Each clause selects three variables and independently negates each with probability one half. Difficulty depends critically on density L/N. At low density, many assignments satisfy the formula; at very high density, contradictions become easy to expose. Around the transition, solutions are scarce enough to be difficult while unsatisfiability is not yet obvious.

The authors use approximately L≈4.3N for the tested sizes, noting convergence near 4.25 for more than 150 variables and that the exact point was then unknown. Modern threshold estimates should not be imported into a reconstruction of their experimental design. The important control is that comparisons use the hard region rather than easy random samples.

This corrects a known evaluation trap. Earlier average-case results could make complete search look polynomial because the sampled formulas were so satisfiable that random guessing also found models quickly. Benchmark generation is part of the experiment: an algorithm cannot demonstrate hardness-handling on a distribution that rarely generates hard cases.

For smaller sizes, the authors used the complete DP procedure to select satisfiable test instances. For larger formulas DP became impractical, so GSAT was run on instances of initially unknown status and results were reported when models were found. Unsatisfiable formulas are uninformative for a GSAT success test because it will mechanically consume its flip-and-try budget and return non-discovery.

The comparison shows a sharp growth difference on their machine and implementations. DP becomes impractical around the 140-variable region, while GSAT finds models at 300 variables and on some 500-variable formulas. The headline “order of magnitude larger” refers to solvable variable scale in this hard random setting, not a general complexity bound.

At 50 variables and 215 clauses, GSAT used MAX-FLIPS 250, averaged 6.4 tries and took about 0.4 seconds; DP took about 1.4 seconds. At 100 variables and 430 clauses, GSAT averaged 42.5 tries and six seconds, while DP used roughly 84,000 binary choices and 2.8 minutes. By 140 variables and 602 clauses, GSAT’s reported average remained 14 seconds while DP took about 4.7 hours.

Beyond that point the table does not provide DP results. GSAT’s selected satisfiable instances at 200, 250, 300, 400 and 500 variables took from minutes to roughly 1.6 hours under rising flip budgets. Finding any model at those sizes was striking relative to the tested complete baseline, but it does not say how often an unknown random instance was unsatisfiable or how a later complete solver would perform.

Both programs were written in C and run under UNIX on a MIPS machine. The paper counts DP tree choices and GSAT flips to supplement clock time. These operations are not equal-cost units, yet their different growth patterns support the claim that timing is not solely a coding peculiarity.

The comparison uses the Davis–Putnam label for a backtracking procedure with unit propagation. SAT terminology and implementations have since changed. Canon 0082 already showed how Chaff’s propagation, learning and branching engineering transformed complete search. Reading GSAT’s 1992 advantage as a modern local-search-versus-CDCL ranking would be anachronistic.

The result should therefore be stated narrowly and strongly: on hard satisfiable random 3CNF drawn near the chosen transition, the original implementation found models for instances far larger than the complete DP procedure could practically solve, with substantially slower observed growth in its search-work measure. Its failures remained non-conclusive.

For a 125-vertex graph, the 18-colour SAT encoding contains 2,250 variables and 89,288 clauses. GSAT found a colouring in approximately five hours; specialised algorithms in the cited study ranged from about 20 minutes to 1.7 hours. DP ran longer without a model. GSAT was slower than domain methods but surprisingly viable after generic encoding.

The 17-colour encoding contained 2,125 variables and 83,272 clauses. Initial random-start GSAT did not find the likely optimal colouring. A footnote reports later success using non-completely-random initial assignments suggested by Geoff Hinton. This is evidence that initial-state structure matters, not permission to count the original experiment as a clean success.

The N-queens encoding uses one variable per board square, long clauses requiring at least one queen in each row and binary clauses excluding attacks in rows, columns and diagonals. At N=100 it has 10,000 variables and about 1.6 million clauses. GSAT reported 5,076 flips, one try and 195 seconds.

For N above 30, the runs found solutions on the first try, and flips scaled around 0.5N². A random Boolean assignment places roughly half the N² possible queens, most of which must be removed, so this is near a simple lower bound for that starting representation. The authors note that starting with about N queens reduces the needed order to N in later work.

Boolean-induction results are deliberately mixed. GSAT is comparable overall to an integer-programming method, but one reported instance takes 2,764 seconds versus 78 seconds for integer programming, while others favour GSAT dramatically. The table supports broad applicability and heterogeneity, not uniform domination.

The first small group of clauses forces variable 1 to be positive in every model. A much larger group contains its negative literal, so changing 1 to false immediately satisfies many clauses. The greedy clause-count signal therefore pulls search towards the wrong half of the hypercube.

Once variable 1 is false, improving the residual score cannot repair the fundamental mistake without accepting a sufficiently unattractive intermediate move. Ordinary GSAT may solve the family only when a random restart begins near a satisfying assignment. As the construction grows, that favourable region can occupy an exponentially small fraction of states.

This is not a bug in gain calculation. The local objective is exactly maximised at each step, but it is not a reliable potential function for distance to a model. Clause count measures current satisfaction, not the number or accessibility of models downstream. A greedy algorithm can execute its rule perfectly and still be globally misled.

The counterexample also limits “statistically minimal errors”. Rare under tested applications is not impossible, and constructed families are relevant whenever an adversary or generator can exploit the heuristic. A safe use of GSAT must treat budget exhaustion as uncertainty and retain another route when negative conclusions matter.

Later stochastic local-search methods add noise, clause weighting, focused moves and adaptive mechanisms to escape such traps. None eliminates NP-completeness or makes every landscape benign. The enduring lesson is to pair performance distributions with explicit failure semantics.

Soundness on success is elementary and strong. The solver returns a complete assignment only after checking that it satisfies the input formula. A separate verifier can repeat that test in linear time in the number of literal occurrences. Randomness affects how the witness is found, not whether the witness is valid.

Incompleteness concerns both satisfiable and unsatisfiable inputs. On a satisfiable formula, GSAT may miss every model within its budget. On an unsatisfiable formula, it necessarily misses, but its execution looks operationally similar. The final state cannot distinguish “no model exists” from “search did not reach one”.

This limits theorem-proving uses, where the desired result often is precisely unsatisfiability. It favours constructive applications such as finding a plan, configuration, interpretation or vivid model. The authors propose generating one or more vivid representations offline, then answering later queries efficiently against them. Such answers inherit the coverage limits of the sampled models.

For first-order problems with finite Herbrand universes, grounding yields a finite propositional search. The paper suggests iterative expansion for larger universes as a future direction. That proposal adds another incompleteness boundary: failure at one finite universe size says nothing final about larger domains.

A responsible interface should return a witness plus verification details on success, and a resource statement on failure: tries, flips, time, seeds and best score reached. Replacing that statement with “false” or “unsatisfiable” changes the semantics and can make a useful heuristic dangerously misleading.

The random-like landscape contains six three-literal clauses. The plateau landscape contains a ridge on which several assignments share the same clause count. The deceptive landscape repeats semantically redundant clauses so the local count can pull away from a model even though the model set is unchanged by duplication.

Each square represents one assignment in binary order abcd. Fill intensity records satisfied clauses; a teal ring marks the current state; green rings mark models. Neighbour outlines show the four states reachable by one flip. The button chooses the alphabetically first variable among the maximum-gain tie set so the demonstration is reproducible; original GSAT breaks such ties randomly.

Three exact audits cover every formula and all sixteen assignments. First, incremental make-minus-break gain is compared with a full clause recount for every possible flip. Second, each laboratory choice must belong to the exhaustive arg-max set. Third, every vertex labelled a model is reevaluated against every original clause. These tests validate local mechanics, not the 1992 performance claims.

To reproduce GSAT, preserve the complete-assignment state, clause-count objective, one-variable neighbourhood, random tie-breaking, sideways moves, MAX-FLIPS restarts and MAX-TRIES termination. Record random seeds. Return “not found” rather than unsatisfiable. Independently verify every model.

For efficient scoring, store each variable’s positive and negative clause occurrences, current true-literal counts per clause and make/break totals. After a flip, update only affected clauses. Cross-check incremental values against full recounts on small random formulas before using the fast path.

Recreate hard random 3CNF with documented N, L, K, duplicate policy and negation sampling. Separate satisfiable and unsatisfiable populations using an independent complete solver; otherwise GSAT’s non-discovery contaminates runtime with unknown status. Report success probability, conditional time-to-model and censored failures.

Reproduce structured encodings exactly, including symmetry and initial-assignment policy. Generic CNF and domain-preserving local search have different neighbourhoods. For historical comparisons, preserve binaries, compiler, machine, timeouts and parameter grids where possible; otherwise label results as a modern reimplementation rather than a replication.

Audit rare losses and adversarial families alongside averages. Sweep MAX-FLIPS and MAX-TRIES under a fixed total budget. Compare strict improvement, sideways movement and controlled noise. The object is not to make one curve flattering but to reveal which landscapes each policy can and cannot traverse.

Review one: scholarship. The reconstruction preserves complete interpretations, CNF clause count, Hamming-one neighbours, maximum-gain flips, random tie-breaking, nested flip/try budgets, sideways motion, rare downhill qualification, sound-success/incomplete-failure semantics, hard-random density control, DP comparison, structured encodings, the adversarial variable-1 family, vivid-model applications and the absence of an unsatisfiability certificate.

Review two: teaching and execution. Ten paper-specific SVGs explain output contracts, the nested loop, hypercube locality, plateaux, restart probability, the transition region, historical scaling, structured encodings, deceptive gradients and soundness asymmetry. Twelve examples and twelve causal probes isolate distinct links. The laboratory enumerates complete small landscapes instead of animating an untested path.

Evidence and AI-telltale review. Claims retain year, machine, generator, density, status-selection and parameter boundaries. The account includes the failed 17-colouring, the Boolean-induction loss, missing DP results at large N and the constructed exponential trap. It does not equate random non-discovery with proof, call clause count a true distance metric or compare 1992 DP directly with modern CDCL.

Accessibility and responsive review. Each SVG has a unique title, description, caption and source scope; colour is redundant with labels and geometry; motion stops under reduced-motion preference. Controls are visibly labelled, changing output uses text and a live region, the claim table scrolls narrowly, and grids collapse at 900 and 600 pixels. Tests name their exact semantic oracle.

GSAT compresses a formula’s immediate state into one number: clauses satisfied. That number turns a discrete logical space into a navigable landscape. The signal is weak: one bit of clause improvement says little about global model geometry: but it is available at every complete assignment.

Sideways moves reveal why evaluation cannot be equated with progress. Two states can have the same score and radically different escape routes. Agency in this mechanism consists not only of preferring improvement but of spending bounded effort when improvement is temporarily invisible.

Restarts acknowledge another limit: local history can become a liability. Original GSAT discards the whole state rather than diagnose why it failed. This makes it computationally light and epistemically forgetful. Chaff, by contrast, restarts with proof-derived memory. The comparison separates diversification from learning.

The model-finding perspective also changes the product of reasoning. A witness is a positive construction that can be checked without replaying search. A proof of absence requires a different object. Treating these products separately prevents a fast heuristic from being asked to certify what its state does not encode.

GSAT therefore supplies a clean model of bounded rational search: choose a measurable objective, inspect local alternatives, accept neutral motion, restart under a resource budget and verify success. Its impressive competence on selected landscapes and its explicit blind spots both follow from that design. Neither competence nor failure semantics imply consciousness.